Refutational theorem proving using term-rewriting systems.

*(English)*Zbl 0558.68072The paper proposes a new approach to theorem proving in first-order logic based on term-rewriting systems. First, for propositional calculus a canonical term-rewriting system for Boolean algebra is introduced. The key point enabling successful construction of the canonical term- rewriting system (in contrast with all the previous attempts that failed due to the fact that the prime implicant representation of Boolean terms is not unique) consists in choosing exclusive or instead of or. The canonical system for Boolean algebra enables transformation of the first- order calculus into a form of equational logic and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix completion algorithm. These strategies deal with predicate logic and built-in (equational) theories in a uniform and quite efficient way.

Comparison of implementation of a theorem prover based on term-rewriting with other theorem provers based on locking reduction or natural deduction shows that the method proposed is in general much more efficient then the methods based on resolution. Great efficiency and easy modifiability of a theorem prover based on the term-rewriting method makes the method a serious counterpart to resolution and it will probably have significant impact on theorem proving.

Comparison of implementation of a theorem prover based on term-rewriting with other theorem provers based on locking reduction or natural deduction shows that the method proposed is in general much more efficient then the methods based on resolution. Great efficiency and easy modifiability of a theorem prover based on the term-rewriting method makes the method a serious counterpart to resolution and it will probably have significant impact on theorem proving.

Reviewer: J.Zlatuška

##### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

03B30 | Foundations of classical theories (including reverse mathematics) |

03B35 | Mechanization of proofs and logical operations |

03B10 | Classical first-order logic |

06E20 | Ring-theoretic properties of Boolean algebras |

08A50 | Word problems (aspects of algebraic structures) |

##### Software:

REVE
Full Text:
DOI

##### References:

[1] | Bledsoe, W.E., Non-resolution theorem proving, Artificial intelligence, 9, 1-35, (1977) · Zbl 0358.68131 |

[2] | Brand, D., Proving theorems with the modification method, SIAM J. comput., 4, (1975) · Zbl 0333.68059 |

[3] | Chang, C.L.; Lee, C.T., () |

[4] | Cook, S.A., The complexity of theorem proving procedures, (), 151-158 · Zbl 0363.68125 |

[5] | Davis, M., Obvious inferences, () |

[6] | Dershowitz, N., Orderings for term-rewriting systems, Theoret. comput. sci., 17, 3, 279-301, (1982) · Zbl 0525.68054 |

[7] | Dershowitz, N., Private communication, (1983) |

[8] | Dershowitz, N., Applications of the Knuth-bendix completion procedure, () |

[9] | Fages, F., Associative-commutative unification, () · Zbl 0547.03012 |

[10] | Goguen, J.A., How to prove algebraic inductive hypothesis without induction, (), 356-372 |

[11] | Greenbaum, S.; Nabasaka, A.; O’Rorke, P.; Plaisted, D.A., ‘comparison of natural deduction and locking resolution implementations, () |

[12] | Greenbaum, S.; O’Rorke, P.; Plaisted, D.A., Comparison of abstraction and a robust resolution strategy, () |

[13] | Hsiang, J.; Josephson, N.A., Terse: A term rewriting theorem prover, () |

[14] | Huet, G.; Oppen, D.C., Equations and rewrite rules: A survey, () |

[15] | Huet, G.; Hullot, J.M., Proofs by inducation in equational theories with constructors, (), 797-821 |

[16] | Huet, G., A complete proof of correctness of Knuth-bendix completion algorithm, J. comput. system sci., 23, 11-21, (1981) · Zbl 0465.68014 |

[17] | Hullot, J.M., A catalogue of canonical term rewriting systems, () |

[18] | Hullot, J.M., Canonical forms and unification, (), 318-334 |

[19] | Jouannaud, J.P.; Lescanne, P.; Reinig, F., Recursive decomposition ordering, (), 331-346 |

[20] | Jouannaud, J.; Kirchner, H., Completion of a set of rules modulo a set of equations, () · Zbl 0665.03005 |

[21] | Kapur, D.; Narendran, P., An equational approach to predicate calculus, (1984), GE Research Lab, Unpublished manuscript |

[22] | Kirchner, C., A new equational unification method: A generalization of martelli-Montanari’s algorithm, (), 224-247 |

[23] | Knuth, D.E.; Bendix, P.B., Simple word problems in universal algebras, (), 263-297 · Zbl 0188.04902 |

[24] | Kowalski, R.A.; Hayes, P., Semantic trees in automatic theorem proving, (), 181-201 |

[25] | Kuchlin, W., A criterion for constraining critical pair formulation in Knuth-bendix algorithm, (1983), ETH-Zentrum, Unpublished manuscript |

[26] | Lankford, D.S., Canonical inference, () |

[27] | Lankford, D.S.; Ballantyne, A.M., Decision procedure for simple equational theories with commutative-associative axioms, () · Zbl 0449.20059 |

[28] | Lankford, D.S.; Musser, D.R., On semideciding first order validity and invalidity, USC-ISI rept., (1978) |

[29] | Lankford, D.S.; Ballantyne, A.M., The refutation completeness of blocked permutative narrowing and resolution, () |

[30] | Lescanne, P., Computer experiments with the REVE term rewriting system generator, () |

[31] | Livesey, M.; Siekmann, J., Unification of bags and sets, () |

[32] | Manna, Z., () |

[33] | Musser, D.R., On proving inductive properties of abstract data types, (), 154-162 |

[34] | Peterson, G.E.; Stickel, M.E., Complete sets of reductions for some equational theories, J. ACM, 28, 233-264, (1981) · Zbl 0479.68092 |

[35] | Plaisted, D.A., A recursively defined ordering for proving termination of term rewriting systems, () |

[36] | Plaisted, D.A., A simplified problem reduction format, Artificial intelligence, 18, 227-262, (1982) · Zbl 0497.68058 |

[37] | Plotkin, G., Building in equational theories, (), 73-90 · Zbl 0262.68036 |

[38] | Robinson, J.A., Theorem proving on computers, J. ACM, 10, 163-174, (1963) · Zbl 0109.35603 |

[39] | Robinson, J.A., A machine oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41, (1965) · Zbl 0139.12303 |

[40] | Robinson, J.A., The generalized resolution principle, (), 77-94 · Zbl 0195.31102 |

[41] | Siekmann, J.; Szabo, P., Universal unification and a class of equational theories, () · Zbl 0584.68050 |

[42] | Siekmann, J., Universal unification, () · Zbl 0584.68050 |

[43] | Slagle, J.; Norton, K., Experiments with an automatic theorem prover having partial ordering inference rules, Comm. ACM, 682-688, (1973) · Zbl 0271.68062 |

[44] | Slagle, J., Automated theorem-proving for theories with simplifiers, commutativity, associativity, J. ACM, 21, 622-642, (1974) · Zbl 0296.68092 |

[45] | Stickel, M.E., A unification algorithm for associative-commutative functions, J. ACM, 28, 233-264, (1981) · Zbl 0462.68075 |

[46] | Stone, M., The theory of representations for Boolean algebra, Trans. AMS, 40, 37-111, (1936) · JFM 62.0033.04 |

[47] | Watts, D.E.; Cohen, J.K., Computer implemented set theory, Amer. math. monthly, 87, 7, 557-560, (1980) · Zbl 0457.04001 |

[48] | Winkler, F., A criterion for eliminating unnecessary reductions in the Knuth-bendix algorithm, Colloq. algebra, combinatorics, logic comput. sci., (1983) · Zbl 0607.03003 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.