Abstract
In this paper, we describe a factorization rule which is based on the introduction of Skolem terms. This rule generalizes non-unifiable terms to a new term not occurring elsewhere in the clause set. Clauses of the form p(x,t 1) ˅ p(y,t 2) are factorized to p(x,m) where t 1 t 2 are ground terms and m is a new constant not occurring in the Herbrand universe of the original clause set. A refutation of p(x,m) implies a refutation of p(x,t 1) ˅ p(y,t 2) but not vice versa. We extend this factorization rule in several ways and show that the application of such rules may increase the performance of automated theorem provers. A linear resolution proof of exponential length may collapse into a linear resolution proof of linear length.
This research was supported by the Federal Ministry for Research and Technology within the project TASSO under grant no. ITW 8900 A7.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Baaz and A. Leitsch. Die Anwendung starker Reduktionsregeln in automatischen Beweisen. Proc. of the Austrian Acad, of Science II, 194:287–307, 1985. In German.
M. Baaz and A. Leitsch. A Strong Reduction Method for Clause Logic. Technical Report 8901, Technische Universität Wien, Institut für Computersprachen, Abteilung für Anwendungen der Formalen Logik, Getreidemarkt 9, A-1060 WIEN, Austria, 1989.
M. Baaz and A. Leitsch. A Strong Problem Reduction Method Based on Function Introduction. In ISSAC 90, pages 30–37. ACM-Press, 1990.
M. Baaz and A. Leitsch. Complexity of Resolution Proofs and Function Introduction. Technical Report TR-9101, Technische Universität Wien, Institut für Computersprachen, Abteilung für Anwendungen der Formalen Logik, Getreidemarkt 9, A- 1060 WIEN, Austria, 1991.
W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987.
W. W. Bledsoe. Splitting and Reduction Heuristics in Automatic Theorem Proving. Artificial Intelligence, 2:57–78, 1971.
C. L. Chang and R. C. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.
U. Egly. Problem-Reduction Methods and Clause Splitting in Automated Theorem Proving. Master#x0027;s thesis, Technische Universität Wien, Institut für Computersprachen, Abteilung für Anwendungen der Formalen Logik, Getreidemarkt 9, A-1060 WIEN, 1990.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETIIEO — A high-performance theorem prover for first-order logic. Journal of Automated Reasoning, 1991.
G. Neugebauer and T. Schaub. A pool-based connection calculus. Technical Report AIDA-91–2, FG Intellektik, FB Informatik, TH Darmstadt, Alexanderstraße 10, D-6100 Darmstadt, January 1991.
F. J. Pelletier. Seventy-Five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2:191–216., 1986.
J. Schumann, N. Trapp, and M. van der Koelen. SETHEO/PARTHEO Users Manual. Report FKI-121–89, Institut für Informatik, Technische Universität München, Arcisstr. 21, D-8000 München 2, Germany, December 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U. (1991). A Generalized Factorization Rule Based on the Introduction of Skolem Terms. In: Kaindl, H. (eds) 7. Österreichische Artificial-Intelligence-Tagung / Seventh Austrian Conference on Artificial Intelligence. Informatik-Fachberichte, vol 287. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-46752-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-46752-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54567-5
Online ISBN: 978-3-642-46752-3
eBook Packages: Springer Book Archive