Simplifying conditional term rewriting systems: Unification, termination and confluence (Q1100891)

In the field of conditional term rewriting systems, the reduction of a given term involves recursive reduction of the premises of the rule currently applied, which leads to intractability. In this paper, we introduce simplifying systems, that allow to control this recursivity. Our approach enables the extension of several results for non-conditional rewriting to the conditional framework. In particular, we obtain results about the correctness of evaluation procedures, unification in conditional theories, termination and confluence, together with Knuth- Bendix theorem proving methods. Finally, the extension of such results to fully general conditional systems is discussed.