###
A Gentzen system for (residuated) Kleene algebras and lattices

The residuated lattice part of 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 Kleene * axioms and rules are from the article

P. Jipsen,
*
From semirings to residuated Kleene lattices*, Studia Logica
**76**(2) (2004), 291-303.

Note: Wojciech Buszkowski, *On Action Logic*, Journal of Logic and Computation,
(2006) shows that the system implemented here is not complete without
the cut rule.

The (in)equations are in the language of residuated Kleene lattices.
Specifically, the language used here has

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

Enter your own (in)equation
Standard equational results about residuated Kleene lattices

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