Advertisement

A New Interpretation of the Resolution Principle

  • Etienne Paul
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

Abstract

We show in this paper that the application of the resolution principle to a set of clauses can be regarded as the construction of a term rewriting system confluent on valid formulas. This result allows the extension of standard properties and methods of equational theories (such as Birkhoff’s theorem and Knuth and Bendix completion algorithm) to quantifier-free first order predicate calculus.

These results are extended to first order predicate calculus in an equational theory, as studied by Plotkin [15], Slagle [17] and Lankford [12].

This paper is a continuation of the work of Hsiang [5], who has already shown that rewrite methods can be used in first order predicate calculus. The main difference is that Hsiang applies rewrite methods only as a refutational proof technique, trying to generate the equation TRUE=FALSE. We generalize these methods to satisfiable theories; in particular, we show that the concept of confluent rewriting system, which is the main tool for studying equational theories, can be extended to any quantifier-free first order theory. Furthermore, we show that rewrite methods can be used even if formulas are kept in clausal form.

Keywords

Normal Form Equational Theory Critical Pair Valid Consequence Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    BIRKHOFF G.: On the structure of abstract algebras. Proc.Cambridge Phil.Soc. 31, pp 433–454 (1935).CrossRefzbMATHGoogle Scholar
  2. [2]
    BUCKEN H.: Reduction systems and small cancellation theory. Proc. Fourth Workshop on Automated Deduction, 53–59 (1979)Google Scholar
  3. [3]
    CHANG C.L. and LEE R.C.: Symbolic logic and mechanical theorem proving. Academic Press, New-York (1973)zbMATHGoogle Scholar
  4. [4]
    FAGES F.: Formes canoniques dans les algebres booleennes, et application a la demonstration automatlque en logique du premier ordre. These de 3me cycle, Universite Pierre et Marie Curie, Juin 1983.Google Scholar
  5. [5]
    HSIANG J. and DERSHOWITZ N.: Rewrite methods for clausal and non-clausal theorem proving. ICALP 83, Spain.(1983).Google Scholar
  6. [6]
    HUET G.: A complete proof of correctness of the KNUTH-BENDIX completion algorithm. INRIA, Rapport de recherche No 25, Juillet 1980.Google Scholar
  7. [7]
    HUET G., OPPEN D.C., Equations and rewrite rules: a survey, Technical Report CSL-11, SRI International, Jan. 1980.Google Scholar
  8. [8]
    HULLOT J.M., Canonical form and unification. Proc. of the Fifth Conference on Automated Deduction, Les Arcs. (July 1980).Google Scholar
  9. [9]
    JOUANNAUD J.P., KIRCHNER C. and KIRCHNER H.: Incremental unification in equational theories. Proc. of the 21th Allerton Conference (1982).Google Scholar
  10. [10]
    JOUANNAUD J.P.: Confluent and coherent sets of reduction with equations. Application to proofs in data types. Proc. 8th Colloquium on Trees in Algebra and Programming (1983).Google Scholar
  11. [11]
    KNUTH D. and BENDIX P., Simple word problems in universal algebra Computational problems in abstract algebra, Ed. Leech J., Pergamon Press, 1970, 263–297.Google Scholar
  12. [12]
    LANKFORD D.S.: Canonical inference, Report ATP-32, Department of Mathematics and Computer Science, University of Texas at Austin, Dec. 1975.Google Scholar
  13. [13]
    LEE R.C.: A completeness theorem and a computer program for finding theorems derivable for given axioms. Ph.D diss. in eng., U. of California, Berkeley, Calif., 1967.Google Scholar
  14. [14]
    PETERSON G. and STICKEL M.: Complete sets of reductions for some equationnal theories. JACM, Vol. 28, No2, Avril 1981, pp 233–264.Google Scholar
  15. [15]
    PLOTKIN G.: Building-in Equational Theories. Machine Intelligence, pp 73–90. (1972)Google Scholar
  16. [16]
    ROBINSON J.A: A machine-oriented logic based on the resolution principle. JACM, Vol.12, No1, Janvier 1965, pp 23–41Google Scholar
  17. [17]
    SLAGLE J.R: Automatic theorem proving for theories with simplifiers, commutativity and associativity. JACM 21, pp. 622–642. (1974)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Etienne Paul
    • 1
  1. 1.Centre national d’etudes des TelecommunicationsIssy les MoulineauxFrance

Personalised recommendations