Canonical Conditional Rewrite Systems Containing Extra Variables
Jürgen Avenhaus, Carlos Lorı́a-Sáenz · 1993
We study deterministic conditional rewrite systems, i.e. conditional rewrite systems where the extra variables are not totally free but 'input bounded'. If such a system R is quasi-reductive then !R is decidable and terminating. We develop a critical pair criterion to prove confluence if R is quasi-reductive and strongly deterministic. In this case we prove that R is logical, i.e. /!R = =R holds. We apply our results to prove Horn clause programs to be uniquely terminating.