Deciding Equations in Lattice-ordered Groups

Peter Jipsen, Chapman University

The algorithm implemented here is due to W. C. Holland and S. H. McCleary, Solvability of the word problem in free lattice-ordered groups, Houston Journal of mathematics, 5(1), (1979) p. 99--105.

With a simple translation, the same algorithm can be used to decide the equational theory of the variety of negative cones of l-groups.

Recently N. Galatos discovered a further translation that gives a decision procedure for integral generalized MV-algebras. He also shows that an equation holds for all generalized MV-algebras iff it holds for integral generalized MV-algebras and for l-groups.

The (in)equations are in the language of l-groups (or residuated lattices). Specifically, the language used here has

The uppercase variables denote the inverses of the corresponding lowercase variables.

Enter your own (in)equation and check if it holds in the varieties LG, LG-, IGMV, and GMV. (An (in)equation holds in GMV iff it holds in LG and IGMV.)

Test yourself by deciding randomly generated l-group equations.

The JavaScript code is available for browsing.

Here is a list of l-group equations, followed by their arrow-diagram proofs (generated by the embedded JavaScript program)