## Compatibility of order-sorted rewrite rules

**Uwe Waldmann**
In Stéphane Kaplan and Mitsuhiro Okada, editors, *Conditional
and Typed Rewriting Systems, 2nd International Workshop*, LNCS 516,
pages 407-416, Montreal, Canada, June 11-14, 1990. Springer-Verlag.

**Abstract:**
Unlike in the unsorted case the application of an order-sorted rewrite
rule to a term *t* may be prohibited although the left hand side of
the rule matches with a subterm of *t*, since the resulting term
would be ill-formed. A rewrite rule is called compatible, if it may be
applied to a term, whenever its left hand side matches with a subterm.
We show that compatibility in finite signatures is decidable.

Previous |

Up |

Next

Uwe Waldmann
<

uwe@mpi-inf.mpg.de>,
1997-10-02.