[Back]

F. Schernhammer, B. Gramlich:
"On Proving and Characterizing Operational Termination of Deterministic Conditional Rewrite Systems";
2007; 14 pages.

We define the notion of context-sensitive quasi-reductivity which implies operational termination of deterministic conditional term rewriting systems. Furthermore, we show how existing transformations from such systems into unconditional ones can be used (with slight modifications) to prove context-sensitive quasi-reductivity. Finally, we give a few equivalent characterizations of this notion.

Conditional term rewriting systems (CTRSs), deterministic CTRSs, operational termination, quasi-reductivity, context-sensitivity, elimination of conditions.