Introduction

Two semantics are nowadays considered to be the most important ones for normal logic programs. Stable model semantics [1] is the main two-valued approach whereas the major three-valued semantics is the well-founded semantics [2]. These two semantics are well-known to be closely related. However, enriching normal logic programs with indefinite information by allowing disjunctions in the head 3 of the clauses separates these two approaches. While disjunctive stable models [5] are a straightforward extension of the stable model semantics, the issue of disjunctive well-founded semantics remains unresolved, although several proposals exist.

Even a comparison of existing proposals is difficult due to the large variety of completely different constructions on which these semantics are based. In [6], Ross introduced the strong well-founded semantics (SWFS) based on a topdown procedure using derivation trees. The generalized disjunctive well-founded semantics (GDWFS) was defined by Baral, Lobo, and Minker in [7], built on several bottom-up operators and the extended generalized closed world assumption [8]. Brass and Dix proposed the disjunctive well-founded semantics (D-WFS) in [9] based on two operators iterating over conditional facts, respectively some general program transformations.

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 [10]. This results in characterizations providing easy comparisons of the corresponding semantics.

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 [11].

General Notions and Preliminaries

A disjunctive logic program Π consists of finitely many universally quantified clauses of the form

H 1 ∨ • • • ∨ H l ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m

where H k , A i , and B j , 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

H 1 ∨ • • • ∨ H l and the body A 1 , . . . , A n , ¬B 1 , • • • , ¬B m .

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 ⊆ B P and A ∩ B = ∅, where elements in A, B respectively, are t, f , and the remaining wrt. B P are u. The set of three-valued interpretations is denoted by I P,3 . Given a three-valued interpretation I, the body of a ground clause

H ← L 1 , . . . , L n is true in I if and only if L i ∈ I, 1 ≤ i ≤ n, or false in I if and only if L i ∈ 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 I 1 and I 2 , is defined as I 1 ≤ k I 2 if and only if I 1 ⊆ I 2 . For a program P and a three-valued interpretation I ∈ I P,3 an I-partial level mapping for P is a partial mapping l : B P → α 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 [2]. Definition 2.1. ( [10]) Let P be a normal logic program, let I be a model for P , and let l be an I-partial level mapping for P . We say that P satisfies (WF) with respect to I and l if each A ∈ dom(l) satisfies one of the following conditions.

(WFi) A ∈ I and there is a clause A ← L 1 , . . . , L n in ground(P ) such that L i ∈ I and l(A) > l(L i ) for all i.

(WFii) ¬A ∈ I and for each clause A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(P ) one (at least) of the following conditions holds:

(WFiia) There exists i with ¬A i ∈ I and l(A) ≥ l(A i ).

(WFiib) There exists j with B j ∈ I and l(A) > l(B j ).

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. ( [10]) Let P be a normal logic program with well-founded model M . Then, in the knowledge ordering, M is the greatest model amongst all models I for which there exists an I-partial level mapping l for P such that P satisfies (WF) with respect to I and l.

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 D 1 and

D 2 , ¬D 1 ∈ I ′ and ¬D 2 ∈ I ′ if and only if ¬(D 1 ∨ D 2 ) ∈ I ′ . Then, I is consistent if there is no D ∈ cl(I) with ¬D ∈ cl(I) as well 4 . A disjunctive three-valued interpretation I of a disjunctive program Π is a consistent set A ∪ ¬B, A, B ⊆ EB Π ,

Another way of representing disjunctive information are state-pairsA ∪ ¬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 ′ then C ′ ∈ B.

Disjunctions in A are t, conjunctions in B are f , and all remaining are u. A state-pair is consistent if whenever D ∈ A then there is at least one disjunct D ′ ∈ D such that D ′ ∈ B and whenever C ∈ B then there is at least one conjunct C ′ ∈ C such that C ′ ∈ A. The notions of models and the disjunctive knowledge ordering can easily be adopted. Note that a state-pair is not necessarily consistent and that it contains indefinite positive and negative information in opposite to disjunctive interpretations where negative information will be precise. Level mappings are adjusted to state-pairs in the following and now we do not extend the mapping to identify l(D) = l(¬D) since in a state-pair D is a disjunction and ¬D a negated conjunction. 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.

Strong Well-founded Semantics

We start with SWFS which was introduced by Ross [6] and based on disjunctive interpretations. The derivation rules of the applied top-down procedure are the following. Given a set of disjunction literals I and a disjunctive program Π the derivate I ′ is strongly derived from

