Conditional Rewrite Systems

Conditional term rewriting systems naturally come into play in the algebraic specification of abstract data types. The specification by positive conditional equations is not only more natural but also more expressive; see [BM84, BN98]. Papers like Kaplan [Kap84] and Bergstra and Klop [BK86] are mainly motivated by this point of view. Now, conditional term rewriting plays a fundamental role in the integration of functional and logic programming; see Hanus [Han94] for an overview of this field. Moreover, it should not be forgotten that conditional systems have been used as a proof-theoretic tool for establishing properties of unconditional term rewriting systems as well as λ-calculus extensions; for an overview, see Klop and de Vrijer [KV90].