Deciding Equations in Generalized MV-algebras

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.

Deciding Equations in Generalized MV-algebras

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