Bounds for cut elimination in intuitionistic propositional logic

DOI10.1007/BF01627506zbMath0765.03028MaRDI QIDQ1204120

Jörg Hudelmaier

Publication date: 1 March 1993

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

zbMATH Keywords

cut eliminationlength of proofinversion principledegrees of formulasefficient decision procedure for intuitionistic propositional logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Subsystems of classical logic (including intuitionistic logic) (03B20) Complexity of proofs (03F20)

Related Items

1998 European Summer Meeting of the Association for Symbolic Logic, An intuitionistic formula hierarchy based on high‐school identities, Admissibility of structural rules for contraction-free systems of intuitionistic logic, Sufficient conditions for cut elimination with complexity analysis, Intuitionistic Decision Procedures Since Gentzen, A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications, Uniform interpolation and the existence of sequent calculi, Some results on cut-elimination, provable well-orderings, induction and reflection, Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas, Invertible infinitary calculus without loop rules for restricted FTL, The G4i analogue of a G3i sequent calculus, Effective longest and infinite reduction paths in untyped λ-calculi

Cites Work

• Unnamed Item
• On the scheme of induction for bounded arithmetic formulas
• Untersuchungen über das logische Schliessen. I
• A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic
• On cut elimination in the presence of perice rule