Term Rewrite Systems for Lattice Theory
It is shown that, even though there is a very well-behaved, natural normal form for lattice theory, there is no finite, convergent AC term rewrite system for the equational theory of all lattices.