Deciding Equations in Residuated Lattices
The algorithm implemented here is from Okada and Terui, JSL 64(2), 1999, but
the Gentzen system and decidability are originally due to Ono and Komori,
JSL 50(1), 1985.
An algebraic version
of this algorithm for residuated lattices is described in the article
P. Jipsen and C. Tsinakis,
A Survey of Residuated Lattices, in "Ordered
Algebraic Structures" (J. Martinez, editor), Kluwer Academic Publishers,
Dordrecht, 2002, 19-56.
The (in)equations are in the language of (bounded) residuated lattices. Specifically,
the language used here has
- constant symbols:
- binary operation symbols:
- binary predicate symbols:
Talk given at the l-groups and f-rings
conference, University of Florida, Feb 28-Mar 03, 2001
Enter your own (in)equation
Standard equational results about residuated lattices can be viewed
Test yourself by deciding
randomly generated RL equations.
Here is the list of residuated lattice equations, followed by their
To display the proofs in a linear fashion, rather than the more usual Gentzen style,
the proof trees are displayed from the root downwards, with the depth of nodes indicated
by the indentation level. (Only the branching rules increase the indentation depth.)
Each sequent is labeled by the name of the rule that produced it. When a terminal
node is reached, the indentation level decreases again.