=Paper=
{{Paper
|id=Vol-277/paper-3
|storemode=property
|title=A Comparison of Disjunctive Well-founded Semantics
|pdfUrl=https://ceur-ws.org/Vol-277/paper3.pdf
|volume=Vol-277
|dblpUrl=https://dblp.org/rec/conf/ki/KnorrH07
}}
==A Comparison of Disjunctive Well-founded Semantics==
Comparing Disjunctive Well-founded Semantics⋆
Matthias Knorr1 and Pascal Hitzler2
1
CENTRIA, Universidade Nova de Lisboa, Portugal
2
AIFB, Universität Karlsruhe, Germany
Abstract. 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 se-
mantics 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 intro-
duced 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 han-
dling of negation. Additionally, we show some of the problems occurring
when trying to handle minimal models (and thus disjunctive stable mod-
els) within the framework.
1 Introduction
Two semantics are nowadays considered to be the most important ones for nor-
mal 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 head3 of the clauses separates these two approaches. While disjunctive sta-
ble 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 vari-
ety of completely different constructions on which these semantics are based. In
[6], Ross introduced the strong well-founded semantics (SWFS) based on a top-
down procedure using derivation trees. The generalized disjunctive well-founded
⋆
This research has been partly funded by the European Commission within
the 6th Framework Programme projects REWERSE number 506779 (cf.
http://rewerse.net/) and NeOn (IST-2006-027595, cf. http://www.neon-
project.org/), and by the Deutsche Forschungsgemeinschaft under project
ReaSem.
3
For an overview of semantics for disjunctive logic programs we refer to [3] and [4].
semantics (GDWFS) was defined by Baral, Lobo, and Minker in [7], built on sev-
eral 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 compar-
isons 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].
2 General Notions and Preliminaries
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 se-
mantics 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 ← L1 , . . . , Ln in ground(P ) such that
Li ∈ I and l(A) > l(Li ) for all i.
(WFii) ¬A ∈ I and for each clause A ← A1 , . . . , An , ¬B1 , . . . , ¬Bm in
ground(P ) one (at least) of the following conditions holds:
(WFiia) There exists i with ¬Ai ∈ I and l(A) ≥ l(Ai ).
(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. ([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 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 ∈ I 5 . 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 (count-
able) 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 [6].
5
The extension is necessary since we might e.g. know the truth of some disjunction
without knowing which particular disjunct is true.
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.
3 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 ← A1 , . . . , An , ¬ B such that either
(S1) H ⊆ D and I ′ = (I \ {D}) ∪ {A1 ∨ D, . . . , An ∨ D} ∪ ¬B or
(S2) H ⊆ D, H ∩ D = ∅, C = H \ D, and I ′ = (I \ {D}) ∪ A ∪ ¬B ∪ ¬C.
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 ΓD S
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
S S
of a disjunctive program Π is called MW F (Π) and D ∈ MW F (Π), i.e. D is true,
S
if some child of D is false and ¬D ∈ MW F (Π), i.e. D is false, if every child of
S
D is true. Otherwise, D is undefined and neither D nor ¬D occur in MW F (Π).
S
In [6], it was shown that MW 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
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}
S
with the only (true) child and e is false. Thus, we have that MW F (Π) = {l ∨
r, f, ¬b, ¬c, ¬e, ¬g} while p and q remain undefined. Literally, this is only a small
S
part of the model and we might close the model (e.g. ¬(e ∨ g) ∈ MW 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
S S
trees defined on ΓΠ which is the power set of ΓΠ - the set of all strong global
trees with respect to Π.
S
Definition 3.1. Let Π be a disjunctive logic program, MW F (Π) the strong well-
S
founded model, and Γ ∈ ΓΠ . We define:
S S S S
– TΠ (Γ ) = {ΓD ∈ ΓΠ | ΓD contains an active strong derivation sequence
{D}, I1 , . . . , Ir with child C = I¯r and I1 = {D1 , . . . , Dn , ¬Dn+1 , . . . , ¬Dm }
S S S S S
where ¬C ∈ MW F (Π), ΓC ∈ Γ if C = {}, ΓDi ∈ Γ , Di ∈ MW F , ΓDj ∈ Γ ,
S
¬Dj ∈ MW F for all i = 1, . . . , n and j = n + 1, . . . , m}
S S S S
– UΠ (Γ ) = {ΓD ∈ ΓΠ | for all active strong derivation sequences in ΓD the
S S
corresponding child C is true in MW F (Π) and Γ C ∈ Γ }
S S S S
The information is joined by WΠ (Γ ) = TΠ (Γ ) ∪ UΠ (Γ ) and iterated: WΠ ↑
S S S S S
0 = ∅, WΠ ↑ n + 1 = WΠ (WΠ ↑ n), and WΠ ↑ α = β<α WΠ ↑ β for limit
S
ordinal α. It was shown in [11] that WΠ is monotonic, allowing to apply the
S
Tarski fixed-point theorem which yields that the operator WΠ always has a
S
least fixed point, and that this least fixed point coincides with MW 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:
S
(SWFi) D ∈ I and Γ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 ←
A1 , . . . , An , ¬B1 , . . . , ¬Bm in ground(Π) which is used for the first derivation
of that sequence such that ¬Bj ∈ I and l(D) > l(Bj ), 1 ≤ j ≤ m, and one
of the following conditions holds:
(SWFia) H ⊆ D such that there is Di ⊆ D with (Di ∨ Ai ) ∈ I and
l(D) > l(Di ∨ Ai ), 1 ≤ i ≤ n.
(SWFib) H ⊆ D, H ∩ D = ∅, {C1 , . . . , Cl } = H \ D, Ai ∈ I and
l(D) > l(Ai ), 1 ≤ i ≤ n, and ¬Ck ∈ I and l(D) > l(Ck ), 1 ≤ k ≤ l.
S
(SWFii) ¬D ∈ I and for each active strong derivation sequence in ΓD with
child C ∈ I there is a clause H ← A1 , . . . , An , ¬B1 , . . . , ¬Bm in ground(Π)
which is used for the first derivation of that sequence such that (at least) one
of the following conditions holds:
(SWFiia’) H ⊆ D and there exists i, 1 ≤ i ≤ n, with ¬(Ai ∨ D) ∈ I,
l(D) ≥ l(Ai ∨ D).
(SWFiia”) H ⊆ D, H ∩ D = ∅, and there exists i with ¬Ai ∈ I, l(D) ≥
l(Ai ), 1 ≤ i ≤ n.
(SWFiib’) H ⊆ D and there exists D′ with D′ ⊆ B, D′ ∈ I and l(D) >
l(D′ ).
(SWFiib”) H ⊆ D, H ∩ D = ∅, C = (H \ D), and there exists D′ with
D′ ⊆ (B ∪ C), D′ ∈ I and l(D) > l(D′ ).
(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 well-
founded 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) = α,
S S S S
where α is the least ordinal such that ΓD ∈ (WΠ ↑ (α + 1)) = WΠ (WΠ ↑ α).
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 b, c, and e also (SWFiic) is satisfied.
It should be mentioned that the reference to derivation sequences in the
S
conditions is also necessary because of the missing closure property of MW F (Π).
4 Generalized Disjunctive Well-founded Semantics
Baral, Lobo, and Minker introduced GDWFS [7] based on state-pairs. They
applied various operators for calculating the semantics and we recall at first TSD
and FSD for disjunctive programs.
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 ) ∈ Sor (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), TS = n<ω TS ↑ n, and FSD ↓ 0 = CBΠ , FSD ↓ (n + 1) = FSD (FSD ↓ n),
D D
FSD = n<ω FSD ↓ 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
D
to the construction used for stable models and we recall TΠ (T ), a simplification
of TSD (T ) to definite programs. Given a definite (disjunctive) program Π and
D
T , a subset of EBΠ , we have that TΠ (T ) = {D ∈ EBΠ | H ← A1 , . . . , An in
ground(Π) such that for all i, 1 ≤ i ≤ n, (Ai ∨ Di ) ∈ T , Di might be empty, and
D D D D
(H ∪ i Di ) ⊆ D.} We then iterate TΠ ↑ 0 = ∅, TΠ ↑ (n + 1) = TΠ (TΠ ↑ n),
D D
and TΠ = n<ω TΠ ↑ 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 previous two constructions yield the operators TSED = {D | D ∈
D
TDis(Π,S) and D ∈ S} and FSED = {C | C ∈ EGCWA(Dis(Π, S) ∪ S) and
C ∈ S}. Now we can combine all the operators and obtain
S ED (S) = S ∪ TSD ∪ ¬FSD ∪ TSED ∪ ¬FSED .
The iteration is done via M0 = ∅, Mα+1 = S ED (Mα ), and Mα = β<α Mβ
for limit ordinal α, and has a fixed point [7]. The fixed point corresponds to
ED
the generalized disjunctive well-founded model MΠ which is consistent [7].
However, for normal logic programs in general, the well-founded semantics and
GDWFS do not coincide.
ED
Example 4.1. Recall the program from Example 3.1. We have MΠ = {l ∨
ED
r, q, f, ¬p, ¬b, ¬c, ¬e, ¬g, ¬(l ∧ r)}. Note that MΠ 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 si-
multaneous iteration of the two operators dealing with positive, negative respec-
tively, information. The very same argument necessitates the different orderings.
From a more general perspective, e.g. (GDWFiia) and (GDWFiia’) employ ba-
sically 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 well-
founded 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 map-
pings l1 and l2 for Π such that Π satisfies (GDWF) w.r.t. I, l1 , and l2 .
D
Example 4.2. (Example 4.1 continued) From [11] we know that if D ∈ TM α
then
D ED
β is the least ordinal such that D ∈ TMα ↑ (β+1) and l1 (D) = (α, β), if D ∈ TM α
D
then β is the least ordinal such that D ∈ TDis(Π,M α ) ↑ (β + 1) and l 2 (D) =
D
(α, β). For negative conjunctions it holds that l1 (¬C) = (α, 0) if C ∈ FM α
and
ED
l2 (¬C) = (α, 0) if C ∈ FMα . Thus, we obtain e.g. l1 (l ∨ r) = l2 (l ∨ r) = (0, 0)
by (GDWFi) and (GDWFi’), l1 (f ) = (2, 0) by (GDWFi), l2 (¬p) = (0, 0) by
(GDWFii’), l1 (¬e) = (1, 0) by (GDWFiia’) and l1 (¬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).
5 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
TΦ . Given Φ and a
start with 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 [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 MΠ 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 ← 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 depen-
dency 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 D ∈ 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].
6 Discussions
6.1 Comparison of the Characterizations
It was already shown in [9] that D-WFS and GDWFS satisfy five program trans-
formation 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 characteriza-
tions. 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 charac-
terization 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
D
additionally a condition (GDWFi’) but that is the part (corresponding to TΠ )
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 char-
acterization 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 char-
acterize 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 Minimal Models
As mentioned when dealing with the EGCWA appearing in GDWFS it is diffi-
cult 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 ∨ H1 ∨ · · · ∨ Hl ← A1 , . . . , An in ground(Π) with Ai ∈ M , Hk ∈
M or l(Hk ) > l(A), and l(A) > l(Ai ), 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 .
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 [15] a similar result was obtained working in both directions
restricted to head-cycle free programs.
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.
7 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 dis-
junctions. 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 seman-
tics, 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–20, 14].
References
1. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming.
In Kowalski, R.A., Bowen, K.A., eds.: Logic Programming. Proceedings of the
5th International Conference and Symposium on Logic Programming, MIT Press
(1988) 1070–1080
2. van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general
logic programs. Journal of the ACM 38 (1991) 620–650
3. Lobo, J., Minker, J., Rajasekar, A.: Foundations of Disjunctive Logic Program-
ming. MIT Press (1992)
4. Minker, J., Seipel, D.: Disjunctive logic programming: A survey and assessment.
In: Essays in Honour of Robert A. Kowalski, Part I, LNAI 2407, Springer (2002)
5. Przymusinski, T.C.: Stable semantics for disjunctive programs. New Generation
Computing 9 (1991) 401–424
6. Ross, K.A.: The well founded semantics for disjunctive logic programs. In Kim,
W., Nicolas, J.M., Nishio, S., eds.: First International Conference on Deductive
and Object Oriented Databases, Elsevier Science Publishers B.V. (North-Holland)
(1990) 385–402
7. Baral, C., Lobo, J., Minker, J.: Generalized disjunctive well-founded semantics
for logic programs. In Z. W. Ras, M.Z., Emrich, M., eds.: Proceedings of the
Fifth International Symposium on Methodologies for Intelligent Systems. ACM
SIGMOD-SIGACT-SIGART, North Holland (1989) 465–473
8. Yahya, A., Henschen, L.: Deduction in non-Horn databases. Journal Automated
Reasoning 1 (1985) 141–160
9. Brass, S., Dix, J.: Disjunctive semantics based upon partial and bottom-up eval-
uation. In: Proceedings of the 12th International Logic Programming Conference,
Tokyo, MIT Press (1995) 199–213
10. Hitzler, P., Wendt, M.: A uniform approach to logic programming semantics.
Theory and Practice of Logic Programming 5 (2005) 123–159
11. Knorr, M., Hitzler, P.: A comparison of disjunctive well-founded semantics. Tech-
nical report, AIFB, University of Karlsruhe, Germany (2006) http://www.aifb.uni-
karlsruhe.de/Publikationen/showPublikation?publ id=1383.
12. Minker, J.: On indefinite databases and the closed world assumption. In: Lecture
Notes in Computer Science 138, Springer, Berlin (1982) 292–308
13. Dix, J., Stolzenburg, F.: Computation of non-ground disjunctive well-founded se-
mantics with constraint logic programming. In Dix, J., Pereira, L.M., Przymusin-
ski, T.C., eds.: Selected Papers of the Workshop on Non-Monotonic Extensions
of Logic Programming in Conjunction with Joint International Conference and
Symposium on Logic Programming 1996, Springer, Berlin, Heidelberg, New York
(1997) 202–224
14. Dix, J., Müller, M.: An axiomatic approach to semantics of disjunctive programs.
In van Hentenryck, P., ed.: Logic Programming, Proc. of the 11th International
Conference, MIT Press (1994) 303–320
15. Ben-Eliyahu, R., Dechter, R.: Propositional semantics for disjunctive logic pro-
grams. Ann. Math. Artif. Intell. 12 (1994) 53–87
16. Wang, K., Zhou, L.: Comparisons and computation of well-founded semantics for
disjunctive logic programs. ACM Trans. Comput. Logic 6 (2005) 295–327
17. Alcântara, J., Damásio, C.V., Pereira, L.M.: A well-founded semantics with dis-
junction. In M. Gabbrielli, G.G., ed.: Proceedings of the 21st Intl.Conf. on Logic
Programming (ICLP ’05). LNCS 3668, Springer (2005) 341–355
18. Przymusinski, T.: Stationary Semantics for Normal and Disjunctive Logic Pro-
grams. In Delobel, C., Kifer, M., Masunaga, Y., eds.: DOOD ’91, Proceedings of
the 2nd International Conference, Springer, LNCS 566 (1991)
19. Przymusinski, T.C.: Static semantics for normal and disjunctive logic programs.
Annals of Mathematics and Artificial Intelligence 14 (1995) 323–357
20. Baral, C., Lobo, J., Minker, J.: Wf 3 : A semantics for negation in normal dis-
junctive logic programs. In Ras, Z.W., Zemankova, M., eds.: Methodologies for
Intelligent Systems, LNAI 542, Springer (1991) 459–468