Permutability of proofs in intuitionistic sequent calculi

DOI10.1016/S0304-3975(98)00138-8zbMath0913.68110MaRDI QIDQ1275625

Roy Dyckhoff, Luís Pinto

Publication date: 12 January 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

sequent calculus; proof theory; natural deduction; intuitionistic logic

Mathematics Subject Classification ID

03B60: Other nonclassical logic

68Q42: Grammars and rewriting systems

Related Items

A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs, A proof-theoretic study of the correspondence of classical logic and modal logic, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, The \(\lambda \)-calculus and the unity of structural proof theory, Termination of permutative conversions in intuitionistic Gentzen calculi, Varieties of linear calculi

Cites Work

• Termination of permutative conversions in intuitionistic Gentzen calculi
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Uniform proofs as a foundation for logic programming
• Logic Programming with Focusing Proofs in Linear Logic
• Contraction-free sequent calculi for intuitionistic logic
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item