Oriented Equational Logic Programming is Complete

We show the completeness of an extension of SLD resolution to the equational setting. This proves a conjecture of Laurent Fribourg and shows the completeness of an implementation of his. It is the first completeness result for superposition of equational Horn clauses which reduces to SLD resolution in the nonequational case. The inference system proved complete is actually more general than the one of Fribourg, because it allows for a selection rule on program clauses. Our completeness result also has implications for Conditional Narrowing and Basic Conditional Narrowing