Canonical Conditional Rewrite Systems Containing Extra Variables

Abstract

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.