Order-sorted completion: The many-sorted way (Q1177935)

The author improves previous results about the relation between order- sorted and many-sorted rewriting. In particular it has been shown that one step of order-sorted rewriting with a set of rules \(R\) is one step of many-sorted rewriting with the lowest parse of the sort specialization \(R/s/\) of \(R\) modulo the axioms \(LP\) of the lowest parse. This result also holds in the presence of non-sort-decreasing rules. It has been shown that in many practical cases non-sort decreasing rules can be replaced by sort decreasing ones without changing the initial algebra. An unfailing completion procedure for conditional equations that can handle both non-reductive equations and quasi-reductive equations is described.