Residuated Lattice Inequations Quiz
The randomly generated
(in)equations below are in the language of (bounded) residuated lattices. Specifically,
the language used here has
- constant symbols:
- binary operation symbols:
- binary predicate symbols:
Recall that a residuated lattice is of the form
where
is a lattice,
is a monoid, and for all
T is the top element of the lattice, 0 is the bottom element, and 1 is the unit
with respect to the monoid operation *.
Decide if the following inequations are true in the theory of bounded 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