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 Tc↓ ω, where Tcis 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.