Negative Subgoals with Free Variables

Prolog systems currently work with the restriction that negative subgoals not contain free variables, although some authors have suggested that this restriction can be lifted by running the theorem prover to exhaustion on the subgoal being considered. We suggest that this approach is likely not to be computationally viable in practice, and describe and formalize a new approach to dealing with quantified default queries that avoids this difficulty. 1 Introduction Consider the following prolog fragment: 1 f :- not(g(x)). g(A). The interpretation we will assign to the implication f :- not(g(x)) will be that it is universally quantified over x, and therefore corresponds to the implication 8x:[:g(x) oe f ] (1) or, equivalently, [9x::g(x)] oe f: Given this interpretation, what should the response be if we provide the system with the query f? 2 Intuitively, we would expect the query to succeed, since f follows from any negative instance of g, and the only known positive instance of g is..