Bounds for cut elimination in intuitionistic propositional logic
From MaRDI portal
Publication:1204120
DOI10.1007/BF01627506zbMath0765.03028MaRDI QIDQ1204120
Publication date: 1 March 1993
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
cut eliminationlength of proofinversion principledegrees of formulasefficient decision procedure for intuitionistic propositional logic
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
