Evaluation of queries under closed-world assumption (Q1367075)

This paper deals with the problem of computational feasibility of a criterion for minimal entailment in an indefinite deductive data base \(P\) with a set of ground clauses and a given first-order consequence operation. The goal is to find an algorithm deciding a formula \(P\lvdash_{\text{Min}}\varphi\), for an arbitrary clause \(\varphi\), without actually computing all ground positive consequences of \(P\) and \(P\cup\{\varphi\}\). To construct the algorithm a concept of minimal indefinite Herbrand model for \(P\) is introduced as the set of subsumption minimal ground positive clauses provable from \(P\). The algorithm first computes the Herbrand model \({\mathfrak M}_P\) and then it verifies whether every such clause derivable from \({\mathfrak M}_P\cup \{\varphi\}\) by one application of the parallel positive resolution (PPR) rule is subsumed by an element of \({\mathfrak M}_P\). It is proved that the PPR rule, which derives only positive clauses, is positively complete. From this it is concluded that the algorithm is partially correct and eventually halts if both \(P\) and \({\mathfrak M}_P\) are finite. A modification of the algorithm when handling data bases with infinite Herbrand models, leads to a concept of a universal model, which appears to be a good candidate for representation of indefinite deductive data bases.