Cut-elimination and a permutation-free sequent calculus for intuitionistic logic

DOI10.1023/A:1005099619660zbMath0954.03062OpenAlexW1506616756MaRDI QIDQ1577341

Roy Dyckhoff, Luís Pinto

Publication date: 4 September 2000

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1005099619660

zbMATH Keywords

sequent calculusnatural deductionintuitionistic logiccut-eliminationterminationnormalisationrecursive path ordering

Mathematics Subject Classification ID

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

Related Items (9)

Proof-Search in Natural Deduction Calculus for Classical Propositional Logic ⋮ Two loop detection mechanisms: A comparison ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ Genetic programming \(+\) proof search \(=\) automatic improvement ⋮ 1999 Spring Meeting of the Association for Symbolic Logic ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Lexicographic Path Induction ⋮ Permutability of proofs in intuitionistic sequent calculi ⋮ A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs

This page was built for publication: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic