On The Unnecessity of Multiple Overlaps in Completion Theorem Proving

  • Jürgen Müller
  • Rolf Socher-Ambrosius
Conference paper
Part of the Informatik-Fachberichte book series (INFORMATIK, volume 181)


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.

Unable to display preview. Download preview PDF.


  1. 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
  2. Chang, C.L.& Lee, R.C.T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press, New YorkzbMATHGoogle Scholar
  3. 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
  4. Herold, A. (1983). Some Basic Notions of First–Order Unification Theory. MEMO-SEKI-VIII, Universität KarlsruheGoogle Scholar
  5. 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
  6. Hsiang, J. (1985). Refutational Theorem Proving using Term-rewriting Systems. Artificial Intelligence 25, 255 – 300MathSciNetzbMATHCrossRefGoogle Scholar
  7. 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
  8. 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
  9. 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
  10. 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
  11. Müller, J. & Socher, R. (1988). Topics in Completion Theorem Proving. SEKI-Report, Universität Kaiserslautern. (To appear)Google Scholar
  12. Paterson, M. & Wegman, M. (1978). Linear Unification. Journal of Computer and Systems Science. 16, 158 – 167MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Jürgen Müller
    • 1
  • Rolf Socher-Ambrosius
    • 1
  1. 1.Fachbereich InformatikUniversität KaiserslauternKaiserslauternGermany

Personalised recommendations