While the stable model semantics, in the form of Answer Set Programming, has become a successful semantics for disjunctive logic programs, a corresponding satisfactory extension of the well-founded semantics to disjunctive programs remains to be found. The many current proposals for such an extension are so diverse, that even a systematic comparison between them is a challenging task. In order to aid the quest for suitable disjunctive well-founded semantics, we present a systematic approach to a comparison based on level mappings, a recently introduced framework for characterizing logic programming semantics, which was quite successfully used for comparing the major semantics for normal logic programs. We extend this framework to disjunctive logic programs, which will allow us to gain comparative insights into their different handling of negation. Additionally, we show some of the problems occurring when trying to handle minimal models (and thus disjunctive stable models) within the framework.
Two semantics are nowadays considered to be the most important ones for
normal logic programs. Stable model semantics [
Even a comparison of existing proposals is difficult due to the large
variety of completely different constructions on which these semantics are based. In
[
In order to allow for easier comparison of different semantics, a methodology
has recently been proposed for uniformly characterizing semantics by means of
level mappings, which allow for describing syntactic and semantic dependencies
in logic programs [
In this paper, we attempt to utilize this approach and present level mapping characterizations for the three previously mentioned semantics, namely SWFS, GDWFS and D-WFS. The obtained uniform characterizations will allow us to compare the semantics in a new and more structured way. It turns out, however, that even under the uniform level-mapping characterizations the three semantics differ widely, such that there is simply not enough resemblance between the approaches to obtain a coherent picture. We can thus, basically, only confirm in a more formal way what has been known beforehand, namely that the issue of a good definition of well-founded semantics for disjunctive logic programs remains widely open. We still believe that our approach delivers structural insights which can help to guide the quest.
The paper is structured as follows. In Section 2, basic notions are presented and we recall shortly the well-founded semantics. Then we devote one section to each of the three semantics recalling the approach itself and presenting the level mapping characterization. We start with SWFS in Section 3, continue with GDWFS in Section 4 and end with D-WFS in Section 5. After that, in Section 6 we compare the characterizations looking for common conditions which might be properties for an appropriate well-founded semantics for disjunctive programs, and consider some of the difficulties occurring when applying the framework to minimal models. We conclude with Section 7.
The formal proofs required for the level-mapping characterizations of the
semantics reported in this paper are very involved and technical. Due to space
limitations, it was obviously not possible to include them. They can be found in
the publicly available Technical Report [
A disjunctive logic program Π consists of finitely many universally quantified clauses of the form H1 ∨ · · · ∨ Hl ← A1, . . . , An, ¬B1, . . . , ¬Bm where Hk, Ai, and Bj , for k = 1, . . . , l, i = 1, . . . , n, and j = 1, . . . , m, are atoms of a given first order language, consisting of predicate symbols, function symbols, constants and variables. The symbol ¬ is representing default negation. A clause c can be divided into the head H1 ∨ · · · ∨ Hl and the body A1, . . . , An, ¬B1, · · · , ¬Bm. If the body is empty then c is called a fact. We also abbreviate c by H ← A, ¬B, where H, A and B are sets of pairwise distinct atoms and, likewise, we sometimes handle disjunctions D and conjunctions C as sets. A normal (definite) clause contains exactly one atom in H (no atom in B) and we call a program consisting only of normal (definite) clauses a normal (definite) logic program. We denote normal programs by P to distinguish from disjunctive ones represented by Π. Any expression is called ground if it contains no variables. The Herbrand base BΠ is the set of all ground atoms that can be formed by using the given language from Π. A literal is either a positive literal, respectively an atom, or a negative literal, a negated atom, and usually we denote by A, B, . . . atoms and by L, M, . . . literals. Moreover, a disjunction literal is a disjunction or a negated disjunction. The extended Herbrand base EBΠ (conjunctive Herbrand base CBΠ ) is the set of all disjunctions (conjunctions) that can be formed using pairwise distinct atoms from BΠ . Finally, ground(Π) is the set of all ground instances of clauses in Π with respect to BΠ .
We continue by recalling three-valued semantics based on the truth values true (t), undefined (u), and false (f ). A (partial) three-valued interpretation I of a normal program P is a set A ∪ ¬B, for A, B ⊆ BP and A ∩ B = ∅, where elements in A, B respectively, are t, f , and the remaining wrt. BP are u. The set of three-valued interpretations is denoted by IP,3. Given a three-valued interpretation I, the body of a ground clause H ← L1, . . . , Ln is true in I if and only if Li ∈ I, 1 ≤ i ≤ n, or false in I if and only if Li ∈ I for some i, 1 ≤ i ≤ n. Otherwise the body is undefined. The ground clause H ← body is true in I if and only if the head H is true in I or body is false in I or body is undefined and H is not false in I. Moreover, I is a three-valued model for P if and only if all clauses in ground(P ) are true in I. The knowledge ordering is recalled which, given two three-valued interpretations I1 and I2, is defined as I1 ≤k I2 if and only if I1 ⊆ I2. For a program P and a three-valued interpretation I ∈ IP,3 an I-partial level mapping for P is a partial mapping l : BP → α with domain dom(l) = {A | A ∈ I or ¬A ∈ I}, where α is some (countable) ordinal. Every such mapping is extended to literals by setting l(¬A) = l(A) for all A ∈ dom(l). Any ordinal α is identified with the set of ordinals β such that α > β. Thus, any mapping f : X → {β | β < α} is represented by f : X → α. Given two ordinals α, β, the lexicographic order (α × β) is also an ordinal with (a, b) ≥ (a′, b′) if and only if a > a′ or a = a′ and b ≥ b′ for all (a, b), (a′, b′) ∈ α × β. This order can be split into its components, namely (a, b) >1 (a′, b′) if and only if a > a′ for all (a, b), (a′, b′) ∈ α × β and (a, b) ≥2 (a′, b′) if and only if a = a′ and b ≥ b′ for all (a, b), (a′, b′) ∈ α × β. Additionally we allow the order ≻ which given an ordinal (α × β) is defined as (a, b) ≻ (a′, b′) if and only if b > b′ for all (a, b), (a′, b′) ∈ (α × β).
We shortly recall the level mapping characterization of the well-founded
semantics and refer for the original bottom-up operator to [
Definition 2.1. ([
(WFiib) There exists j with Bj ∈ I and l(A) > l(Bj ).
If A ∈ dom(l) satisfies (WFi), then we say that A satisfies (WFi) with respect to I and l, and similarly if A ∈ dom(l) satisfies (WFii).
Theorem 2.1. ([
Example 2.1. Consider the program P = {p ← ¬q; q ← q; r ← ¬p}. We obtain the well-founded model M = {p, ¬q, ¬r} with l(p) = 1, l(q) = 0 and l(r) = 2. Note that, for I = ∅ and arbitrary l, P satisfies (WF) wrt. I and l as well but I is not the greatest such model wrt. ≤k and thus not the well-founded model.
We continue extending some of the previous notions to the disjunctive case. Let I be a set of disjunction literals. The closure of I, cl(I), is the least set I′ with I ⊆ I′ satisfying the following conditions: if D ∈ I′ then D′ ∈ I′ for all D′ with D ⊆ D′, and for all disjunctions D1 and D2, ¬D1 ∈ I′ and ¬D2 ∈ I′ if and only if ¬(D1 ∨ D2) ∈ I′. Then, I is consistent if there is no D ∈ cl(I) with ¬D ∈ cl(I) as well4. A disjunctive three-valued interpretation I of a disjunctive program Π is a consistent set A ∪ ¬B, A, B ⊆ EBΠ , where elements in A are t, elements in B are f , and the remaining wrt. EBΠ are u. The body of a ground clause H ← A, ¬B is true in I if and only if all literals in the body are true in I, or false in I if and only if there is a D such that either D ⊆ A with ¬D ∈ I or D ⊆ B with D ∈ I5. Otherwise the body is undefined. The truth of a ground clause H ← body is identical to normal programs and I is a disjunctive three-valued model of Π if every clause in ground(Π) is true in I. The disjunctive knowledge ordering k is defined as I1 k I2 if and only if I1 ⊆ I2 and the corresponding level mapping is extended as follows.
Definition 2.2. For a disjunctive program Π and a disjunctive interpretation I a disjunctive I-partial level mapping for Π is a partial mapping l : EBΠ → α with domain dom(l) = {D | D ∈ I or ¬D ∈ I}, where α is some (countable) ordinal. Every such mapping is extended to negated disjunctions by setting l(¬D) = l(D) for all D ∈ EBΠ .
Another way of representing disjunctive information are state-pairs A ∪ ¬B,
where A is a subset of EBΠ such that for all D′ if D ∈ A and D ⊆ D′ then
D′ ∈ A, and B is a subset of CBΠ such that for all C′ if C ∈ B and C ⊆ C′
4 Here, a consistent set is not automatically closed, in contrast with the assumption
made in [
Definition 2.3. For a disjunctive program Π and a state-pair I a disjunctive I-partial level mapping for Π is a partial mapping l : (EBΠ ∪ ¬CBΠ ) → α with domain dom(l) = {D | D ∈ I or ¬D ∈ I}, where α is some (countable) ordinal. 3
We start with SWFS which was introduced by Ross [
Consider a ground disjunction D, let I0 = {D} and suppose that I0 ⇐
I1 ⇐ I2 . . ., then I0, I1, I2 . . . is a (strong) derivation sequence for D. An active
(strong) derivation sequence for D is a finite derivation sequence for D whose last
element, also called a basis of D, is either empty or contains only negative literals.
A basis I = {¬l1, . . . , ¬ln} is turned into a disjunction I¯ = l1 ∨ · · · ∨ ln and if I
is empty, denoting t, then I¯ denotes f . Thus, a strong global tree ΓDS for a given
disjunction D ∈ EBΠ contains the root D and its children are all disjunctions of
the form I¯, where I ranges over all bases for D. The strong well-founded model
of a disjunctive program Π is called M WS F (Π) and D ∈ M WS F (Π), i.e. D is true,
if some child of D is false and ¬D ∈ M WS F (Π), i.e. D is false, if every child of
D is true. Otherwise, D is undefined and neither D nor ¬D occur in M WS F (Π).
In [
p ∨ q ← ¬q b ∨ l ← ¬r c ← ¬l, ¬r f ← ¬e
q ← ¬q l ∨ r ← e ← ¬f, c g ← e 6 More precisely, the disjunctive model has to be restricted to (non-disjunctive) literals.
We obtain a sequence {l ∨ r} ⇐ {} and l ∨ r is true as expected. Furthermore, there is a finite sequence in ΓeS , namely {e} ⇐ {¬f, e ∨ c} ⇐ {¬f, ¬l, ¬c} with the only (true) child and e is false. Thus, we have that M WS F (Π) = {l ∨ r, f, ¬b, ¬c, ¬e, ¬g} while p and q remain undefined. Literally, this is only a small part of the model and we might close the model (e.g. ¬(e ∨ g) ∈ M WS F ) for this example, but the strong well-founded is not necessarily closed which does not allow us to add this implicit information in general.
The level mapping framework is based on bottom-up operators and SWFS is a top-down-procedure so we introduced a bottom-up operator on derivation trees defined on Γ S
Π which is the power set of ΓΠS - the set of all strong global trees with respect to Π.
Definition 3.1. Let Π be a disjunctive logic program, M WS F (Π) the strong wellfounded model, and Γ ∈ Γ S
Π . We define: – TΠS (Γ ) = {ΓDS ∈ ΓΠS | ΓDS contains an active strong derivation sequence {D}, I1, . . . , Ir with child C = I¯r and I1 = {D1, . . . , Dn, ¬Dn+1, . . . , ¬Dm} where ¬C ∈ M WS F (Π), ΓCS ∈ Γ if C = {}, ΓDSi ∈ Γ , Di ∈ M WS F , ΓDSj ∈ Γ , ¬Dj ∈ M WS F for all i = 1, . . . , n and j = n + 1, . . . , m} – UΠS (Γ ) = {ΓDS ∈ ΓΠS | for all active strong derivation sequences in ΓDS the corresponding child C is true in M WS F (Π) and ΓCS ∈ Γ }
The information is joined by WΠS (Γ ) = TΠS (Γ ) ∪ UΠS (Γ ) and iterated: WΠS ↑
0 = ∅, WΠS ↑ n + 1 = WΠS (WΠS ↑ n), and WΠS ↑ α = β<α WΠS ↑ β for limit
ordinal α. It was shown in [
(SWFiic) l(D) > l(C).
Theorem 3.1. Let Π be a disjunctive program with strong well-founded model M . Then, in the disjunctive knowledge ordering, M is the greatest model amongst all models I for which there exists a disjunctive I-partial level mapping l for Π such that Π satisfies (SWF) with respect to I and l.
The characterization is obviously more involved than Definition 2.1. In fact, even though it appears that for every true disjunction there are a sequence and a clause satisfying (SWFia), we were unable to show that due to the missing closure property of the strong well-founded model. Thus, we have to keep the condition (SWFib). Moreover, it can be checked that all the cases for negated disjunctions yield that (SWFiic) holds as well. We therefore could have formulated (SWFii) just using (SWFiic), but for a better comparison to the characterization of wellfounded semantics and the following semantics we separate the case. We continue with the example.
Example 3.2. (Example 3.1 continued) As shown in [
It should be mentioned that the reference to derivation sequences in the conditions is also necessary because of the missing closure property of M WS F (Π). 4
Baral, Lobo, and Minker introduced GDWFS [
Definition 4.1. Let S be a state-pair and Π be a disjunctive program. Let T ⊆ EBΠ and F ⊆ CBΠ .
TSD(T ) = {D ∈ EBΠ | D undefined in S, H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π) such that for all i, 1 ≤ i ≤ n, (Ai ∨ Di) ∈ S or (Ai ∨ Di) ∈ T , Di might be empty, ¬Bj ∈ S for all j, 1 ≤ j ≤ m, and (H ∪ i Di) ⊆ D.}
FSD(F ) = {C ∈ CBΠ | C is undefined in S, A ∈ C, and for all clauses H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π), with A ∈ H, at least one of the following three cases holds: (B1 ∨ · · · ∨ Bm) ∈ S, ¬(A1 ∧ · · · ∧ An) ∈ S, or ¬(A1 ∧ · · · ∧ An) ∈ F }
TSD is bottom-up and FSD is top-down: TSD ↑ 0 = ∅, TSD ↑ (n + 1) = TSD(TSD ↑ n), TSD =n<ω nF<SDω ↓TSnD. ↑ n, and FSD ↓ 0 = CBΠ , FSD ↓ (n + 1) = FSD(FSD ↓ n), FSD =
There are two more operators defined for definite programs which necessitates the following program transformations. Given a disjunctive program Π and a state-pair S, DIS(Π) is obtained by transferring all negated atoms in the body of each clause of Π as atoms to its head. Then, Dis(Π, S) results from DIS(Π) by reducing the clauses in DIS(Π) as follows: remove atoms from the body of a clause if they are true in S, remove a clause if its head is true in S, and remove atoms from the head of a clause if they are false in S. This is similar to the construction used for stable models and we recall TΠD(T ), a simplification of TSD(T ) to definite programs. Given a definite (disjunctive) program Π and T , a subset of EBΠ , we have that TΠD(T ) = {D ∈ EBΠ | H ← A1, . . . , An in ground(Π) such that for all i, 1 ≤ i ≤ n, (Ai ∨ Di) ∈ T , Di might be empty, and (H ∪ i Di) ⊆ D.} We then iterate TΠD ↑ 0 = ∅, TΠD ↑ (n + 1) = TΠD(TΠD ↑ n), and TΠD = n<ω TΠD ↑ n.
For deriving indefinite false conjunctions the Extended Generalized Closed
World Assumption (EGCWA) [
The previous two constructions yield the operators TSED = {D | D ∈ TDDis(Π,S) and D ∈ S} and FSED = {C | C ∈ EGCWA(Dis(Π, S) ∪ S) and C ∈ S}. Now we can combine all the operators and obtain
SED(S) = S ∪ TSD ∪ ¬FSD ∪ TSED ∪ ¬FSED.
The iteration is done via M0 = ∅, Mα+1 = SED(Mα), and Mα = β<α Mβ
for limit ordinal α, and has a fixed point [
Example 4.1. Recall the program from Example 3.1. We have MΠED = {l ∨ r, q, f, ¬p, ¬b, ¬c, ¬e, ¬g, ¬(l ∧ r)}. Note that MΠED is closed in so far that any superset of a true disjunction (false conjunction) is true (false) as well. Moreover, the semantics concludes q to be true from q ← ¬q. This is exactly the kind of reasoning which is not applied for the well-founded semantics, thus being the cause for GDWFS and WFS not to coincide on normal programs.
We continue with the level mapping characterization of GDWFS. Definition 4.2. Let Π be a disjunctive logic program, let the state-pair I be a model for Π, and let l1, l2 be disjunctive I-partial level mappings for Π. We say that Π satisfies (GDWF) with respect to I, l1, and l2 if each D ∈ dom(l1) and each ¬C ∈ dom(l1) satisfies one of the following conditions: (GDWFi) D ∈ I and there is a clause H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π) with H ⊆ D such that ¬Bj ∈ I and l1(D) >1 lt(¬Bj ), t ∈ {1, 2}, for all j = 1, . . . , m, and, for all i = 1, . . . , n, there is Di ⊆ D with (Di ∨ Ai) ∈ I where l1(D) > l1(Di ∨ Ai) or l1(D) >1 l2(Di ∨ Ai). (GDWFii) ¬C ∈ I with atom A ∈ C and for each clause H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π) with A ∈ H (at least) one of the following conditions holds: (GDWFiia) ¬(A1 ∧ . . . ∧ An) ∈ I and l1(¬C) ≥ l1(¬(A1 ∧ . . . ∧ An)). (GDWFiia’) ¬(A1 ∧ . . . ∧ An) ∈ I and l1(¬C) >1 l2(¬(A1 ∧ . . . ∧ An)). (GDWFiib) (B1 ∨ . . . ∨ Bm) ∈ I and l1(¬C) >1 lt(B1 ∨ . . . ∨ Bm) for t ∈ {1, 2}. and each D, ¬C ∈ dom(l2) satisfies one of the following conditions: (GDWFi’) D ∈ I and there is a clause H1 ∨ · · · ∨ Hl ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π) such that ∅ = ((H ∪ B) \ D ) ⊆ D, Hk ∈ D′ for each ′ ¬Hk ∈ I with l2(D) >1 lt(¬Hk), t ∈ {1, 2}, Bj ∈ D′ for each ¬Bj ∈ I with l2(D) >1 lt(¬Bj ), t ∈ {1, 2}, for all k = 1, . . . , l and all j = 1, . . . , m, and, for all i = 1, . . . , n, there is Di ⊆ D with (Di ∨ Ai) ∈ I where l2(D) >2 l2(Di ∨ Ai) or Ai ∈ I where l2(D) >1 ls(Ai), s ∈ {1, 2}. (GDWFii’) ¬C ∈ I and C ∈ EGCWA(Dis(Π, S)∪S), C ∈ S and l2(¬C) >1 lt(L), t ∈ {1, 2}, if and only if L ∈ S.
The reason for introducing two mappings is to extrapolate exactly the simultaneous iteration of the two operators dealing with positive, negative respectively, information. The very same argument necessitates the different orderings. From a more general perspective, e.g. (GDWFiia) and (GDWFiia’) employ basically the same kind of dependency, just the proof of the following theorem stating the equivalence enforces the diverse conditions.
Theorem 4.1. Let Π be a disjunctive program with generalized disjunctive
wellfounded model M . Then, in the disjunctive knowledge ordering, M is the greatest
model amongst all models I for which there exist disjunctive I-partial level
mappings l1 and l2 for Π such that Π satisfies (GDWF) w.r.t. I, l1, and l2.
Example 4.2. (Example 4.1 continued) From [
The condition (GDWFii’) directly refers to EGCWA due to problems with minimal models in the level mapping framework (see Section 6).
The third approach we study is the disjunctive well-founded semantics presented
by Brass and Dix in [
We recall the operators defining D-WFS. Both map sets of conditional facts which are disjunctive clauses without any positive atoms in the body and we start with TΦ. Given Φ and a set of conditional facts Γ , we have that TΦ(Γ ) = {(H ∪ i(Hi \{Ai})) ← ¬(B ∪ i Bi) | there is H ← A1, . . . , An, ¬B in ground(Φ) and conditional facts Hi ← ¬Bi ∈ Γ with Ai ∈ Hi for all i = 1, . . . , n.} The iteration of TΦ is given as TΦ ↑ 0 = ∅, TΦ ↑ (n + 1) = TΦ(TΦ ↑ n), and TΦ = n<ω TΦ ↑ n and yields a fixed point.
The next operator is top-down starting with the previous fixed point also applying the notion of heads(S) which is the set of all atoms occurring in some head of a clause contained in a given set of ground clauses S: given a set of conditional facts Γ we define R(Γ ) = {H ← ¬(B ∩ heads(Γ )) | H ← ¬B ∈ Γ , and there is no H′ ← in Γ with H′ ⊆ B or there is no H′ ← ¬B′ in Γ with H′ ⊆ H and B′ ⊆ B where at least one ⊆ is proper.} Note that the second condition forcing one ⊆ to be proper is necessary since otherwise we could remove each conditional fact by means of itself. The iteration of this operator is defined as R ↑ 0 = TΦ, R ↑ (n + 1) = R(R ↑ n) and the fixed point of this operator is called the residual program of Φ.
Given the residual program res(Φ), the disjunctive well-founded model MΦ
is MΦ = {D ∈ EBΦ | there is H ← in res(Φ) with H ⊆ D} ∪ {¬D | D ∈ EBΦ
and ∀D′ ∈ D : D′ ∈ heads(res(Φ))}. Though TΦ is monotonic, R is not and
we cannot generalize the following results to all disjunctive logic programs. We
should note that in [
In the following, we present the alternative characterization of D-WFS. Definition 5.1. Let Φ be a DATALOG program, let I be a model for Φ, and let l be a disjunctive I-partial level mapping for Φ. We say that Φ satisfies (DWF) with respect to I and l if each D ∈ dom(l) satisfies one of the following conditions: (DWFi) D ∈ I and there is a clause H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Φ) with H ⊆ D such that there is Di ⊆ D with (Di ∨ Ai) ∈ I, l(D) > l(Di ∨ Ai), and l(D) ≻ l(Di ∨ Ai) if l(D) >1 l(Di ∨ Ai), for all i = 1, . . . , n, and ¬Bj ∈ I and l(D) >1 l(Bj ) for all j = 1, . . . , m. (DWFii) ¬D ∈ I and for each clause H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Φ) with A ∈ H and A ∈ D (at least) one of the following conditions holds: (DWFiia) ¬Ai ∈ I and l(D) ≥ l(Ai).
(DWFiib) D′ ∈ I with D′ ⊆ B and l(D) >1 l(D′). (DWFii’) ¬D ∈ I and for each conditional fact H ← ¬B in TΦ with A ∈ H and A ∈ D (at least) one of the following conditions holds: (DWFiia’) there is H′ ← ¬B′ in R ↑ α with H′ ⊂ H and B′ ⊆ (B \ D′) ′ where A ∈ H , Bj ∈ B, ¬Bj ∈ I, and l(D) >1 (l(Bj ) + 1) for all Bj ∈ D′, and l(D) >1 (α, β) for some β.
(DWFiib’) D′ ∈ I with D′ ⊆ B and l(D) >1 l(D′).
It is evident that (DWFiib) and (DWFiib’) apply the same kind of dependency only that the former does this wrt. to one clause while the latter may employ several, i.e. (DWFiib) can be considered a special case of (DWFiib’) which appears basically for easier comparison.
Theorem 5.1. Let Φ be a (disjunctive) DATALOG program with disjunctive
well-founded model M . Then, in the disjunctive knowledge ordering, M is the
greatest model amongst all models I for which there exists a disjunctive I-partial
level mapping l for Φ such that Φ satisfies (DWF) with respect to I and l.
Example 5.2. (Example 5.1 continued) From [
Finally, we mention that ≻ was introduced for technical reasons in the proof
to match the precise behavior of the operators [
It was already shown in [
We will now further compare the semantics on the basis of our characterizations. We will in particular attempt to obtain some insights into good general criteria for a well-founded semantics for disjunctive programs.
Level-mapping characterizations separate positive and negative information. One key insight which can be drawn from our investigations is that any characterization basically states that a true disjunction D satisfies the following scheme with respect to the model I and the program Π.
D ∈ I and there is a clause H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π) with H ⊆ D such that there is Di ⊆ D with (Di ∨Ai) ∈ I, l(D) > l(Di ∨Ai), for all i = 1, . . . , n, and ¬Bj ∈ I and l(D) > l(Bj ) for all j = 1, . . . , m.
We can see that this corresponds in general to (SWFia) from Definition 3.2, to (GDWFi) from Definition 4.2, and to (DWFi) from Definition 5.1. We only have to consider that the relation > is technically not sufficient and that we sometimes apply a more precise order. Nevertheless, in all cases we obtain levels such that l(D) is greater with respect to the specific ordering. There are further differing details. For (SWF), we have to abstract additionally from the notion of derivation sequences and their children, and there is also (SWFib) which arises from proof-theoretical treatments. In case of (GDWF) we have additionally a condition (GDWFi’) but that is the part (corresponding to TΠD) which derives more knowledge than the well-founded semantics and should thus not be an intended result for a well-founded semantics for disjunctive programs. We claim that the condition given above is the ’disjunctive’ version of (WFi) from Definition 2.1 and we propose it to be a condition for any semantics aiming to extend the well-founded semantics to disjunctive programs.
If we look for adequate extensions of (WFii) to disjunctive programs then we see that the conditions for negative information differ more. However, we still obtain straightforward extensions of (WFii) for each of the semantics only abstracting a little from the technical details. We generalize to the following scheme: ¬D ∈ I and for each clause H ← A1, . . . , An, ¬B1, . . . , ¬Bm in ground(Π) with A ∈ H and A ∈ D (at least) one of the following conditions holds: (iia)¬α ∈ I and l(D) ≥ l(α).
(iib) D′ ∈ I with D′ ⊆ B and l(D) >1 l(D′).
For SWFS, we have (SWFiia’) with α = D ∨ Ai and (SWFiia”) with α = Ai corresponding to (iia) depending on whether H ⊆ D or H ⊆ D but H ∩ D = ∅7, and (SWFiib’) as equivalent to (iib). In case of GDWFS, we have (GDWFiia) and (GDWFiia’) both with α = ¬(A1∧. . .∧An) for (iia) and (GDWFiib) for (iib). We only have to take care that l(D) has to be l(¬D) in this case since we are dealing with negated conjunctions and thus indefinite information. Finally, (DWFiia) with α = Ai and (DWFiib) correspond to (iia) and (iib), respectively. We claim as well that the scheme above should be part of any well-founded semantics for disjunctive programs ignoring some minor differences depending e.g. on whether we represent negative information by conjunctions or disjunctions.
Unfortunately, since positive information may be indefinite, it is also possible to obtain a correspondence to (iib) which results from several clauses (consider the program Π = {p ∨ q ←; r ← s, ¬p; s ← ¬q} where ¬r is derivable). This is covered by (SWFiic), (GDWFii’), and (DWFiib’). Still, this is not the whole characterization for any of the semantics. (SWFiib”) extends (SWFiib’) to include particular atoms from the head. (GDWFii’) is in fact much more powerful by 7 Note that in both cases there is an A common to H and D. means of the EGCWA and allows for deriving more knowledge difficult to characterize in a clause-based approach. In case of D-WFS we also have (DWFiia’) which resolves the elimination of non-minimal clauses, a feature not contained in SWFS and also covered by (GDWFii’) for GDWFS.
Summarising, it is obvious (and certainly expected) that it is in the derivation of negative information where the semantics differ wildly. All characterizations contain extensions of (WFii), but contain also additional non-trivial conditions some of which are difficult to capture within level mapping characterizations. The obtained uniform characterizations thus display in a very explicit manner the very different natures of the different well-founded semantics – there is simply not enough resemblance between the approaches to obtain a coherent picture. We can thus, basically, only confirm in a more formal way what has been known beforehand, namely that the issue of a good definition of well-founded semantics for disjunctive logic programs remains widely open. We believe, though, that our approach delivers structural insights which can guide the quest. 6.2
As mentioned when dealing with the EGCWA appearing in GDWFS it is
difficult within the level mapping framework to characterize minimal models which
are the main evaluation principle for EGCWA. In the appendix of [
This is of course not a characterization but just saying that a model satisfying the given level mapping characterization is in fact minimal. Unfortunately, it is not possible to state this the other way around since there are minimal models which do not satisfy this condition8.
Example 6.1.
a ∨ b ←
a ← b
b ← a
This program has only one minimal model {a, b}, so according to the condition
above, the first clause cannot be used since both atoms in the head are true.
With the remaining two clauses we cannot have a level mapping satisfying the
given condition since we must have l(a) > l(b) and l(b) > l(a) which is not
possible.
8 Note though that in [
Apparently, the condition imposed is too strong but all attempts (cf. [
We can thus not apply a more precise condition for EGCWA. More generally, any semantics based on minimal models seems to fail being characterized in the framework (excluding cases like GDWFS where we simply do not treat the details of EGCWA). So surprisingly, even though disjunctive stable models are a straightforward extension of stable models, the corresponding characterization does not extend easily if at all.
It remains to be said that in opposite to that there exist characterizations for various semantic extensions of the well-founded semantics, though being rather complicated and diverse, which might allow the conclusion that (almost) any of the approaches has a better structural foundation than minimal models. 7
We have characterized three of the extensions of the well-founded semantics to disjunctive logic programs. It has been revealed that these characterizations are non-trivial and we have seen that they share a common derivability for true disjunctions. The conditions for deriving negative information however vary a lot. Some parts of the characterizations are common extensions of conditions used for the well-founded semantics while others cover specific deduction mechanisms occurring only in one semantics. We have obtained some structural insights into the differences and similarities of proposals for disjunctive well-founded semantics, but the main conclusion we have to draw is a negative one: Even under our formal approach which provides uniform characterizations of different semantics, the different proposals turn out to be too diverse for a meaningful comparison. The quest for disjunctive well-founded semantics thus remains widely open. Our uniform characterizations provide, however, arguments for approaching the quest in a more systematic way.
In this paper, we covered only those of the well-founded semantics which
a priory appeared to be the most important and promising ones. Obviously,
further insights could be obtained from considering also the remaining proposals
reported e.g. in [