SLDNF-resolution with equality (Q1189731)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | SLDNF-resolution with equality |
scientific article |
Statements
SLDNF-resolution with equality (English)
0 references
27 September 1992
0 references
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).
0 references
\(E\)-unification
0 references
completion
0 references
negation as failure
0 references
Logic programs with equality
0 references
SLDNF-resolution
0 references