ON NEGATION AS INSTANTIATION
 
Alessandra Di Pierro, W{\l}odzimierz Drabent

Given a logic program  $P$  and a goal  $G$,  we introduce a notion which
states when an SLD-tree for  $P\cup\{G\}$  instantiates a set of variables
$V$  with respect to another one,  $W$.  We call this notion {\em weak
instantiation}, as it is a generalization of the instantiation property
introduced in \cite{DMP95}.  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
$\exists\neg 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  $\forall_W\exists_V\neg Q$  and of the form
$\forall_W\exists_V\forall_Z\neg Q$,  where  $Z$  is the set of the
remaining variables of  $Q$.