New Abstract Criteria for Termination and Confluence
of Conditional Rewrite Systems

Bernhard Gramlich
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, D-67653 Kaiserslautern, Germany
E-mail: gramlich@informatik.uni-kl.de

Abstract
We consider the problem of verifying confluence and
termination of conditional term rewriting systems (TRSs).
For unconditional TRSs the critical pair lemma holds
which enables a finite test for confluence of (finite)
terminating systems. And for ensuring termination of
unconditional TRSs a couple of methods for constructing
appropiate well-founded term orderings are known.
If however termination is not guaranteed then proving
confluence is much more difficult. Recently we have
obtained some interesting results for unconditional TRSs
which provide sufficient criteria for termination plus
confluence in terms of restricted termination and
confluence properties. In particular, we have shown that
any innermost terminating and locally confluent overlay
system is complete, i.e.  terminating and confluent.
Here we generalize our approach to the conditional case
and show how to solve the additional complications due
to the presence of conditions in the rules. Our main
result can be stated as follows: Any conditional TRS
which is an innermost terminating semantical overlay
system such that all (conditional) critical pairs are
joinable is complete.


Keywords
conditional term rewriting systems, overlay systems,
confluence, termination, weak termination, innermost
termination

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