Abstract
In this paper, we consider the free-variable variant of the calculus KE and investigate the effect of different preprocessing activities to the proof length of variants of KE. In this context, skolemization is identified to be harmful as compared to the δ-rule. This does not only have consequences for proof length in KE, but also for the “efficiency” of some structural translations. Additionally, we investigate the effect of quantifier-shifting and quantifier-distributing rules, respectively. In all these comparisons, we identify classes of formulae for which a non-elementary difference in proof length occur.
The author would like to thank Hans Tompits for his useful comments on an earlier version of this paper.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baaz, M., Egly, U., Leitsch, A.: Extension Methods in Automated Deduction. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction– A Basis for Applications, part 4, ch. 12, vol. II, pp. 331–360. Kluwer Academic Press, Dordrecht (1998)
Baaz, M., Fermüller, C., Leitsch, A.: A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation. In: LICS 1994, pp. 213–219. IEEE Computer Society Press, Los Alamitos (1994)
Baaz, M., Leitsch, A.: On Skolemization and Proof Complexity. Fundamenta Informaticae 20, 353–379 (1994)
Beckert, B., Posegga, J.: leanTAP: Lean Tableau-based Deduction. J. Automated Reasoning 15(3), 339–358 (1995)
D’Agostino, M.: Are Tableaux an Improvement on Truth-Tables? Cut-Free Proofs and Bivalence. J. Logic, Language and Information 1, 235–252 (1992)
D’Agostino, M., Mondadori, M.: The Taming of the Cut. Classical Refutations with Analytic Cut. J. Logic and Computation 4, 285–319 (1994)
Eder, E.: Relative Complexities of First Order Calculi. Vieweg (1992)
Egly, U.: On the Value of Antiprenexing. In: Pfenning, F. (ed.) Proceedings of the International Conference on Logic Programming and Automated Reasoning, pp. 69–83. Springer, Heidelberg (1994)
Egly, U.: On Different Structure-preserving Translations to Normal Form. J. Symbolic Computation 22, 121–142 (1996)
Egly, U.: Cuts in Tableaux. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction– A Basis for Applications, part 1, ch. 4, vol. I, pp. 103–132. Kluwer Academic Press, Dordrecht (1998)
Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)
Leitsch, A.: The Resolution Calculus. Springer, Heidelberg (1997)
Lifschitz, V.: Computing Circumscription. In: Proceedings of IJCAI-1985, Los Altos, CA., pp. 121–127. Morgan Kaufmann, San Francisco (1985)
McCarthy, J.: Circumscription – A Form of Non-Monotonic Reasoning. Artificial Intelligence 13, 27–39 (1980)
Mondadori, M.: Classical Analytical Deduction. Technical Report Annali dell’Università di Ferrara, Sezione III, Discussion Paper 1, Università di Ferrara (1988)
Orevkov, V.P.: 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, pp. 2337–2350 (1982)
Sieg, W., Kauffmann, B.: Unification for Quantified Formulae. PHIL 44, Carnegie Mellon University (1993)
Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, Leningrad. Seminars in Mathematics, vol. 8, pp. 234–259 (1968); English translation: Consultants Bureau, New York, pp. 115–125 (1970)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U. (1999). Quantifiers and the System KE: Some Surprising Results. In: Gottlob, G., Grandjean, E., Seyr, K. (eds) Computer Science Logic. CSL 1998. Lecture Notes in Computer Science, vol 1584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10703163_7
Download citation
DOI: https://doi.org/10.1007/10703163_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65922-8
Online ISBN: 978-3-540-48855-2
eBook Packages: Springer Book Archive