Is there a finite term-rewriting system of some kind for free lattices?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Is there a finite term-rewriting system of some kind for free lattices?

Recorded progress.

As mentioned in a remark to RTALooP entry trs-lattices, it has been shown in [Pedersen, 1991] that there is no finite, normal form, associative-commutative term-rewriting system for lattices.

Recorded update.

Submitted by Jordi Levy on Fri Apr 17 20:20:41 MET DST 1998.

There are bi-rewriting systems for free lattices and distributive free lattices [Pedersen, 1991]. Bi-rewriting systems are used to automatize deduction in theories with monotonic order relations. They are composed of a pair of rewriting systems. One is used for rewriting terms into smaller terms, and the other for rewriting terms into bigger terms.