Incorporating equality into the unification process has added great power to automated theorem provers. We see a similar trend in logic programming where a number of languages are proposed with specialized or extended unification algorithms. There is a need to give a logical basis to these languages. We present here a general framework for logic programming with definite clauses, equality theories, and generalized unification. The classic results for definite clause logic programs are extended in a simple and natural manner. The extension of the soundness and completeness of the negation-as-failure rule for complete logic programs is conceptually more delicate and represents the main result of this paper. © 1984.
Jaffar, J., Lassez, J. L., & Maher, M. J. (1984). A theory of complete logic programs with equality. The Journal of Logic Programming, 1(3), 211–223. https://doi.org/10.1016/0743-1066(84)90010-4