A Completion Procedure for Conditional Equations
The paper presents a new completion procedure for conditional equations. The work is based on the notion of reductive conditional rewriting. The procedure has been designed to also handle nonreductive equations that are generated during completion. The paper in particular presents techniques for simplification of conditional equations and rules, so that the procedure terminates on more specifications. The correctness proofs which form a substantial part of this paper employ recursive path orderings on proof trees, an extension of the ideas of Bachmair, Dershowitz and Hsiang to the conditional case.