Canonical Conditional Rewrite Systems Containing
       Extra Variables

Juergen Avenhaus, Carlos Loria-Saenz.
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, W-6750 Kaiserslautern, GERMANY
E-mail: {avenhaus, loria}@uni-kl.de

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
$\to_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.
$\stackrel{*}{\longleftrightarrow}_R \; = \; =_R$
holds.
We apply our results to prove Horn
clause programs to be uniquely terminating.

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1993/papers/
file: Avenhaus.SR-93-03.english.ps.Z