A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs

DOI10.1112/S1461157000000188zbMath0951.03049OpenAlexW2111155907MaRDI QIDQ4506460

Andrew A. Adams

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/

zbMATH Keywords

weak normalisationimplicational fragment of intuitionistic logiccut-free intuitionistic sequent calculus

Mathematics Subject Classification ID

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

Uses Software

• Coq
• Nuprl
• Automath

Cites Work

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

This page was built for publication: A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs