Abstract
In this paper, different variants of classical analytic calculi for first-order logic are compared with respect to the length of proofs possible in such calculi. A cut-free sequent calculus is used as a prototype for different other analytic calculi like analytic tableau or various connection calculi. With modified branching rules (β-rules), non-elementary shorter minimal proofs can be obtained for a class of formulae. Moreover, by a simple translation technique and a standard sequent calculus, analytic cuts, i.e., cuts where the cut formulae occur as subformulae in the input formula, can be polynomially simulated.
The author would like to thank Hans Tompits and the referees for their useful comments on an earlier version of this paper.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Baaz, U. Egly, and C. G. Fermüller. Lean Induction Principles for Tableaux. In Proceedings of the International Conference on Theorem Proving with Analytic Tableaux and Related Methods. Springer Verlag, 1997.
M. Baaz and C. G. Fermüler. Non-elementary Speedups between Different Versions of Tableaux. In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Proceedings of the Fourth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 217–230. Springer Verlag, 1995.
M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae, 20:353–379, 1994.
E. W. Beth. Semantic Entailment and Formal Derivability. Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen, 18(13), 1955.
W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second edition, 1987.
W. Bibel. Deduction: Automated Logic. Academic Press, London, 1993.
W. Bibel and E. Eder. Methods and Calculi for Deduction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, chapter 3, pages 67–182. Oxford University Press, Oxford, 1993.
G. Boolos. Don't Eliminate Cut. J. Philosophical Logic, 13:373–378, 1984.
G. Boolos. A Curious Inference. J. Philosophical Logic, 16:1–12, 1987.
S. Cook and R. Reckhow. On the Lenghts of Proofs in the Propositional Calculus. In Proceedings of the 5th Annual ACM Symposium on Theory of Computing, pages 135–148. University of Toronto, 1974.
M. D'Agostino. Are Tableaux an Improvement on Truth-Tables? Cut-Free Proofs and Bivalence. J. Logic, Language and Information, 1:235–252, 1992.
E. Eder. Relative Complexities of First Order Calculi. Vieweg, Braunschweig, 1992.
U. Egly. An Answer to an Open Problem of Urquhart, 1996. Submitted.
U. Egly. On Different Structure-preserving Translations to Normal Form. J. Symbolic Computation, 22:121–142, 1996.
M. Fitting. First-Order Logic and Automated Theorem Proving. Springer Verlag, second edition, 1996.
G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. English translation in [24].
R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. J. Automated Reasoning, 13:297–337, 1994.
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.
J. Posegga and P. H. Schmitt. Automated Deduction with Shannon Graphs. J. Logic and Computation, 5(6):697–729, 1995.
D. Prawitz. A Proof Procedure with Matrix Reduction. In M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger, editors, Symposium on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics, pages 207–214. Springer Verlag, 1970.
K. Schütte. Proof Theory. Springer Verlag, 1977.
R. Smullyan. First-Order Logic. Springer Verlag, 1968.
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.
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). Non-elementary speed-ups in proof length by different variants of classical analytic calculi. In: Galmiche, D. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1997. Lecture Notes in Computer Science, vol 1227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027412
Download citation
DOI: https://doi.org/10.1007/BFb0027412
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62920-7
Online ISBN: 978-3-540-69046-7
eBook Packages: Springer Book Archive