Summary
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. H. Clifford: A system arising from a weakened set of group postulates. Ann. Math. 34 (1933), 865–871.
A. H. Clifford and G. B. Preston: The algebraic theory of semigroups. Math. Surveys 7 ( Amer. Math. Soc., 1961 ).
L. E. Dickson: Definitions of a group and a field by independent postulates. Trans. Amer. Math. Soc. 6 (1905), 198–204.
Trevor Evans: On multiplicative systems defined by generators and relations. I. Normal form theorems. Proc. Camb. Phil. Soc. 47 (1951), 637–649.
Trevor Evans: Products of points—some simple algebras and their identities. Amer. Math. Monthly 74 (1967), 362–372.
J. R. Guard, F. C. Oglesby, J. H. Bennett and L. G. Settle: Semi-automated mathematics. J. Assoc. Comp. Mach. 16 (1969), 49–62.
Donald E. Knuth:Notes on central groupoids. J. Combinatorial Theory (to appear).
Henry B. Mann: On certain systems which are almost groups. Bull. Amer. Math. Soc. 50 (1944), 879–881.
M. H. A. Newman: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43 (1942), 223–243.
J. A. Robinson: A machine-oriented logic based on the Resolution Principle. J. Assoc. Comp. Mach. 12 (1965), 23–41.
O. Taussky: Zur Axiomatik der Gruppen. Ergebnisse eines Math. Kolloquiums Wien 4 (1963), 2–3.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1983 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Knuth, D.E., Bendix, P.B. (1983). Simple Word Problems in Universal Algebras. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive