SLDNF-resolution with equality (Q1189731)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 57769
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | SLDNF-resolution with equality |
scientific article; zbMATH DE number 57769 |
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
0.8729815483093262
0 references
0.8486906886100769
0 references
0.8459284901618958
0 references
0.8337617516517639
0 references
