[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?
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.
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.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |