Canonical conditional rewrite systems.

*(English)*Zbl 0667.68043
Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 538-549 (1988).

[For the entire collection see Zbl 0638.00038.]

Conditional rewrite (CR) rule R has the form \(s_ 1=t_ 1 \&...\& s_ n=t_ n\to s=t\). It allows to replace \(s\sigma\) by \(t\sigma\) if the substitution \(\sigma\) satisfies all equations \(s_ i=t_ i\). Various defintions of satisfaction determine various notions of CR. The authors consider seven such notions, the most important being join systems, where it is required, that \(s_ i\sigma\) and \(t_ i\sigma\) be joinable, i.e., reducible to one and the same term. Sufficient conditions for confluence, mainly in terms of Knuth-Bendix critical pairs and good control of the convergence Noetherian property of rewriting, are established. The Noetherian property (together with some others) usually guarantees the coincidence of the rewrite equality (t and s can be rewritten into one and the same term) with the deducibility of \(t=s\) in the predicate calculus with equality from the implications expressing rewrite rules. A CR system is decreasing if there exists a well-founded extension \(>\) of the proper subterm relation to all pairs of terms, containing the reducibility relation, and satisfying for any CR rule R and any substitution \(\sigma\) such that s;\(\sigma\) nd \(t_ i\sigma\) are joinable, the condition \(s\sigma >s_ 1\sigma,...,t_ n\sigma\). In decreasing CR systems main basic properties (one step reducibility, joinability, irreducibility etc.) are decidable, they are canonical (under natural conditions) and contain other classes with the Noetherian property.

Conditional rewrite (CR) rule R has the form \(s_ 1=t_ 1 \&...\& s_ n=t_ n\to s=t\). It allows to replace \(s\sigma\) by \(t\sigma\) if the substitution \(\sigma\) satisfies all equations \(s_ i=t_ i\). Various defintions of satisfaction determine various notions of CR. The authors consider seven such notions, the most important being join systems, where it is required, that \(s_ i\sigma\) and \(t_ i\sigma\) be joinable, i.e., reducible to one and the same term. Sufficient conditions for confluence, mainly in terms of Knuth-Bendix critical pairs and good control of the convergence Noetherian property of rewriting, are established. The Noetherian property (together with some others) usually guarantees the coincidence of the rewrite equality (t and s can be rewritten into one and the same term) with the deducibility of \(t=s\) in the predicate calculus with equality from the implications expressing rewrite rules. A CR system is decreasing if there exists a well-founded extension \(>\) of the proper subterm relation to all pairs of terms, containing the reducibility relation, and satisfying for any CR rule R and any substitution \(\sigma\) such that s;\(\sigma\) nd \(t_ i\sigma\) are joinable, the condition \(s\sigma >s_ 1\sigma,...,t_ n\sigma\). In decreasing CR systems main basic properties (one step reducibility, joinability, irreducibility etc.) are decidable, they are canonical (under natural conditions) and contain other classes with the Noetherian property.

Reviewer: G.Mints

##### MSC:

68Q65 | Abstract data types; algebraic specification |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |