scientific article; zbMATH DE number 1169377
From MaRDI portal
Publication:4397029
zbMath0897.03053MaRDI QIDQ4397029
Publication date: 25 June 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
intuitionistic predicate logicmultiplicative linear logiccut-free derivationsnatural deduction in linear logic
Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
A connection between cut elimination and normalization ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Three faces of natural deduction ⋮ Computing interpolants in implicational logics ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Permutability of proofs in intuitionistic sequent calculi ⋮ Termination of permutative conversions in intuitionistic Gentzen calculi ⋮ Normal derivations and sequent derivations ⋮ The normalization theorem for extended natural deduction ⋮ Maximum segments as natural deduction images of some cuts ⋮ Varieties of linear calculi
