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.