Evaluation of queries under closed-world assumption. Part II: The hierarchical case
This paper constitutes the second part of a paper published in the Journal of Automated Reasoning 18 (1997), 357-398. The minimal entailment proves (Min) has been characterized elsewhere by P proves (Min) phi iff Cn(P boolean OR{phi}) boolean AND G P-os subset of or equal to Cn(P) (1) where Cn is the first-order consequence operation, P is a set of clauses (disjunctive logic program; in short: a program), phi is a clause (a query), and G Pos is the set of positive (that is, bodiless) ground clauses. In this part, we address the problem of computational feasibility of certain iterative applications of criterion (1). In the first part of the paper we proposed a query evaluation algorithm that decided P proves (Min) phi by what we called indefinite modeling. The query evaluation algorithm was capable of deciding the right-hand side of (1) without actually computing all ground positive consequences of P or P boolean OR{phi}. The objective of the second part of the paper is to extend the proposed approach so that it properly captures phenomena associated with allowing negation in clauses' bodies, however, at a price of substantial complication (in particular, computing all ground positive consequences of P boolean OR{phi} that are not consequences of P can no longer be avoided). For that purpose, we introduce the concepts of a layered program and its hierarchically minimal semantics, a special case of which covers stratified programs with semantics defined by second-order prioritized circumscription and, in the case of definite programs, perfect models. We characterize the hierarchically minimal entailment proves (HMin) in terms of iterative application of the right-hand side of criterion (1). Finally, we generalize the indefinite modeling and query evaluation algorithms presented in Part I over the layered programs, and indicate their computational advantages relative to other methods (e.g., those based on prefect model semantics). The presented approach does not require assigning different meanings to logically equivalent clauses, so it actually eliminates the need for program clauses with negation in their bodies.
closed-world assumption disjunctive logic programs negation in clauses' bodies prioritized circumscription indefinite deductive data bases indefinite herbrand models minimal-model theory perfect model semantics stratified logic programs