LIPIcs.CSL.2015.94.pdf
- Filesize: 461 kB
- 16 pages
Document
Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic
Authors
-
Part of:
Volume:
24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-09-07
Cite As Get BibTex
Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CSL.2015.94
Abstract
The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.
Subject Classification
Keywords
- Cut-elimination
- sequent calculus
- intuitionistic logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Matthias Baaz and Alexander Leitsch. Cut normal forms and proof complexity. Annals of Pure and Applied Logic, 97(1):127-177, 1999.
-
Matthias Baaz and Alexander Leitsch. Methods of Cut-elimination. Springer, 2011.
-
Samuel R. Buss. An introduction to proof theory. In Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 1-78. Elsevier, 1998.
-
Gerhard Gentzen. Untersuchungen über das logische Schließen. I & II. Mathematische Zeitschrift, 39(1):176-210, 405-431, 1935.
-
Jörg Hudelmaier. Bounds for cut elimination in intuitionistic propositional logic. Archive for Mathematical Logic, 31(5):331-353, 1992.
-
Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4(2):258-282, 1982.
-
V.P. Orevkov. Lower bounds for increasing complexity of derivations after cut elimination. Journal of Soviet Mathematics, 20:2337-2350, 1982.
-
Richard Statman. Lower bounds on Herbrand’s theorem. Proc. of the Amer. Math. Soc., 75:104-107, 1979.