Abstract
Completion Theorem Proving is based on the observation that the task of proving a formula can be transformed into the task of solving a system of equations over a boolean polynomial ring. The latter can be accomplished by means of the completion of a set of rewrite rules obtained from the equational system. The central operation in this completion process is the generation of critical pairs comprising the computation of overlaps on products of atoms. This computation requires weak AC-unification, which is known to be NP-hard. Motivated by the THEOPOGLES system (Müller 1987), we show that Hsiang’s (1985) N-strategy can still be strengthened by precluding multiple overlaps. This results in a drastical reduction of the search space. Moreover, these systems manage with unification in a free theory, which can be performed in linear time. Since this special critical pair generation can be translated into a resolution step, provided the two rules correspond to clauses, our result also amounts to a generalization of Dietrich’s (1986) result on the translation from superposition steps into resolution steps.
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
Bachmair, L. & Dershowitz, N. (1987). Inference Rules for Rewrite–Based First Order Theorem Proving. Proc. 2nd Annual Symp. on Logic in Comp. Sci. Ithaca, N.Y
Chang, C.L.& Lee, R.C.T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York
Dietrich, R. (1986). Relating Resolution and Algebraic Completion for Horn Logic. In: J. Siekmann (Ed.): Proc. 8th International Conference on Automated Deduction, Oxford, England. Springer LNCS 230, 62–78
Herold, A. (1983). Some Basic Notions of First–Order Unification Theory. MEMO-SEKI-VIII, Universität Karlsruhe
Hsiang, J. (1982). Topics in Automated Theorem Proving and Program Generation. Ph. D. Thesis, Dep. of Comp. Sci., University of Illinois at Urbana-Champaign
Hsiang, J. (1985). Refutational Theorem Proving using Term-rewriting Systems. Artificial Intelligence 25, 255 – 300
Knuth, D.E. & Bendix, P.B. (1970). Simple Word Problems in Universal Algebra, in: J. Leech (Ed.): Computational Problems in Universal Algebra, Pergamon Press
Kapur, D. & Narendran, P. (1985). An Equational Approach to Theorem Proving in First-Order Predicate Calculus. 84CRD322, General Electric Corp. Research and Development Report, Schenectady, N.Y
Kapur, D. & Narendran, P. (1986). NP-Completeness of the Set Unification and Matching Problems. In: J. Siekmann (Ed.): Proc. 8th International Conference on Automated Deduction, Oxford, England. Springer LNCS 230, 489 – 495
Müller, J. (1987). THEOPOGLES – A Theorem Prover Based on First Order Polynomials and a Special Knuth–Bendix Procedure. In: K. Morik (Ed.): Proc. of 11th German Workshop on Artificial Intelligence, Geseke. Springer IFB 152
Müller, J. & Socher, R. (1988). Topics in Completion Theorem Proving. SEKI-Report, Universität Kaiserslautern. (To appear)
Paterson, M. & Wegman, M. (1978). Linear Unification. Journal of Computer and Systems Science. 16, 158 – 167
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, J., Socher-Ambrosius, R. (1988). On The Unnecessity of Multiple Overlaps in Completion Theorem Proving. In: Hoeppner, W. (eds) Künstliche Intelligenz. Informatik-Fachberichte, vol 181. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-74064-0_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-74064-0_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50293-7
Online ISBN: 978-3-642-74064-0
eBook Packages: Springer Book Archive