Sciweavers

Share
RTA
1993
Springer

Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations

9 years 1 months ago
Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations
We propose an extension of rewriting techniques to derive inclusion relations a ⊆ b between terms built from monotonic operators. Instead of using only a rewriting relation ⊆ −→ and rewriting a to b, we use another rewriting relation ⊇ −→ as well and seek a common expression c such that a ⊆ −→ ∗ c and b ⊇ −→ ∗ c. Each component of the bi-rewriting system ⊆ −→, ⊇ −→ is allowed to be a subset of the corresponding inclusion ⊆ or ⊇. In order to assure the decidability and completeness of the proof procedure we study the commutativity of ⊆ −→ and ⊇ −→. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. We present the canonical bi-rewriting system corresponding to the theory of non-distributive lattices.
Jordi Levy, Jaume Agustí-Cullell
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1993
Where RTA
Authors Jordi Levy, Jaume Agustí-Cullell
Comments (0)
books