I (I ⇐ I ′ ) if I contains a disjunction D and ground(Π) a clause H ← A 1 , . . . , A n , ¬ B such that either (S1) H ⊆ D and I ′ = (I \ {D}) ∪ {A 1 ∨ D, . . . , A n ∨ D} ∪ ¬B or (S2) H ⊆ D, H ∩ D = ∅, C = H \ D, and I ′ = (I \ {D}) ∪ A ∪ ¬B ∪ ¬C.

Consider a ground disjunction D, let I 0 = {D} and suppose that I 0 ⇐ I 1 ⇐ I 2 . . ., then I 0 , I 1 , I 2 . . . 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 = {¬l 1 , . . . , ¬l n } is turned into a disjunction Ī = l 1 ∨ • • • ∨ l n

and if I is empty, denoting t, then Ī denotes f . Thus, a strong global tree Γ S D for a given disjunction D ∈ EB Π contains the root D and its children are all disjunctions of the form Ī, where I ranges over all bases for D. The strong well-founded model

of a disjunctive program Π is called M S W F (Π) and D ∈ M S W F (Π), i.e. D is true, if some child of D is false and ¬D ∈ M S W 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 S W F (Π)

. In [6], it was shown that M S W F (Π) is a consistent interpretation and that, for normal programs, SWFS coincides with the well-founded semantics6 .

Example 3.1. The following program Π will be used to demonstrate the behavior of the three semantics.

p ∨ q ← ¬q b ∨ l ← ¬r c ← ¬l, ¬r f ← ¬e q ← ¬q l ∨ r ← e ← ¬f, c g ← e

We obtain a sequence {l ∨ r} ⇐ {} and l ∨ r is true as expected. Furthermore, there is a finite sequence in Γ S e , namely {e} ⇐ {¬f, e ∨ c} ⇐ {¬f, ¬l, ¬c} with the only (true) child and e is false. Thus, we have that M S W 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 S W 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 Π.

I 1 = {D 1 , . . . , D n , ¬D n+1 , . . . , ¬D m } where ¬C ∈ M S W F (Π), Γ S C ∈ Γ if C = {}, Γ S Di ∈ Γ , D i ∈ M S W F , Γ S Dj ∈ Γ , ¬D j ∈ M S W F for all i = 1, . . . , n and j = n + 1, . . . , m} -U S Π (Γ ) = {Γ S D ∈ Γ S Π | for all active strong derivation sequences in Γ S D the corresponding child C is true in M S W F (Π) and Γ S C ∈ Γ } 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 [11] that W S Π is monotonic, allowing to apply the Tarski fixed-point theorem which yields that the operator W S Π always has a least fixed point, and that this least fixed point coincides with M S W F . This was used to derive the following alternative characterization of SWFS. Definition 3.2. Let Π be a disjunctive logic program, let I be a model for Π, and let l be a disjunctive partial level mapping for Π. We say that Π satisfies (SWF) with respect to I and l if each D ∈ dom(l) satisfies one of the following conditions:

(SWFi) D ∈ I and Γ S D contains an active strong derivation sequence with child C, ¬C ∈ I and l(D) > l(C) if C = {}, and there is a clause H ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π) which is used for the first derivation of that sequence such that ¬B j ∈ I and l(D) > l(B j ), 1 ≤ j ≤ m, and one of the following conditions holds:

(SWFia) H ⊆ D such that there is 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.

D i ⊆ D with (D i ∨ A i ) ∈ I and l(D) > l(D i ∨ A i ), 1 ≤ i ≤ n. (SWFib) H ⊆ D, H ∩ D = ∅, {C 1 , . . . , C l } = H \ D, A i ∈ I and l(D) > l(A i ), 1 ≤ i ≤ n,

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 [11], we obtain l(D) = α, where α is the least ordinal such that Γ S D ∈ (W S Π ↑ (α + 1)) = W S Π (W S Π ↑ α). Thus, we have l(l ∨ r) = 0 by (SWFia) and l(e) = 1 by (SWFiia') and therefore l(f ) = 2 by (SWFia). Moreover, l(b) = 1 by (SWFiib') whereas l(c) = 1 by (SWFiib"). Note that in case of c, and e also (SWFiic) is satisfied.

It should be mentioned that the reference to derivation sequences in the conditions is also necessary because of the missing closure property of M S W F (Π).

4 Generalized Disjunctive Well-founded Semantics

⊆ CB Π . T D S (T ) = {D ∈ EB Π | D undefined in S, H ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π) such that for all i, 1 ≤ i ≤ n, (A i ∨ D i ) ∈ S or (A i ∨ D i ) ∈ T , D i might be empty, ¬B j ∈ S for all j, 1 ≤ j ≤ m, and (H ∪ i D i ) ⊆ D.} F D S (F ) = {C ∈ CB Π | C is undefined in S, A ∈ C

, and for all clauses H ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π), with A ∈ H, at least one of the following three cases holds:

