On negation as instantiation

Abstract

Given a logic program P and a goal G, we introduce a notion which states when an SLD-tree for P U {G} instantiates a set of variables V with respect to another one, W. We call this notion weak instantiation, as it is a generalization of the instantiation property introduced in [3]. 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 Ǝ¬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 ∀wƎѵ¬Qand of the form ∀wƎѵ∀z¬Q, where Z is the set of the remaining variables of Q.