On sufficient-completeness and related properties of term rewriting systems (Q1077161)

The decidability of the sufficient-completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible with respect to the term rewriting system under consideration. These results are first shown for untyped systems and are subsequently extended to typed systems.