(B 1 ∨ • • • ∨ B m ) ∈ S, ¬(A 1 ∧ • • • ∧ A n ) ∈ S, or ¬(A 1 ∧ • • • ∧ A n ) ∈ F } T D S is bottom-up and F D S is top-down: T D S ↑ 0 = ∅, T D S ↑ (n+1) = T D S (T D S ↑ n), T D S = n<ω T D S ↑ n,andF D S ↓ 0 = CB Π , F D S ↓ (n + 1) = F D S (F D S ↓ n), F D S = n<ω F D S ↓ n.

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 T D S (T ) to definite programs. Given a definite (disjunctive) program Π and T , a subset of EB Π , we have that

T D Π (T ) = {D ∈ EB Π | H ← A 1 , . . . , A n in ground(Π) such that for all i, 1 ≤ i ≤ n, (A i ∨ D i ) ∈ T , D i might be empty, and (H ∪ i D i ) ⊆ D.} We then iterate T D Π ↑ 0 = ∅, T D Π ↑ (n + 1) = T D Π (T D Π ↑ n),andT D Π = n<ω T D Π ↑ n.

For deriving indefinite false conjunctions the Extended Generalized Closed World Assumption (EGCWA) [8] is applied. It intuitively says that a conjunction can be inferred to be false from Π if and only if it is false in all minimal models of Π where a minimal model [12] is a two-valued model M of Π such that no subset of it is a model as well.

The The iteration is done via M 0 = ∅, M α+1 = S ED (M α ), and M α = β<α M β for limit ordinal α, has a fixed point [7]. The fixed point corresponds to the generalized disjunctive well-founded model M ED Π which is consistent [7]. However, for normal logic programs in general, the well-founded semantics and GDWFS do not coincide. = {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 l 1 , l 2 be disjunctive I-partial level mappings for Π. We say that Π satisfies (GDWF) with respect to I, l 1 , and l 2 if each D ∈ dom(l 1 ) and each ¬C ∈ dom(l 1 ) satisfies one of the following conditions:

(GDWFi) D ∈ I and there is a clause H ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π) with H ⊆ D such that ¬B j ∈ I and l 1 (D) > 1 l t (¬B j ), t ∈ {1, 2}, for all j = 1, . . . , m, and, for all i = 1, . . . , n, there is

D i ⊆ D with (D i ∨ A i ) ∈ I where l 1 (D) > l 1 (D i ∨ A i ) or l 1 (D) > 1 l 2 (D i ∨ A i ).

(GDWFii) ¬C ∈ I with atom A ∈ C and for each clause H ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π) with A ∈ H (at least) one of the following conditions holds:

(GDWFiia)

