A New Procedural Interpretation of Horn Clauses with Equality
LEON S. STERLING · 1995
We introduce the equality elimination method which is a new procedure for dealing with Horn clause logic programs with equality. The method combines SLD-resolution with a bottom-up equation solving. By solving equations, we try to transform a logic program with equality to a logic program without equality. The transformation uses basic superposition as the main operation. We prove soundness and completeness of the equality elimination method. We also show that approaches based on complete sets of E-unifiers are not satisfying. In particular, we provide a negative solution to the open problem of completeness of SLDE+-reso1ution.