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 calculusproof theorynatural deductionintuitionistic logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Grammars and rewriting systems (68Q42)

Related Items

CONTRACTIONS OF NONCONTRACTIVE CONSEQUENCE RELATIONS, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, A proof-theoretic study of the correspondence of classical logic and modal logic, The \(\lambda \)-calculus and the unity of structural proof theory, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, Termination of permutative conversions in intuitionistic Gentzen calculi, Theorem proving as constraint solving with coherent logic, A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs, Varieties of linear calculi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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