Order-sorted rewriting builds a nice framework to handle partially defined functions and subtypes (see [Smolka & al 87]). In the previous works about order-sorted rewriting the term rewriting system needs to be sort decreasing in order to be able to prove a critical pair lemma and Birkhoff's completeness theorem. However, this approach is too restrictive.
Therefore, we generalize well-sorted terms to semantically well-sorted terms and well-sorted substitutions to some kind of semantically wellsorted substitutions. Semantically well-sorted terms with respect to a set of equations E are terms that denote well-defined elements in every algebra satisfying E.
We prove a critical pair lemma and Birkhoff's completeness theorem for so-called range unique signatures and arbitrary order-sorted rewriting systems. A transformation is given which allows to obtain an equivalent range unique signature from each non-range-unique one. We also show some decidability results.
This work was supported by the Deutsche Forschungsgemeinschaft as part of the SFB 314.