SLDNF resolution with non-safe rule and fixpoint semantics for general logic programs

AbstractThe SLDNF resolution (SLD resolution with negation as failure) is often restricted to yield a safe rule, that is, negation as failure rule is adopted only in the case that the selected negative literal in each goal should be in ground. In this paper we investigate extensions of goals in SLDNF resolutions with the case of selecting non-ground negative literals. Since Shepherdson's proposal is thought of as most general [16, 18] we formally show how the success and failure sets by Sherpherdson's SLDNFS resolution are related with a fixpoint semantics, which is generalized to be concerned with atom sets involving the variables