Negation as instantiation

We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called "Negation As Instantiation" (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. The set of the atoms whose negation is inferred by the NAI rule is proved equivalent to the complement of T_c ↓ ω, where T_c is the immediate consequence operator extended to non-ground atoms (M. Falaschi et al., 1989, Theoret. Comput, Sci.69(3), 289-318). The NAI rule subsumes negation as failure on ground atoms, it excludes floundering, and can be efficiently implemented, We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness.