On Negation as Instantiation

Given a logic program P and a goal G, we introduce a notion which states when an SLD-tree for P [ fGg instantiates a set of variables V with respect to another one, W . We call this notion weak instantiation, as it is a generalisation of the instantiation property introduced by Di Pierro, Martelli and Palamidessi. A negation rule based on instantiation, the so-called Negation As Instantiation rule (NAI), allows for inferring existentially closed negative queries, that is formulas of the form 9:Q, from logic programs. We show that, by using the new notion, we can infer a larger class of negative queries, namely the class of the queries of the form 8W 9 V :Q and of the form 8W 9 V 8Z :Q, where Z is the set of the remaining variables of Q. 1 Introduction In order to infer negative literals from a logic program, Clark [2] introduced the Negation As Failure (NAF) rule and defined its declarative semantics in terms of the completion, Comp(P ), of a program P . However, this rule allows..