###
Deciding Equations in Generalized MV-algebras

Peter Jipsen,
Chapman University
The algorithm implemented here uses a translation, due to
N. Galatos
(see his forthcoming dissertation), to the decision
procedure for lattice-ordered groups.
The algorithm for deciding equations in
l-groups 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.

The (in)equations are in the language of 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 (i.e. X=e/x=x\e).

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.)

The JavaScript code
is available for browsing.

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