###
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

- constant symbols:
- binary operation symbols:
- binary predicate symbols:
- variables:

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)