Conditional rewrite rules (Q1065790)

The purpose of this paper is to develop a general study of conditional equational theories. A system of conditional equations is defined simply as a finite set of equational Horn clauses. It is shown that from an algebraic point of view these systems give rise to results analogous to those for classical equational theories. Unfortunately, for the related conditional rewriting systems the rewriting problem is unsolvable and the normal form function is uncomputable. Besides its intrinsic beauty such a general model may become a valuable tool for a ''top down'' search of decidability thresholds.