SLDNF-resolution with equality (Q1189731)

Logic programs with equality are considered. The objective is to extend the results of \textit{J. Jaffar}, \textit{J. Lassez} and \textit{M. J. Maher} [J. Logic Program. 1, 211-223 (1984; Zbl 0584.68021)] for definite clause programs to normal programs, where negative as well as positive literals are allowed in the bodies of clauses. An appropriate version of SLDNF-resolution is defined and the analogue of Clark's fundamental theorem is proved (that if a query succeeds it is a consequence of the completion of the program, and if it fails then its negation is a consequence).