We consider the problem of verifying confluence and termination of conditional term rewriting systems. Recently we have obtained some interesting results for unconditional term rewriting systems (TRSs) which are non-overlapping or, more generally, locally confluent overlay systems. These results provide sufficient criteria for termination plus confluence in terms of restricted termination and confluence properties (Gramlich 1994a). 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 (CTRS) which is an innermost terminating overlay system such that all (conditional) critical pairs are joinable is complete, Le., terminating and confluent.
CITATION STYLE
Gramlich, B. (1995). On termination:And confluence of conditional rewrite systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 968, pp. 166–185). Springer Verlag. https://doi.org/10.1007/3-540-60381-6_10
Mendeley helps you to discover research relevant for your work.