Evaluation of queries under closed-world assumption

The minimal entailment proves (Min) has been characterized elsewhere by P proves (Min) phi iff Cn (P boolean OR {phi}) boolean AND P os subset of or equal to Cn(P), where Cn is the first-order consequence operation, P is a set of clauses (indefinite deductive data base; in short: a data base), phi is a clause (a query), and P os is the set of positive (that is, bodiless) ground clauses. In this paper, we address the problem of the computational feasibility of criterion (1). Our objective is to find a query evaluation algorithm that decides P proves (Min) phi by what we call indefinite modeling, without actually computing all ground positive consequences of P and P boolean OR {phi}. For this purpose, we introduce the concept of minimal indefinite Herbrand model M-P of P, which is defined as the set of subsumption-minimal ground positive clauses provable from P. The algorithm first computes M-P by finding the least fixed-point of an indefinite, consequence operator mu T-P(I). Next, the algorithm verifies whether every ground positive clause derivable from M-P boolean OR {phi} by one application of the parallel positive resolution rule (in short: the PPR rule) is subsumed by an element of M-P. We prove that the PPR rule, which can derive only positive clauses, is positively complete, that is, every positive clause provable from a data base P is derivable from P by means of subsumption and finitely many applications of PFR. From this we conclude that the presented algorithm is partially correct and that it eventually halts if both P and M-P are finite. Moreover, we indicate how the algorithm can be modified to handle data bases with infinite indefinite Herbrand models. This modification leads to a concept of universal model that allows for nonground clauses in its Herbrand base and appears to be a good candidate for representation of indefinite deductive data bases.