A residuated lattice
is an algebra `bfL=<<(L,vv,^^,*,e,\,/)>>` such that `<<(L,vv,^^)>>` is a
lattice, `<<(L,*,e)>>` is a monoid, and for all `x,y,z in L`
We usually write `x*y` as `x.y` and use the convention that,
in the absence of parentheses,
`*` is performed first, followed by `\,/` and then `vv, ^^`.
The class RL of all residuated lattices is a variety.
An equational basis is given by the monoid and lattice identities together
with, for instance,
`x\(y ^^ z) = x\y ^^ x\z` `(x ^^ y)/z = x/z ^^ y/z`
`x <= x.y/y` `(x/y).y <= x`
`y <= x\x.y` `x.(x\y) <= y`.
The subvariety of all integral residuated lattices
is defined by the identity `x^^e=x` and is denoted by IRL.
CRL is the variety of commutative residuated lattices.
Whitman's solution to the word problem is extended to residuated
lattices by adding the following Gentzen rules (with associativity
of `*` assumed in the application):
Okada and Terui (JSL 1999) proved this result in logical form for
(non)commutative propositional intuitionistic linear logic.
Theorem: The variety of residuated lattices has a decidable
Proof: Click here