Abstract
In this paper, we compare different normal form translations from a practical point of view. The usual translation of a closed first-order formula to a disjunctive normal form has severe drawbacks, namely the disruption of the formula's structure and an exponential worst case complexity. In contrast, definitional translations avoid these drawbacks by introducing some additional new predicates yielding a moderate increase of the length of the normal form. In implementations, the standard translation is preferred, possibly because the theorem prover has to cope with some additional redundancy introduced by the new predicates. We show that definitional translations can excellently compete with the usual translation by providing run-time measurements with our theorem prover KoMeT. Moreover, for some problems like the halting problem, proofs can only be obtained in reasonable time if definitional translations are used.
The second author was partially supported by the DFG under grant Bi228/6-3. The authors would like to thank the referees for their useful comments on a draft of this paper.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
P. Andrews. Theorem Proving via General Matings. JACM, 28(2):193–214, 1981.
M. Baaz, C. Fermüller, and A. Leitsch. A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation. In LICS, 1994.
W. Bibel. Automated Theorem Proving. Vieweg, second edition, 1987.
W. Bibel, S. Brüning, U. Egly, and T. Rath. Towards an Adequate Theorem Prover Based on the Connection Method. In Proceedings of the Sixth International Conference on Artificial Intelligence and Information-Control of Robots, pages 137–148. World Scientific Publishing Company, 1994.
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, pages 67–182. Oxford University Press, 1993.
T. Boy de la Tour. Minimizing the Number of Clauses by Renaming. In Mark E. Stickel, editor, Proceedings of the Conference on Automated Deduction, Lecture Notes in Computer Science, pages 558–572. Springer Verlag, 1990.
M. Bruschi. The Halting Problem. AAR Newsletter, pages 7–12, March 1991.
A. Bundy, editor. Proceedings of the Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, Springer Verlag, 1994.
L. Burkholder. The Halting Problem. SIGACT News, 18(3):48–60, 1987.
Heng Chu and D. A. Plaisted. Semantically Guided First-Order Theorem Proving using Hyper-Linking. In [8], pages 192–206.
L. Dafa. A Mechanical Proof of the Halting Problem in Natural Deduction Style. AAR Newsletter, pages 4–9, June 1993.
L. Dafa. The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem. AAR Newsletter, pages 1–7, October 1994.
E. Eder. An Implementation of a Theorem Prover Based on the Connection Method. In W. Bibel and B. Petkoff, editors, AIMSA 84. North-Holland, 1984.
E. Eder. Relative Complexities of First Order Calculi. Vieweg, 1992.
U. Egly. On Methods of Function Introduction and Related Concepts. PhD thesis, TH Darmstadt, Alexanderstr. 10, D-64283 Darmstadt, 1994.
U. Egly. On the Value of Antiprenexing. In F. Pfenning, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 69–83. Springer Verlag, 1994.
U. Egly. On Different Structure-Preserving Translations to Normal Form, 1996. Submitted.
U. Egly and T. Rath. The Halting Problem: An Automatically Generated Proof. AAR Newsletter, 30:10–16, 1995.
S. Greenbaum, A. Nagasaka, P. O'Rorke, and D. Plaisted. Comparison of Natural Deduction and Locking Resolution Implementations. In D. W. Loveland, editor, Proceedings of the Conference on Automated Deduction, Lecture Notes in Computer Science, pages 159–171. Springer Verlag, 1982.
R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13:297–337, 1994.
H. J. Ohlbach and C. Weidenbach. A Note on Assumptions about Skolem Functions. Journal of Automated Reasoning, 15:267–275, 1995.
F. J. Pelletier and G. Sutcliffe. An Erratum for Some Errata to Automated Theorem Proving Problems, AAR Newsletter, 31:8–14, 1995.
D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.
M. E. Stickel. A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Technical Note 464, SRI International, 1989.
G. Sutcliffe, Ch. Suttner, and T. Yemenis. The TPTP Problem Library. In [8], pages 252–266.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U., Rath, T. (1996). On the practical value of different definitional translations to normal form. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_103
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_103
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive