Generalized Negation As Failure and Semantics of Normal Disjunctive Logic Programs

Chitta Baral

Department of Computer Science University of Texas at El Paso El Paso, Texas, 79968 chitta@cs.ep.utexas.edu

Abstract

We introduce the concept of generalized negation as failure (GNAF) to infer the falsity of a conjunction of atoms when the individual atoms can not be inferred to be false. Using GNAF, we present disjunctive well-founded Semantics (DWFS), a constructive extension of well-founded semantics, to the class of normal disjunctive logic programs. We also use an extension of Rajasekar and Minker’s fixpoint operator for disjunctive logic programs [8] to be able to infer the truth of disjunctions of literals. Our semantics is equivalent to well-founded semantics for normal logic programs. For disjunctive programs (i.e. without negation in their bodies) it gives a fixpoint characterization of Minker’s GCWA [7]. It differs from Stationary semantics [9] by assigning the truth value false to A, in the program {A∨B ← ¬C; B∨C}. It also differs from the Generalized Disjunctive Well-Founded semantics by Baral et al. [2] and well-founded semantics for normal disjunctive logic programs given by Ross [11].

1 Motivation and Introduction

Well-founded semantics was developed by Van Gelder et al. [5] to characterize all normal logic programs. They assume an atom A to be false with respect to a partial interpretation I and a program P, if for all rules with A in its head the body is false with respect to I. In this paper we extend this notion of negation as failure ^{1} to be able to infer the falsity of conjunction of atoms, even when none of the individual atoms in the conjunction can be assumed false. We refer to our extension as generalized negation as failure (GNAF) and use it to give a constructive iterated fixpoint semantics of normal disjunctive logic programs, called the disjunctive well-founded semantics (DWFS).

DWFS is similar to the stationary semantics [9]. The main feature of DWFS is its definition in terms of GNAF. In the absence of GNAF, stationary semantics [9] is defined using Minker’s GCWA and a modal operator. The iterated fixpoint semantics of DWFS closely follows the iterated fixpoint semantics [10] of well-founded semantics and uses disjunction of literals to capture truth, and conjunction of literals to capture falsity. Moreover, it behaves exactly like the well-founded semantics (at each iteration level) when applied to normal logic programs.

1a variant of the original negation as failure

Recently there has been lot of interests in disjunctive logic programs and its semantics [8, 2, 12]. This is because, disjunctive logic programs can represent disjunctive information naturally. For example, if we know that Fred is either a bird or a mammal, and both mammals and birds are living beings, then we should be able to conclude that Fred is a living being. If there is no reason for us to prefer between the possibilities of Fred being a bird or a mammal we can not represent this information as a normal Horn program consisting of the clause bird(F red) ← ¬mammal(F red) or the clause mammal(F red) ← ¬bird(F red). Also, using a constructive semantics we can not infer bird(F red) ∨ mammal(F red) from the program consisting of both the clauses bird(F red) ← ¬mammal(F red) and mammal(F red) ← ¬bird(F red). Hence a natural way to represent this information is the disjunctive clause bird(F red) ∨ mammal(F red).

Normal disjunctive logic programs allow negation in their bodies. Formally, a normal disjunctive logic program is a set of clauses of the form A_{1} ∨ ⋯ ∨ A_{n} ← L_{1} ∧ ⋯ ∧ L_{m}, where the A’s are atoms and the L’s are literals. Disjunctive Well-founded Semantics as proposed in this paper differs from other semantics proposed for normal disjunctive logic programs. It differs from Generalized Disjunctive Well-Founded Semantics [2], and W F^{3} semantics [1], by being more constructive in its approach. Disjunctive Well-founded Semantics does not infer p to be true in the programs {p ← ¬p}, {p ← a; p ← ¬a} and {p ← a; p ← b; a ← ¬b; b ← ¬a}. It differs from Ross’s extended well-founded semantics [11] by being able to characterize p to be true in {p ← ¬a; p ← ¬b; a ∨ b}. It differs from the stationary model semantics of Przymusinski [9] by being able to characterize p to be false in {p ∨ q ← ¬r; q ∨ r}.

The rest of the paper is organized as follows. In the next section we present various definition used in the rest of the paper. In section 3, we introduce generalized negation as failure (GNAF) and explain it through examples. In section 4 we define the iterated fixpoint characterization of disjunctive well-founded semantics (DWFS) using GNAF. In section 5 we compare DWFS with other semantics using various benchmark programs.

2 Definitions

A normal disjunctive logic program is a finite set of clauses (sometimes referred as rules) of the form

A_{1} ∨ … ∨ A_{n} ← L_{1} ∧ … ∧ L_{m}

where n ≥ 1, m ≥ 0, the As are atoms and the Ls are literals (i.e. positive or negated atoms). A normal Horn clause is a clause where n = 1. A normal Horn logic program or a normal logic program is a normal disjunctive logic program that consists of normal Horn clauses. We use the term program to refer to both logic programs and normal disjunctive logic programs.

For a program P, the Herbrand universe U_{P}, the Herbrand base HB(P), a Herbrand interpretation, a Herbrand model, a model and a minimal model are defined as in Lloyd’s book [6]. The Extended Herbrand Base of P, EHB(P) is the set of all possible disjunctions of atoms in HB(P). An element of EHB(P) is referred as a positive disjunct. The Conjunctive Herbrand Base of P, CHB(P) is the set of all possible conjunctions of atoms in HB(P). An element of CHB(P) is referred as a conjunct. Let S be a set of atoms. Then by ¬S we mean, {¬x : x ∈ S}. If F is a set of conjuncts then by ∼ F we mean, {¬A_{1} ∨ ⋯ ∨ ¬A_{k} : A_{1} ∧ ⋯ ∧ A_{k} ∈ F }. The Negative Herbrand Base of P, NHB(P) is the set of all possible disjunctions of negated atoms in (¬(HB(P)). An element of NHB(P) is referred as a negative disjunct. The General Herbrand Base of P, GHB(P) is the set of all possible disjunctions of literals in HB(P)∪¬(HB(P)) such that no disjunct is a tautology. A g-state (general state)^{2} of a normal disjunctive program program P is a subset of GHB(P).

Example 2.1 Let P be {a ← b; b} HB(P) = {a, b} EHB(P) = {a, b, a ∨ b} ¬HB(P) = {¬a, ¬b} NHB(P) = {¬a, ¬b, ¬a ∨ ¬b} GHB(P) = {a, b, a ∨ b, ¬a, ¬b, ¬a ∨ ¬b, a ∨ ¬b, b ∨ ¬a}

Definition 2.1 For a set S of ground clauses, can(S) = {C | C ∈ S and ∄C′ s.t. C′ ∈ S and C′ is a subclause of C}

Definition 2.2 Let S be a set of disjunctions of literals. lit(S) is defined as the set of literals that are present in the disjunctions in S.

Example 2.2 Let S = {a ∨ ¬b, ¬c ∨ d ∨ ¬a}, then lit(S) = {a, ¬b, ¬c, d, ¬a}

A set of conjuncts {C_{1}, …, C_{m}} delimited by [ and ] denotes the set of all conjuncts C that logically imply some conjunct C_{i}.

Example 2.3 For example, if HB(P) = {a, b, c} then, [a, b ∧ c] = {a, a ∧ b, a ∧ c, b ∧ c, a ∧ b ∧ c}. ∼ [a, b ∧ c] = {¬a, ¬a ∨ ¬b, ¬a ∨ ¬c, ¬b ∨ ¬c, ¬a ∨ ¬b ∨ ¬c}.

For any formula F and a consistent g-state S, val_{S}(F) is true(false) if F is true(false) in all minimal Herbrand models of S. Otherwise it is unknown.

3 Generalized Negation As Failure

Consider the program P: p ← ¬a p ← ¬b a ∨ b This program is stratified and p is true with respect to the perfect model semantics. Since the program is stratified we can assume a ∧ b to be false by GCWA if we only consider the clause a∨b. We can not assume a∧b to be false by GCWA if we consider the whole program. Since the well-founded semantics considers the whole program at each stage it uses variants of negation as failure to infer the falsity of atoms. Przymusinski [9] uses modal operators in the program to be able to infer the falsity of a ∧ b by using GCWA on the transformed program. We propose the concept of GNAF as an extension to negation as failure to be able to infer a ∧ b to be false.

2Belegrinos [3] was the first to use the concept of a g-state. He calls a g-state a partial interpretation.

For a disjunctive deductive database without any rules GNAF is very similar to the syntactic definition of GCWA. According to it, we can infer a ∧ b to be false with respect to the database D if for all pairs of disjunction of atoms a ∨ X and b ∨ Y in D, X ∨ Y is also in D. Extending this to disjunctive deductive database with rules, we can infer a ∧ b to be false with respect to the database D and a g-state S if for all pairs of rules of the type a ∨ X ← U and b ∨ Y ← V in D, either X ∨ Y is also in D or U ∧ V is false in S.

In program P, the only rule with a in its head is a ∨ b (i.e. X = b). Similarly, the only rule with b in its head is b ∨ a (i.e. Y = a). Hence, we can assume a ∧ b to be false if X ∨ Y is true in P; i.e. if a ∨ b is true in P. Since, a ∨ b is in P, we can assume a ∧ b to be false.

We will now define various versions of GNAF.

3.1 GNAF or GNAF_{0}

According to GNAF_{0} we can assume the conjunction of atoms A_{1} ∧ ⋯ ∧ A_{k} to be false with respect to a program P and g-state S, if for all sets of ground instances of rules of the type RS =

{A_{1} ∨ E_{1} ← B_{11}, ⋯, B_{1m}, ¬B_{1m+1}, ⋯, ¬B_{1n},
⋮
A_{k} ∨ E_{k} ← B_{k1}, ⋯, B_{km}, ¬B_{km+1}, ⋯, ¬B_{kn} }

where RS is a subset of the set of ground instances of rules in P, E_{1} ∨ ⋯ ∨ E_{k} ∨ B_{1m+1} ∨ ⋯ ∨ B_{1n} ∨ ⋯ ∨ B_{km+1} ∨ ⋯ ∨ B_{kn} ∨ ¬B_{11} ∨ ⋯ ∨ ¬B_{1m} ∨ ⋯ ∨ ¬B_{k1} ∨ ⋯ ∨ ¬B_{km} ∈ S The set of conjuncts that can be assumed false with respect to a program P and g-state S using GNAF_{0} is called GNAF_{0}(P, S). The following example explains GNAF_{0}(P, S) in more detail.

Example 3.1 Consider the following logic program P_{1} :

r_{1} : a ∨ c_{1} ← f_{1}

r_{2} : a ∨ c_{2} ← f_{2}, g_{1}
r_{3} : b ∨ d_{1} ← ¬e_{1}, g_{2}
r_{4} : b ∨ d_{2} ← f_{3}

Let S = {c_{1} ∨ d_{1} ∨ e_{1} ∨ ¬g_{2}, ¬f_{1} ∨ ¬f_{3}, c_{2} ∨ e_{1} ∨ ¬g_{1}, ¬g_{1} ∨ ¬f_{3}} We now show that how a ∧ b ∈ GNAF_{0}(P_{1}, S). In the program P_{1}, the atom a is present in the head of the rules r_{1} and r_{2} and b is present in the head of the rules r_{3} and r_{4}. Hence, a and b can be simultaneously true only if there are rules with a and b in their head (not necessarily the same rules) which will enable us to assume a and b to be true. In the program P_{1} there are four sets of rules where each set has rules with a and b in their head. These four sets are S_{1} = {r_{1}, r_{3}}, S_{2} = {r_{1}, r_{4}}, S_{3} = {r_{2}, r_{3}} and S_{4} = {r_{2}, r_{4}}.

1. Since, c_{1} ∨ d_{1} ∨ e_{1} ∨ ¬g_{2} is true with respect to S, we can not use S_{1} to assume a and b to be true. This is because, if c_{1} ∨ d_{1} ∨ e_{1} ∨ ¬g_{2} is true with respect to S then at least one of c_{1}, d_{1} or e_{1} is true, or g_{2} is false. If c_{1} is true then r_{1} can not be used to derive a to be true (by minimality considerations), even if the body of r_{1} is true. Similarly if d_{1} is true then r_{3} can not be used to derive b to be true, even if the body of r_{3} is true. If g_{2} is false then the body of r_{3} is false and hence r_{3} can not be used to derive b to be true. Finally, if e_{1} is true then the body of r_{3} is also false and hence r_{3} can not be used to derive b to be true.

2. Similarly, since ¬f_{1} ∨ ¬f_{3} is true with respect to S, we can not use S_{2} to assume a and b to be true.

3. Similarly, since c_{2} ∨ e_{1} ∨ ¬g_{1} is true with respect to S, we can not use S_{3} to assume a and b to be true.

4. Similarly, since ¬g_{1} ∨ ¬f_{3} is true with respect to S, we can not use S_{4} to assume a and b to be true.

Since these are the only possible ways in which we could derive a and b to be true, and none of them is satisfied by the given S and F, hence we can assume a ∧ b to be false. i.e. a ∧ b ∈ GNAF_{0}(P_{1}, S). □

3.2 GNAF_{−1} and GNAF_{−2}

GNAF_{−1} is a stronger version of GNAF_{0} where interaction between atoms in the head of the clause and the literals in in the body of the clause is not allowed. We believe that an equivalent characterization of stationary semantics can be given using GNAF_{−1}.

According to GNAF_{−1} we can assume the conjunction of atoms A_{1} ∧ ⋯ ∧ A_{k} to be false with respect to a program P and g-state S if for all sets of ground instances of rules of the type RS =

{A_{1} ∨ E_{1} ← B_{11}, ⋯, B_{1m}, ¬B_{1m+1}, ⋯, ¬B_{1n},
⋮
A_{k} ∨ E_{k} ← B_{k1}, ⋯, B_{km}, ¬B_{km+1}, ⋯, ¬B_{kn} }

where RS is a subset of the set of ground instances of rules in P, at least one of the following two conditions hold:

1. E_{1} ∨ ⋯ ∨ E_{k} ∈ S

2. B_{1m+1} ∨⋯∨B_{1n} ∨⋯∨B_{km+1} ∨⋯∨B_{kn} ∨¬B_{11} ∨⋯∨¬B_{1m} ∨⋯∨¬B_{k1} ∨⋯∨¬B_{km} ∈ S The set of conjuncts that can be assumed false with respect to a program P and g-state S using GNAF_{−1} is called GNAF_{−1}(P, S). Still stronger versions of GNAF can be defined by separating the positive and negative literals in step 2 of the previous definition. i.e. Step 2 can be split into the two conditions: 2.1. B_{1m+1} ∨ ⋯ ∨ B_{1n} ∨ ⋯ ∨ B_{km+1} ∨ ⋯ ∨ B_{kn} ∈ S 2.2. ¬B_{11} ∨ ⋯ ∨ ¬B_{1m} ∨ ⋯ ∨ ¬B_{k1} ∨ ⋯ ∨ ¬B_{km} ∈ S. We refer this stronger version of GNAF as GNAF_{−2}.

3.3 Other aspects of GNAF

Due to lack of space, we do not discuss other aspects of GNAF in this paper. These aspects deal with the relationship between GNAF and Clark’s completion of particular Horn translations of the disjunctive program and the difference between GNAF and GCWA.

4 Fixpoint Characterization of DWFS

The fixpoint characterization of disjunctive well-founded semantics is based on the operator S which operates on a g-state S. S is formally defined as : S(S) = S ∪ T_{S} ∪ F_{S}. T_{S} is the maximal g-state that can be assumed to be true from P by knowing S. F_{S} is the maximal set of negative disjuncts (i.e. disjunction of negative literals) that can be assumed true (i.e. the maximum set of conjuncts that can be assumed false) from P by knowing S. We give a fixpoint characterization of T_{S} and F_{S}. As will be seen, stationary semantics, defined by Przymusinski [9] is similar to our semantics. However, Przymusinski defines F_{S} and T_{S} using a modal operator and the Generalized Closed World Assumption [7]. Similar to the well-founded semantics our goal is to minimize the truth of positive disjuncts and maximize the falsity of conjuncts. Although Przymusinski [9] has a similar goal, his stationary semantics assumes a to be unknown in the program {a ∨ b ← ¬c; b ∨ c}, while our semantics characterizes a to be false. We will further discuss differences between these two semantics in the last section of the paper.

We now explain T_{S} and F_{S}. T_{S} is the least fixpoint of the operator T_{S} obtained by iterating it starting from the empty set, until a fixpoint is reached. The operator T_{S} is similar to the operator T_{P}^{I} defined by Minker and Rajasekar for the fixpoint semantics of disjunctive programs [8]. For a g-state s, T_{S}(s) outputs the set of disjuncts that can be assumed to be true about P by knowing S ∪ s, in one step of reasoning. F_{S} is the least fixpoint (based on reverse inclusion) ^{3} of the operator F_{S} obtained by iterating it starting from NHB(P), the set of all possible negative disjuncts, until a fixpoint is reached. The operator F_{S} is similar to the operator F_{I} used in the well-founded semantics [10]. For a g-state s, F_{S}(s) outputs the set of negative disjuncts that can be assumed to be true about P (i.e., the corresponding conjunction of atoms can be assumed false) by using generalized negation as failure and knowing S ∪ s, in one step of reasoning. More formally,

3According to reverse inclusion a ≤ b iff b ⊆ a

Definition 4.1 Let S and s be g-states of a normal disjunctive logic program P. T_{S}(s) = { C ∈ GHB(P) :∃C′ ← B_{1}, ⋯, B_{m} is a ground instance of a rule in P such that for all i, 1 ≤ i ≤ m, (B_{i} ∨ C_{i}) ∈ S ∪ s, C_{i} might be null, and the smallest factor of (C′ ∨ C_{1} ∨ ⋯ ∨ C_{m}) subsumes C. }

F_{S}(s) = { G ∈ NHB(P) : For all sets of ground instances of rules of the type RS =

{A_{1} ∨ E_{1} ← B_{11}, ⋯, B_{1m}, ¬B_{1m+1}, ⋯, ¬B_{1n},
⋮
A_{k} ∨ E_{k} ← B_{k1}, ⋯, B_{km}, ¬B_{km+1}, ⋯, ¬B_{kn} }

where ¬(A_{1} ∧ ⋯ ∧ A_{k}) subsumes ¬G and RS is a subset of the set of ground instances of rules in P, E_{1} ∨ ⋯ ∨ E_{k} ∨ B_{1m+1} ∨ ⋯ ∨ B_{1n} ∨ ⋯ ∨ B_{km+1} ∨ ⋯ ∨ B_{kn} ∨ ¬B_{11} ∨ ⋯ ∨ ¬B_{1m} ∨ ⋯ ∨ ¬B_{k1} ∨ ⋯ ∨ ¬B_{km} ∈ S ∪ s } □

Example 4.1 Consider the logic program: {p ← ¬b, p ← ¬a, a ∨ b}. Let S = {¬a ∨ ¬b}. T_{S}(∅) = {p ∨ ¬a, p ∨ ¬b, a ∨ b} T_{S}(T_{S}(∅)) = {p, p ∨ ¬a, p ∨ ¬b, a ∨ b} T_{S}(T_{S}(T_{S}(∅))) = {p, p ∨ ¬a, p ∨ ¬b, a ∨ b}

Using GNAF_{0}, F_{S}(s) is same as ∼ GNAF_{0}(P, S ∪ s). The following example explains the operator F_{S} in terms of GNAF_{0}(P, S ∪ s).

Example 4.2 Consider the following logic program P_{1} :

r_{1} : a ∨ c_{1} ← f_{1}

r_{2} : a ∨ c_{2} ← f_{2}, g_{1}
r_{3} : b ∨ d_{1} ← ¬e_{1}, g_{2}
r_{4} : b ∨ d_{2} ← f_{3}

Let s = ∅ and S = {c_{1} ∨ d_{1} ∨ e_{1} ∨ ¬g_{2}, ¬f_{1} ∨ ¬f_{3}, c_{2} ∨ e_{1} ∨ ¬g_{1}, ¬g_{1} ∨ ¬f_{3}}

We show in Example 3.1 that a ∧ b is false in GNAF_{0}(P_{1}, S). Since s = ∅, F_{S}(s) is same as GNAF_{0}(P_{1}, S) and hence a ∧ b is false in F_{S}(s). □

Proposition 4.1 T_{S} and F_{S} as defined in Definition 4.1 are monotonic, i.e. if S_{1} ⊆ S_{2}, then T_{S}(S_{1}) ⊆ T_{S}(S_{2}) and F_{S}(S_{1}) ⊆ F_{S}(S_{2}).

Definition 4.2 T_{S} ↑ 0 = ∅; T_{S} ↑ (n + 1) = T_{S}(T_{S} ↑ n); T_{S} = ⋃_{n<ω} T_{S} ↑ n. F_{S} ↓ 0 = NHB(P); F_{S} ↓ (n + 1) = F_{S}(F_{S} ↓ n); F_{S} = ⋂_{n<ω} F_{S} ↓ n. □

Proposition 4.2 The transfinite sequence {T_{S} ↑ n} is monotonically increasing and the transfinite sequence {F_{S} ↓ n} is monotonically increasing. The set T_{S} is the least fixpoint of the operator T_{S} and the set F_{S} is the least fixpoint of the operator F_{S}. ^{4}

Definition 4.3 Let S be the operator that assigns to every g-state S of P a new g-state S(S) defined by : S(S) = S ∪ T_{S} ∪ F_{S}, where T_{S} and F_{S} are as defined in Definition 4.2. □

Theorem 1 S as defined in Definition 4.3 is monotonic.

Definition 4.4 Let M_{0} = ∅; For successor ordinals, M_{α+1} = S(M_{α}), where S is as defined in Definition 4.3. For limit ordinal α, M_{α} = ⋃_{β<α} M_{β} □

Since the sequence {M_{α}} is monotonically increasing there exists a smallest countable ordinal δ such that M_{δ} is the fixpoint of the operator S. We call this fixpoint M_{P}^{S} and refer to it as the Disjunctive Well-founded state of P.

Theorem 2 For a normal disjunctive logic program P, M_{P}^{S}, its Disjunctive Well-founded state is consistent and is the least fixpoint of the operator S as defined in Definition 4.3.

Example 4.3 Consider the program: r_{1} : A_{1} ∨ E_{1} ← B_{1}, ¬C_{1} r_{2} : A_{2} ∨ E_{2} ← ¬C_{2} r_{3} : E_{1} ∨ E_{2} ∨ C_{1} ∨ C_{2} ← ¬D_{1} r_{4} : B_{1} ∨ D_{1} Since the only rules with B_{1} or D_{1} in the head is r_{4}, F_{M_{0}} contains ¬B_{1} ∨ ¬D_{1}. Hence, M_{1} = {B_{1} ∨ D_{1}, ¬B_{1} ∨ ¬D_{1}} Now consider T_{M_{1}}. T_{M_{1}} ↑ 0 = ∅ T_{M_{1}} ↑ 1 = {B_{1} ∨ D_{1}} T_{M_{1}} ↑ 2 = {B_{1} ∨ D_{1}, E_{1} ∨ E_{2} ∨ C_{1} ∨ C_{2} ∨ ¬B_{1}} (Since ¬B_{1} ∨¬D_{1} ∈ M_{1}, by resolving it with r_{3} we obtain E_{1} ∨E_{2} ∨C_{1} ∨C_{2} ∨¬B_{1} ∈ T_{M_{1}} ↑ 2.) T_{M_{1}} = T_{M_{1}} ↑ 2 Consider F_{M_{2}}. It now contains ¬A_{1} ∨ ¬A_{2} as the set of rules {r_{1}, r_{2}} is the only set of rules containing A_{1} and A_{2} in their head respectively. Since E_{1} ∨ E_{2} ∨ C_{1} ∨ C_{2} ∨ ¬B_{1} ∈ M_{2}, hence ¬A_{1} ∨ ¬A_{2} ∈ F_{M_{2}}. Neither GDWFS [2], nor W F^{3} [1] can derive A_{1} ∧ A_{2} to be false with respect to the above program.

4For this operator the ordering is defined as reverse inclusion

Theorem 3 For normal Horn programs disjunctive well-founded semantics coincides with well-founded semantics.

Theorem 4 For disjunctive programs (i.e no negation in the body of a program clause) the semantics is equivalent to Rajasekar and Minker’s [8] semantics. That is, for such a program P, T_{M_{0}} = lfp(T_{P}^{I}) and F_{T_{M_{0}}} = GCW AC(P), where GCW AC(P) = {¬a_{1} ∨ ⋯ ∨ ¬a_{k} : a_{1} ∧ ⋯ ∧ a_{k} is false in all minimal models of P. }

Corollary 4.1 For disjunctive programs disjunctive well-founded semantics gives a fixpoint characterization of the GCWA.

5 Discussion and Comparison with other Semantics

In this section we discuss some benchmark programs whose characterizations vary based on the semantics used.

1. Stratifiability of Programs. Consider the following program:

a ← ¬b a ← ¬c b ∨ c This program is stratified and based on its perfect model semantics a is characterized to be true. Ross’s extended well-founded semantics [11] and Baral, Lobo and Minker’s GDWFS [2] do not characterize a to be true. Stationary semantics [9] and disjunctive well-founded semantics (DWFS) both characterize a to be true.

2. Minimality and Upward Constructivity. Perfect model semantics characterizes p to be false in the program {p ← p}. But Fitting et al.’s [4] semantics characterizes p to be unknown. Stationary semantics, GDWFS and DWFS all agree with the perfect model semantics in characterizing this program.

3. Interaction between atoms in the head and the literals in the body. DWFS characterizes a to be false in the program {a ∨ b ← ¬c; b ∨ c}. The stationary semantics assigns the value unknown to a. We argue that, since we know that b ∨ c is true; even if we do not know which one is true one of them is true. If c is true then the first rule in the program can not be fired and we can assume a to be false by negation as failure. If b is true the head of the first rule is true irrespective of the truth value of a. Since that is the only rule with a in its head and we are maximizing falsehood, we should assume a to be false.

Although we advocate the approach taken in DWFS it can be easily modified to be able to behave like the stationary semantics. This can be done by using GNAF_{−1} instead of GNAF_{0} while defining the F_{S} in the fixpoint operator of DWFS. By using GNAF_{−1} the interaction between atoms in the head and the literals in the body of a rule is restricted.

4. Constructivity and Maximally Informativeness. Consider the programs: {p ← ¬a; p ← a}, {p ← a; p ← b; b ← ¬a; a ← ¬b} and {p ← a, b; b ← ¬a; a ← ¬b}. In constructive characterization of these programs p is inferred to be unknown. In characterizations that aim to maximize the information content p, is inferred to be true with respect to these programs. While GDWFS characterizes p to be true, stationary semantics and DWFS characterizes p to be unknown.

5. Well-foundedness and Total Well-foundedness. A proposed semantics has the wellfoundedness property if for normal Horn programs the well-founded semantics is a subset of the proposed semantics. That is, the atoms assigned the truth value true or false by the well-founded semantics retain their truth value in the proposed semantics.

A proposed semantics has the total well-foundedness property if for normal Horn programs the well-founded semantics is equivalent to the proposed semantics. Stationary semantics and DWFS are both total well-founded.

6 Conclusion

We develop the concept of generalized negation as failure to infer falsity of conjuncts when the atoms in the conjuncts can not be assumed to be false individually by negation as failure. Based on the interaction between atoms in the head of a rule and the literals in the body of a rule we define various versions of GNAF. Using GNAF we have presented a constructive extension of well-founded semantics for normal logic programs through an iterated fixpoint characterization. We have shown that our disjunctive well-founded semantics is equivalent to well-founded semantics for normal Horn programs and is equivalent to Rajasekar and Minker’s fixpoint semantics [8] for disjunctive programs without negation in their bodies. Our semantics also gives a fixpoint characterization of Minker’s GCWA [7]. We compare our disjunctive well-founded semantics with Przymusinski’s stationary semantics [9] and Ross’s extended well-founded semantics [11]. We also define various semantic properties and benchmark programs corresponding to those properties and compare the different characterizations of the benchmark programs by the different semantics in the literature.

We have developed a procedural counterpart of the the Disjunctive Well-founded semantics as presented in this paper. The procedural characterization is similar to the SLISresolution [2]. Due to lack of space it is not presented in this paper.

Acknowledgements

We wish to express our appreciation to Jack Minker, Jorge Lobo and Yuan Liu for their insightful suggestions. We would also like to acknowledge National Science Foundation for their support of our work under grant number IRI-86-09170, the Army Research Office under grant number DAAG-29-85-K-0-177 and the graduate school of University of Maryland for supporting the author through a dissertation fellowship.

References

[1] C. Baral, J. Lobo, and J. Minker. W F^{3}: A Semantics for Negation in Normal Disjunctive Logic Programs with Equivalent Proof Methods. manuscript.

[2] C. Baral, J. Lobo, and J. Minker. Generalized disjunctive well-founded semantics for logic programs. Technical Report UMIACS TR 90-39, CS TR 2436, Dept of Computer Science, University of Maryland, College Park Md 20742, March 1989. Shorter versions appear in ISMIS 90.

[3] N. Belegrinos. Clausal, Partial Interpretations and the Closed World Assumption. Technical report, Dept of Computer Science, University of Melbourne, 1988.

[4] M. Fitting and M. Ben-Jacob. Stratified and Three-Valued Logic programming Semantics. In R.A. Kowalski and K.A. Bowen, editors, Proc. 5^{th} International Conference and Symposium on Logic Programming, pages 1054–1069, Seattle, Washington, August 15-19, 1988.

[5] Van Gelder, K. Ross, and Schlpif. Unfounded Sets and Well-founded Semantics for General Logic Programs. In Proc. 7^{th} Symposium on Principles of Database Systems, pages 221–230, 1988. to appear in JACM.

[6] J.W. Lloyd. Foundations of Logic Programming. Springer–Verlag, second edition, 1987.

[7] J. Minker. On Indefinite Databases and the Closed World Assumption. In Lecture Notes in Computer Science 138, pages 292–308. Springer-Verlag, 1982.

[8] J. Minker and A. Rajasekar. A Fixpoint Semantics for Disjunctive Logic Programs, 1990. To appear in Journal of Logic Programming.

[9] T. Przymusinski. Stationary semantics for disjunctive logic programs and deductive databases. In North American Conference on Logic Programming, pages 40–62, 1990.

[10] T.C. Przymusinski. Every Logic Program has a Natural Stratification and an Iterated Fixed Point Model. In ”Proceedings of the 8th ACM SIGACT-SIGMOD-SIGART Symposium on Principle of Database Systems”, pages 11–21, 1989.

[11] K. Ross. The well-founded semantics for disjunctive logic programs. In Proc. of the First International Conference on Deductive and Object-oriented databases, pages 352–369, Kyoto, Japan, 1989.

[12] C. Sakama. Possible model semantics for disjunctive databases ii. Presented in the NACLP Workshop on Nonmonotonic Reasoning and Logic Programming.