An efficient computation of the extended generalized closed world assumption by support-for-negation sets

Abstract

Closed world assumptions are one of the major approaches for non-monotonic reasoning in artificial intelligence. In [16] this formalism is applied to disjunctive logic programs, i.e. logic programs with positive disjunctive rule heads and positive atoms in the rule bodies. The disjunctive closure operator $\mathcal{T}_P^S$ allows for the derivation of the set $\mathcal{M}\mathcal{S}_P$ of all positive disjunctive clauses logically implied by the program P, the minimal model state. On the other hand, disjunctive clauses over negated atoms are derived in the extended generalized closed world assumption $\mathcal{E}\mathcal{G}\mathcal{C}\mathcal{W}\mathcal{A}_P$. Such a clause is the negation of a conjunction of positive atoms. $\mathcal{E}\mathcal{G}\mathcal{C}\mathcal{W}\mathcal{A}_P$ contains all conjunctions which are false in all minimal Herbrand models of the program.

We present efficient δ-iteration techniques for computing the closed world assumption $\mathcal{E}\mathcal{G}\mathcal{C}\mathcal{W}\mathcal{A}_P$ based on an iterative computation of the set of all support-for-negation sets SN(C) for conjunctions C, i.e. certain sets of clauses which characterize $\mathcal{E}\mathcal{G}\mathcal{C}\mathcal{W}\mathcal{A}_P :C \varepsilon \mathcal{E}\mathcal{G}\mathcal{C}\mathcal{W}\mathcal{A}_P$ iff $\mathcal{M}\mathcal{S}_P \vDash SN(C)$. The support-for-negation sets SN(A) for atoms A are easily derived from the minimal model state $\mathcal{M}\mathcal{S}_P$. We will propose a bottom-up computation deriving the support-for-negation sets of longer conjunctions from shorter ones based on an algebraic formula given by [16]: SN(C₁ ∧ C₂) = SN(C₁) ∀ SN(C₂). We will present techniques for the efficient computation of these disjunctions of two clause sets and a δ-iteration approach for computing the support-for-negation sets of a sequence of growing minimal model states.

For disjunctive normal logic programs, i.e. logic programs with positive disjunctive rule heads and — possibly — negated atoms in the rule bodies, these operators form a basis for computing the generalized disjunctive well-founded semantics.