¬(A 1 ∧ . . . ∧ A n ) ∈ I and l 1 (¬C) ≥ l 1 (¬(A 1 ∧ . . . ∧ A n )). (GDWFiia') ¬(A 1 ∧ . . . ∧ A n ) ∈ I and l 1 (¬C) > 1 l 2 (¬(A 1 ∧ . . . ∧ A n )). (GDWFiib) (B 1 ∨ . . . ∨ B m ) ∈ I and l 1 (¬C) > 1 l t (B 1 ∨ . . . ∨ B m ) for t ∈ {1, 2}.

and each D, ¬C ∈ dom(l 2 ) satisfies one of the following conditions:

(GDWFi') D ∈ I and there is a clause

1 ∨ • • • ∨ H l ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π) such that ∅ = ((H ∪ B) \ D ′ ) ⊆ D, H k ∈ D ′ for each ¬H k ∈ I with l 2 (D) > 1 l t (¬H k ), t ∈ {1, 2}, B j ∈ D ′ for each ¬B j ∈ I with l 2 (D) > 1 l t (¬B j ), t ∈ {1, 2}

, for all k = 1, . . . , l and all j = 1, . . . , m, and, for all i = 1, . . . , n, there is

D i ⊆ D with (D i ∨ A i ) ∈ I where l 2 (D) > 2 l 2 (D i ∨ A i ) or A i ∈ I where l 2 (D) > 1 l s (A i ), s ∈ {1, 2}. (GDWFii') ¬C ∈ I and C ∈ EGCWA(Dis(Π, S)∪S), C ∈ S and l 2 (¬C) > 1 l t (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 l 1 and l 2 for Π such that Π satisfies (GDWF) w.r.t. I, l 1 , and l 2 .

(¬C) = (α, 0) if C ∈ F D Mα and l 2 (¬C) = (α, 0) if C ∈ F ED

Mα . Thus, we obtain e.g. l 1 (l ∨ r) = l 2 (l ∨ r) = (0, 0) by (GDWFi) and (GDWFi'), l 1 (f ) = (2, 0) by (GDWFi), l 2 (¬p) = (0, 0) by (GDWFii'), l 1 (¬e) = (1, 0) by (GDWFiia') and l 1 (¬g) = (1, 0) by (GDWFiia).

The condition (GDWFii') directly refers to EGCWA due to problems with minimal models in the level mapping framework (see Section 6).

Disjunctive Well-founded Semantics

The third approach we study is the disjunctive well-founded semantics presented by Brass and Dix in [9]. We use again disjunctive interpretations for representing information even though in [9] the syntactically different pure disjunctions are applied. D-WFS is only defined for (disjunctive) DATALOG programs which are programs whose corresponding language does not have any function symbols apart from (nullary) constants. Thus they correspond to propositional programs and we use the notation Φ from [9] for DATALOG programs.

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 (H i \{A i })) ← ¬(B ∪ i B i ) | there is H ← A 1 , . . . , A n , ¬B in ground(Φ) and conditional facts H i ← ¬B i ∈ Γ with A i ∈ H i 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 [13] the approach was extended to disjunctive logic programs by combining the transformation rules with constraint logic programming. But the operators are not extended as well and we remain with that restriction.

Example 5.1. Recall Π from Example 3.1. It is obvious that Π is also a DATA-LOG program and we obtain M Π = {l ∨ r, f, ¬p, ¬c, ¬e, ¬g}. Note that Π is closed by definition of the model.

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 ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Φ) with H ⊆ D such that there is D i ⊆ D with (D i ∨ A i ) ∈ I, l(D) > l(D i ∨ A i ), and l(D) ≻ l(D i ∨ A i ) if l(D) > 1 l(D i ∨ A i )

, for all i = 1, . . . , n, and ¬B j ∈ I and l(D) > 1 l(B j ) for all j = 1, . . . , m.

(DWFii) ¬D ∈ I and for each clause H ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Φ) with A ∈ H and A ∈ D (at least) one of the following conditions holds:

(DWFiia) ¬A i ∈ I and l(D) ≥ l(A i ).

(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 ′ , B j ∈ B, ¬B j ∈ I, and l(D) > 1 (l(B j ) + 1) for all B j ∈ 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 [11] we know that if ∈ M then l(D) = (α, β) where α is the least ordinal such that H ← in R ↑ α with H ⊆ D and β is the least ordinal such that the corresponding conditional fact H ← ¬B in T Φ ↑ (β + 1). Furthermore, if ¬D ∈ M then l(D) = (α, 0) where α is the least ordinal such that for each A ∈ D there is no conditional fact H ← ¬B in R ↑ α with A ∈ H. Thus, we obtain e.g. l(f ) = (2, 0) by (DWFi), l(p) = (1, 0) by (DWFiia'), l(c) = (1, 0) by (DWFiib) and l(e) = (1, 0) by (DWFiia).

Finally, we mention that ≻ was introduced for technical reasons in the proof to match the precise behavior of the operators [11].

Discussions

Comparison of the Characterizations

It was already shown in [9] that D-WFS and GDWFS satisfy five program transformation principles while SWFS does not, and that GDWFS always derives more or equal knowledge than D-WFS [14]. However, there is no similar result for D-WFS and SWFS since they are incomparable with respect to the derived knowledge (cf. our main example: SWFS derives ¬b while D-WFS concludes ¬p).

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 ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m in ground(Π) with H ⊆ D such that there is D i ⊆ D with (D i ∨A i ) ∈ I, l(D) > l(D i ∨A i ), for all i = 1, . . . , n, and ¬B j ∈ I and l(D) > l(B j ) 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: For SWFS, we have (SWFiia') with α = D ∨ A i and (SWFiia") with α = A i 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 α = ¬(A 1 ∧. . .∧A n ) 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 α = A i 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 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.

Minimal Models

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 [11] it was concluded that the best possible characterization obtained for minimal models is the following: Corollary 6.1. ( [11]) Let Π be a definite disjunctive program and M be a model of Π. If there exists a total level mapping l : B Π → α such that for each A ∈ M exists a clause A ∨ H 1 ∨ • • • ∨ H l ← A 1 , . . . , A n in ground(Π) with A i ∈ M , H k ∈ M or l(H k ) > l(A), and l(A) > l(A i ), for all i = 1, . . . , n and all k = 1, . . . , l, then M is a minimal model 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 . Apparently, the condition imposed is too strong but all attempts (cf. [11]) to correct the problem end up with a condition too weak being satisfied also by models which are not minimal.

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.

Conclusions

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 [16][17][18][19][20]14].