A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
From MaRDI portal
Publication:4506460
DOI10.1112/S1461157000000188zbMath0951.03049MaRDI QIDQ4506460
Publication date: 25 September 2000
Published in: LMS Journal of Computation and Mathematics (Search for Journal in Brave)
Full work available at URL: http://www.lms.ac.uk/jcm/3/lms1999-009/
weak normalisation; implicational fragment of intuitionistic logic; cut-free intuitionistic sequent calculus
03F05: Cut-elimination and normal-form theorems
03B20: Subsystems of classical logic (including intuitionistic logic)
Uses Software
Cites Work
- Rippling: A heuristic for guiding inductive proofs
- Permutability of proofs in intuitionistic sequent calculi
- Termination of permutative conversions in intuitionistic Gentzen calculi
- On proof normalization in linear logic
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
- Contraction-free sequent calculi for intuitionistic logic
- Metamathematics, Machines and Gödel's Proof
- Residual theory in λ-calculus: a formal development
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item