scientific article; zbMATH DE number 1169377

MaRDI QIDQ4397029zbMATH OpenFDO

Authors G. E. Mints

Publication date 25 June 1998

zbMATH Keywords

cut-free derivationsintuitionistic predicate logicmultiplicative linear logicnatural deduction in linear logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50)

Recommendations

• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Normal form theorem for systems of sequents
• Normal derivations and sequent derivations
• Permutability of proofs in intuitionistic sequent calculi

Cited in

(26)

• Normal derivations and sequent derivations
• Permutability of proofs in intuitionistic sequent calculi
• Termination of permutative conversions in intuitionistic Gentzen calculi
• A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic
• The computational content of arithmetical proofs
• Varieties of linear calculi
• Maximum segments as natural deduction images of some cuts
• A normal form for logical derivations implying one for arithmetic derivations
• Computing interpolants in implicational logics
• Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
• Normal form theorem for systems of sequents
• scientific article; zbMATH DE number 4058922 (Why is no real title available?)
• scientific article; zbMATH DE number 1941934 (Why is no real title available?)
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
• Three faces of natural deduction
• The normalization theorem for extended natural deduction
• Minimum segments in sequent derivations
• Logical Approaches to Computational Barriers
• Normal forms and syntactic completeness proofs for functional independencies
• The elimination of maximum cuts in linear logic and BCK logic
• Permutability in proof terms for intuitionistic sequent calculus with cuts
• Sequent images of normal derivations and natural deduction images of derivations without m-cuts
• Gentzen-Mints-Zucker duality
• The \(\lambda \)-calculus and the unity of structural proof theory
• A connection between cut elimination and normalization

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4397029)