###
Deciding Equations in Residuated Lattices

The algorithm implemented here is due to Okada and Terui, JSL 64(2), 1999. A version
of this algorithm for residuated lattices is described in the preprint
A Gentzen systems and decidability for residuated lattices
(P. Jipsen, Jan 2000)
pdf version
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:

Click here if you want to enter your own (in)equation.
A list of standard equational results about residuated lattices can be viewed
on this page.

Test yourself by deciding the following
randomly generated RL equations.

The JavaScript code is available for browsing.

####
Here is the list of residuated lattice equations, followed by their
Gentzen system proofs (generated by the embedded JavaScript program)

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. With a bit of practice, these
proofs are actually easier to read (and write) than the standard tree-like presentation.
The symbol !- can be interpreted as *not less or equal*, in which case
each line implies the one below it (if at the same indentation level) or one
of the two indented alternatives (in the case of a branching rule). With this
interpretation, the terminal nodes represent contradictions, reminiscent of
a tableau style proof.