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 1980 Huet showed that even if the system is not confluent, the Knuth-Bendix procedure still yiels a demi-decision procedure for word problems, provided that every equation can be oriented. In this paper we show that even if there are non-orientable equations, 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 are also given in the paper together with some experiments. Our method can also be extended to more general theories. Comparison with related works is also given. The proof of completeness, which is an interesting subject by itself, employs a new proof technique which utilizes a notion of transfinite semantic trees which is designed for proving refutational completeness of theorem proving methods in general.
Type de document :
[Research Report] RR-0678, INRIA. 1987, pp.20
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 19:30:27
Dernière modification le : samedi 17 septembre 2016 - 01:06:55
Document(s) archivé(s) le : vendredi 13 mai 2011 - 16:03:50



  • HAL Id : inria-00075875, version 1



Michaël Rusinowitch, Jieh Hsiang. On word problems in equational theories. [Research Report] RR-0678, INRIA. 1987, pp.20. 〈inria-00075875〉



Consultations de la notice


Téléchargements de fichiers