Negation as instantiation: A new rule for the treatment of negation in logic programming

Negation as failure is sound both for the closed world assumption, CWA, and the Clark's completion, Comp(W) of a program W. Anyway, there is no semantics for which it is also complete for all programs and queries, as non-ground negative literals cannot be dealt with, and cause floundering. We define a new negation rule, for which floundering is excluded and we give a semantics Comp(W)* for which the new rule is both sound and complete. This semantics is a weak version of Comp(W) obtained by enlarging as much as possible the free interpretation of variables and functions given by Herbrand-interpretations. We have called the proposed negation rule the Negation As Instantiation rule (NAI rule) because an atom is considered negated, though some of its derivations do not finitely fail, provided that some of its variables get instantiated. The NAI rule subsume negation as failure and can be efficiently implemented. A set FFI (Failure by Finite Instantiation) is defined which is proved equivalent to the complement of T_c↓ω with respect to the set of all atoms, where T_c is the immediate consequence operator extended to deal with interpretations that contain atoms with variables (the C-semantics in [6]).