On word problems in equational theories

Abstract

The Knuth-Bendix procedure for word problems in universal algebra is known to be very effective when it is applicable. However, the procedure will fail if it generates equations which cannot be oriented into rules (i.e., the system is not noetherian), or if it generates infinitely many rules (i.e., the system is not confluent). In 1981 Huet showed that even if the system is not confluent, the Knuth-Bendix procedure still yields a semi-decision procedure for word problems, provided that every equation can be oriented. In this paper we show that even if some equations are not orientable, the Knuth-Bendix procedure can still be modified into a reasonably efficient semi-decision procedure for word problems in equational theories. Thus, we have lifted the noetherian requirement in the Knuth-Bendix procedure. Several confluence results, extensions, and experiments are given. So are some comparisons with related work. The proof of completeness, which is an interesting subject by itself, employs a new proof technique which utilizes a notion of transfinite semantic trees designed for proving refutational completeness of theorem proving methods in general. The outline of the paper is as follows: Section 1 briefly introduces term rewriting. The unfailing Knuth-Bendix procedure and confluence results are given in Section 2, together with some discussions and comparisons. Section 3 extends the results to a more general theory which includes inequalities. Simplification strategies are given in Section 4. In Section 5 we present the completeness proofs, as well as a framework of theorem proving strategies which captures the deletion strategies and fairness of search plans. Section 6 describes an implementation with some experimental results. Section contains some comparisons and discussions. Research reported in this paper is supported in part by the NSF grant DCS-8401624 and the Greco de Programmation of France.