On The Unnecessity of Multiple Overlaps in Completion Theorem Proving
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.
Unable to display preview. Download preview PDF.
- 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.YGoogle Scholar
- 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 Google Scholar
- Herold, A. (1983). Some Basic Notions of First–Order Unification Theory. MEMO-SEKI-VIII, Universität KarlsruheGoogle Scholar
- Hsiang, J. (1982). Topics in Automated Theorem Proving and Program Generation. Ph. D. Thesis, Dep. of Comp. Sci., University of Illinois at Urbana-ChampaignGoogle Scholar
- Knuth, D.E. & Bendix, P.B. (1970). Simple Word Problems in Universal Algebra, in: J. Leech (Ed.): Computational Problems in Universal Algebra, Pergamon PressGoogle Scholar
- 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.YGoogle Scholar
- 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 – 495Google Scholar
- 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 152Google Scholar
- Müller, J. & Socher, R. (1988). Topics in Completion Theorem Proving. SEKI-Report, Universität Kaiserslautern. (To appear)Google Scholar