[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #32

Originator: John Pedersen
Date: April 1991

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

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

Remark

As mentioned in a remark to Problem #77, it has been shown in [Fre93] that there is no finite, normal form, associative-commutative term-rewriting system for lattices.

Comment sent by Jordi Levy

Date: Fri Apr 17 20:20:41 MET DST 1998

There are bi-rewriting systems for free lattices and distributive free lattices [LA96]. 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.

References

[Fre93]

R. Freese. personal communication, 1993.

[LA96]

Jordi Levy and Jaume Agustí. Bi-rewriting systems. Journal of Symbolic Computation, 22(3):279–314, September 1996.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]