Portal de Periódicos da CAPES

Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.

1970; Elsevier BV; Linguagem: Inglês

10.1016/b978-0-08-012975-4.50028-x

Donald E. Knuth, PETER B. BENDIX,

Formal Methods in Verification

An algorithm is described which is capable of solving certain word problems: i.e. of deciding whether or not two words composed of variables and operators can be proved equal as a consequence of a given set of identities satisfied by the operators. Although the general word problem is well known to be unsolvable, this algorithm provides results in many interesting cases. For example in elementary group theory if we are given the binary operator ·, the unary operator −, and the nullary operator e, the algorithm is capable of deducing from the three identities a · (b · c) = (a · b) · c, a · a− = e, a · e = a, the laws a− · a = e, e · a = a, a– = a, etc.; and furthermore it can show that a · b = b · a− is not a consequence of the given axioms. The method is based on a well-ordering of the set of all words, such that each identity can be construed as a “reduction”, in the sense that the right-hand side of the identity represents a word smaller in the ordering than the left-hand side. A set of reduction identities is said to be “complete” when two words are equal as a consequence of the identities if and only if they reduce to the same word by a series of reductions. The method used in this algorithm is essentially to test whether a given set of identities is complete; if it is not complete the algorithm in many cases finds a new consequence of the identities which can be added to the list. The process is repeated until either a complete set is achieved or until an anomalous situation occurs which cannot at present be handled. Results of several computational experiments using the algorithm are given.