Abstract
In this paper, we investigate translations from a classical cut-free sequent calculus LK into an intuitionistic cut-free sequent calculus LJ. Translations known from the literature rest on permutations of inferences in classical proofs. We show that, for some classes of first-order formulae, all minimal LJ-proofs are non-elementary but there exist short LK-proofs of the same formula. Similar results are obtained even if some fragments of intuitionistic first-order logic are considered. The size of the corresponding minimal search spaces for LK and LJ are also non-elementarily related. We show that we can overcome these difficulties by extending LJ with an analytic cut rule.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. Eder. Relative Complexities of First Order Calculi. Vieweg, Braunschweig, 1992.
U. Egly. On Different Structure-preserving Translations to Normal Form. J. Symbolic Computation, 22:121–142, 1996.
U. Egly. On Definitional Translations to Normal Form for Intuitionistic Logic. Fundamenta Informaticae, 29(1,2):165–201, 1997.
G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. English translation in [13].
G. Mints. Proof Theory in the USSR 1925–1969. J. Symbolic Logic, 56(2):385–424, 1991.
G. Mints. Resolution Strategies for the Intuitionistic Logic. In B. Mayoh, E. Tyugu, and J. Penyam, editors, Constraint Programming, Nato ASI Series, pages 289–311. Springer Verlag, 1994.
V. P. Orevkov. On Glivenko Sequent Classes. In V. P. Orevkov, editor, The calculi of Symbolic Logic I, volume 98, pages 147–173. Steklov Institute of Mathematics, 1971.
V. P. Orevkov. Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR, 88:137–161, 1979. English translation in J. Soviet Mathematics, 2337–2350, 1982.
D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. J. Symbolic Computation, 2:293–304, 1986.
D. Pym, E. Ritter, and L. Wallen. On the Intuitionistic Force of Classical Search. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, pages 295–311. Springer Verlag, 1996.
D. Pym, E. Ritter, and L. Wallen. Proof-Terms for Classical and Intuitionistic Resolution. In M.A. McRobbie and J. K. Slaney, editors, Proceedings of the Conference on Automated Deduction, pages 17–31. Springer Verlag, 1996.
R. Statman. Intuitionistic Propositional Logic is Polynomial-Space Complete. J. Theoretical Computer Science, 9:67–72, 1979.
M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1969.
G. Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1975.
G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning, pages 466–483. Springer Verlag, 1983.
A. Voronkov. Theorem Proving in Non-standard Logics Based on the Inverse Method. In D. Kapur, editor, Proceedings of the Conference on Automated Deduction, pages 648–662. Springer Verlag, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U. (1997). Some pitfalls of LK-to-LJ translations and how to avoid them. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_14
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive