UFL Talk

<a href=index.html>Decision procedure for RL equations</a>
(take the quiz) (Note: during the talk one of the random quiz questions
was to decide if `(0^^0)/x<=y vv z` holds in all residuated lattices,
and the algorithm answered no. At the time I thought this was an error
of the implementation, but of course the only error was my incorrect
mental calculation that `0/x=0`. When `x=0`, we have `0/0=T`.)

Compare the decidability of residuated lattices with two important 
results about l-groups:

Theorem (C. Holland and S.H. McCleary 1979): 
The variety of l-groups has a decidable 
equational theory.

Theorem (A.M.W. Glass and Y. Gurevich 1983): 
The (local) word problem for l-groups is undecidable,
i.e. there exists a finitely presented l-group
(with one relator) for which there is no algorithm that
decides if two words are representatives of the same
element.

Corollary:
The quasi-equational theory of l-groups is undecidable.

This is also refered to as the undecidability of the global 
(or uniform) word problem.

The same theorem holds for semigroups 
(E. Post ~'40) and groups (Novikov, W. Boone 1959)

Theorem (N. G. Khisamiew 1966): The universal theory
of abelian l-groups is decidable.

If a class is closed under finite products, then any universal
formula is equivalent to a finite number of 
disjunction of quasi-identities
and negated equations.

Hence such a class has a decidable universal theory iff it has
a decidable quasi-equational theory.

Theorem (V. Weispfenning 1986): The universal theory of
abelian l-groups is co-NP-complete.

Theorem (Y. Gurevich 1967): The first-order theory of
abelian l-groups is hereditarily undecidable. (S. Burris
1985 gives a short proof).

What about the quasi-equational theory of residuated
lattices?

<center><a href=ufltalk1.htm>Next</a>