A New Interpretation of the Resolution Principle
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.
This paper is a continuation of the work of Hsiang , 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.
KeywordsNormal Form Equational Theory Critical Pair Valid Consequence Empty Clause
Unable to display preview. Download preview PDF.
- BUCKEN H.: Reduction systems and small cancellation theory. Proc. Fourth Workshop on Automated Deduction, 53–59 (1979)Google Scholar
- 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
- HSIANG J. and DERSHOWITZ N.: Rewrite methods for clausal and non-clausal theorem proving. ICALP 83, Spain.(1983).Google Scholar
- HUET G.: A complete proof of correctness of the KNUTH-BENDIX completion algorithm. INRIA, Rapport de recherche No 25, Juillet 1980.Google Scholar
- HUET G., OPPEN D.C., Equations and rewrite rules: a survey, Technical Report CSL-11, SRI International, Jan. 1980.Google Scholar
- HULLOT J.M., Canonical form and unification. Proc. of the Fifth Conference on Automated Deduction, Les Arcs. (July 1980).Google Scholar
- JOUANNAUD J.P., KIRCHNER C. and KIRCHNER H.: Incremental unification in equational theories. Proc. of the 21th Allerton Conference (1982).Google Scholar
- 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
- 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
- LANKFORD D.S.: Canonical inference, Report ATP-32, Department of Mathematics and Computer Science, University of Texas at Austin, Dec. 1975.Google Scholar
- 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
- PETERSON G. and STICKEL M.: Complete sets of reductions for some equationnal theories. JACM, Vol. 28, No2, Avril 1981, pp 233–264.Google Scholar
- PLOTKIN G.: Building-in Equational Theories. Machine Intelligence, pp 73–90. (1972)Google Scholar
- ROBINSON J.A: A machine-oriented logic based on the resolution principle. JACM, Vol.12, No1, Janvier 1965, pp 23–41Google Scholar