Classification of Iterative Fixpoint Semantics for Logic Programs and Deductive Databases

Chitta Baral

Department of Computer Science University of Texas at El Paso El Paso, Texas 79930

1 Introduction

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). It is said to be stratified if there is nor recursion through negation. For stratified and locally stratified normal disjunctive logic programs (which includes normal logic programs) there is a consensus about what such programs mean, namely the perfect model semantics [14]. But there is no consensus about a semantics that can characterize all normal disjunctive logic programs. Several semantics have been proposed to this end [12, 2]. Many of these proposed semantics are based on the iterated fixpoint approach. By iterated fixpoint approach, we mean that the semantics is defined as the fixpoint of an operator, and is obtained by iterating the operator starting from the no meaning state ^{1}, until it reaches a fixpoint. The advantage of the iterated fixpoint approach over other approaches like stable models [10] and stable classes [5] is that top down query processing methods mimicking the iterated fixpoint in reverse can be constructed in most cases [13, 2].

Our goal in this paper is twofold. First, we present a general scheme of semantics based on the iterated fixpoint approach. We propose that the meaning accumulating function, whose iterated fixpoint is defined as the semantics has a prioritized part and may also have a classical part. The exact nature of the different parts is based on the semantic structure that is to be used to accumulate meaning of the program. We show how the semantics based on accumulating functions with only the prioritized part differ from the semantics that are based on functions with both the classical part and the prioritized part. We also show how the semantic structure that is used to accumulate meaning also dictates the nature of the resulting semantics. In section 6, we classify the existing iterated fixpoint semantics based on the general scheme presented in this paper. The advantage of having a general scheme is that database language designers can choose the semantics that is close to their intuition with ease. They could choose an alternative semantics using the general scheme presented in this paper.

1In the no meaning state nothing is known to be true and nothing is known to be false

Second, to accumulate negative information of the program, we extend the concept of negation as failure to be able to characterize falsity of conjunction of atoms. The new concept is referred as generalized negation as failure (GNAF). It is discussed in more detail in section 4.2.

In summary, the main issues we address in this paper are:

1. We present a general scheme for semantics based on the iterated fixpoint approach.

2. We present a classification of various semantics presented in the literature using this scheme.

3. We study common properties among the class of semantics whose meaning accumulating function has only the prioritized part. We state that they are always constructive and when applied to a normal logic program they are equivalent to the well-founded semantics [9].

4. We develop various extensions of negation as failure as a function of the semantic structure used and introduce the concept of generalized negation as failure.

5. We suggest ways to develop alternative semantics using our scheme.

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 clause is a clause where n = 1. A normal logic program is a normal disjunctive logic program that consists of normal 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 [11]. 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 disjunction. 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 conjunction. Let S be a set of atoms. Then by ¬S we mean, {¬x : x ∈ S}. If S is a set of conjunction of atoms, then by ∼ S we mean the set {¬x_{1} ∨ ⋯ ∨ ¬x_{k} : x_{1} ∧ ⋯ ∧ x_{k} ∈ S}. 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 disjunction. 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 disjunction is a tautology. A partial interpretation of a normal disjunctive program program P is a pair < T, F > where T and F are subsets of HB(P). A state of a normal disjunctive program program P is a pair < T_{S}, F_{S} > where T is a subset of EHB(P) and and F is a subset of CHB(P). A g-state (general state) of a normal disjunctive program program P is a subset of GHB(P). To have uniformity we might refer a g-state to be a pair < Dl, C >, where Dl is a set of disjunction of a literal and C is a set of conjunction of atoms.

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}

The semantic structures we consider in this paper include: interpretation (as used in the characterization of van Emden and Kowalski [15]), partial interpretation (as in Well-founded Semantics [9]), state (as in GDWFS [2]) and g-state. For uniformity, we assume that a semantic structure is a pair: a positive semantic structure that is to be used for accumulating positive information and a negative semantic structure to be used for accumulating negative information. The positive semantic structures we consider are T, a set of atoms, D, a set of disjunction of atoms, and Dl, a set of disjunction of literals. The negative semantic structures we consider are F, a set of atoms and C, a set of conjunction of atoms.

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. Truth value with respect to other semantic structures is defined in a similar manner.

The union of two states < D_{1}, C_{1} > and < D_{2}, C_{2} > is defined as < D_{1} ∪ D_{2}, C_{1} ∪C_{2} >. Union and intersection with respect to other semantic structures are defined similarly.

3 Iterated Fixpoint Characterization: An Overview

The iterated fixpoint of a logic program is defined as the iterated fixpoint of a meaning accumulating function. The meaning accumulating function in presence of certain meaning of the program, uses the program to accumulate more meaning of the program. The accumulation process is dependent on the semantic structure used for accumulation. The iterated fixpoint semantics is obtained by iterating the accumulating function F, starting from the no meaning state. Formally, F ↑ 0 = ∅ F ↑ n + 1 = F(F ↑ n) For limit ordinal α, F ↑ α = ⋃_{β<α}(F ↑ β)

If F is continuous, then F ↑ ω is its least fixpoint. If F is monotonic but not continuous, then the iteration results in a fixpoint, which may not be at ω. Otherwise, because of the accumulating nature of F the iteration results in a monotonic sequence and a fixpoint is reached (which may not be the least fixpoint). This fixpoint is referred in the literature [6] as an inflationary fixpoint.

By analyzing the various iterated fixpoint semantics that has been proposed for logic programs, we infer that the meaning accumulating function F may have two distinct parts: a prioritized part and a classical part.

The prioritized part accumulates meaning using the constructive meaning of the rules. Positive information is accumulated by resolving the meaning accumulated so far with the rules present in the program. Negative information is accumulated by using rules similar to negation as failure (NAF) [7]. For example the prioritized part can infer a to be true and b to be false in the program {a ← ¬b} using Negation as Failure. It is also necessary to infer a to be false and b to be true in the programs {a ← ¬b ∧ c, b ← ¬a} and {a ← ¬b ∧ ¬c, b ← ¬a, c}. In section 4, we discuss in detail the prioritized part of the meaning accumulating function based on the particular semantic structure used. We present various resolution approaches to accumulate positive information depending on the semantic structure used. We then present various forms of NAF and its extension generalized negation as failure (GNAF) to accumulate negative information.

The classical part looks at all minimal models of the program and picks out the ones that agree with the meaning accumulated so far (called the agreeing minimal models). Based on the semantic structure used, it then accumulates meaning that can be inferred from all the agreeing minimal models. For example using the classical part p can be inferred to be true and q can be inferred to be false in {p ← a, p ← b, a ← ¬b, b ← ¬a, q ← a ∧ b}. In section 5 we discuss in detail the classical part of the meaning accumulating function.

The meaning accumulating function may only have the prioritized part (like the well-founded semantics [9, 13] ) or may have both the prioritized part and the classical part (like the GWFS [3]). When the function has only the prioritized part, the resulting semantics is constructive. When it has both parts then more meaning is accumulated than when it just has the prioritized part, but the resulting semantics is not constructive. Consider the program, { p ← a; p ← b; a ← ¬b; b ← ¬a; q ← ¬r, ¬p; r ← ¬q}. In this program a semantics that has only the prioritized part will characterize everything as unknown. But a semantics that has both the prioritized part and the classical part will infer p to be true using the classical part (as p is true in all minimal models of the program). Then using the prioritized part it will infer q to be false and r to be true. In section 4 we discuss in detail the properties of semantics that have only the prioritized part. In section 5 we discuss the properties of semantics that have both the prioritized part and the classical part.

4 The Prioritized Part

The meaning accumulating function always has the prioritized part. It may or may not have the classical part. The prioritized part further consists of two distinct accumulators. One that accumulates positive information and the other accumulates negative information. In the next subsection we discuss the positive information accumulator and in section 4.2 we discuss the negative information accumulator.

4.1 Inferring Positive Information

The simplest semantic structure that can be used by the meaning accumulating function is an interpretation. van Emden and Kowalski [15] use it to give a fixpoint characterization of Horn logic programs. According to their characterization, given an interpretation I, an atom A is inferred to be true with respect to a program P, if there is a rule in the ground version of P whose head is A and whose body is true with respect to I.

In the next three subsections we present different methods to accumulate positive information, based on the particular semantic structure used.

4.1.1 When semantic structure is “partial interpretation”

Well-founded semantics [9] and GWFS [3] use partial interpretation as the semantic structure. We denote the positive accumulator of the prioritized part, with respect to partial interpretation as P^{<T,F >}. The superscript of P specifies the particular semantic structure used. Formally, with respect to a normal program P and a partial interpretation < T, F >, P^{<T,F >} is defined as: P^{<T,F >}(< T, F >) = {A : ∃B ← L_{1}, ⋯, L_{m} in P, such that for all i, 1 ≤ i ≤ m, L_{i}θ is true in < T, F >, and A = Bθ for a ground substitution θ}.

4.1.2 When semantic structure is “state”

A state is defined as a pair < D, C > where D is a set of disjunction of atoms and C is a set of conjunction of atoms. The meaning of the state < D, C > is that all disjunctions in D are inferred to be true with respect to the program and all conjunctions in C are inferred to be false with respect to the program. The corresponding positive accumulator is defined as follows: P^{<D,C>}(< D, C >) = { A ∈ EHB(P) : ∃A′ ← B_{1}, ⋯, B_{m}, ¬B_{m+1}, ⋯, ¬B_{n} in P such that for all i, 1 ≤ i ≤ m, (B_{i} ∨ A_{i}) ∈ D, A_{i} might be null, {B_{m+1}, ⋯, B_{n}} ⊆ C and the smallest factor of (A′ ∨ A_{1} ∨ ⋯ ∨ A_{m}) subsumes A. }

Example 4.1 Consider the program {a ∨ b ← c, d, ¬e, ¬f}. Let C = {e, f, g} and D = {c ∨ g, d ∨ h}. Then, P^{<D,C>}(< D, C >) = {a ∨ b ∨ g ∨ h}. □

4.1.3 When semantic structure is “g-state”

A g-state S is a set of disjunction of literals. The corresponding positive accumulator is defined as follows: P^{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, C_{i} might be null, and the smallest factor of (C′ ∨ C_{1} ∨ ⋯ ∨ C_{m}) subsumes C. }

Example 4.2 Consider the program {a ∨ b ← c, d, ¬e, ¬f}. Let S = {c ∨ g, d ∨ h, ¬e ∨ ¬i, ¬f ∨ ¬j}. Then, P^{S}(S) = {a ∨ b ∨ g ∨ h ∨ ¬i ∨ ¬j}. □

4.1.4 Positive Information at ω

In the last three subsections we defined the positive information accumulator for the different semantic structures. We now define the meaning accumulated using that accumulator, given some initial meaning.

Let x be a semantic structure and X be the initial meaning of the program. Then P_{X}^{x} is defined as: P_{X}^{x}(Y) = P^{x}(X ∪ Y).

Proposition 4.1 P_{X}^{x} is monotonic. i.e. If Y_{1} ⊆ Y_{2} then P_{X}^{x}(Y_{1}) ⊆ P_{X}^{x}(Y_{2}). □

Definition 4.1 P_{X}^{x} ↑ 0 = ∅, P_{X}^{x} ↑ (n + 1) = P_{X}^{x}(P_{X}^{x} ↑ n), P_{X}^{x} = ⋃_{n<ω} P_{X}^{x} ↑ n. □

Proposition 4.2 The transfinite sequence {P_{X}^{x} ↑ n} is monotonically increasing and P_{X}^{x} is the least fixpoint of the operator P_{X}^{x}. □

4.2 Inferring Negative Information

In the absence of explicit negative information, negative information is inferred using rules like negation as failure and its variants. Depending on the semantic structure we define a negative information accumulator function whose least fixpoint based on reverse inclusion gives the maximal amount of negative information that can be inferred using the initial meaning. This least fixpoint is obtained by iterating the function downwards starting from the information state where every conjunction of atom is assumed to be false. Fitting [8] uses a different approach where the function is iterated upwards starting from the no meaning state. We now define the negative information accumulator function based on the different semantic structures.

4.2.1 Negation as Failure

In case of the simplest semantic structure, the interpretation, the negative information accumulator is defined using negation as failure [7]. We denote it as NAF^{I}. Formally, an atom can be assumed to be false about a program P using NAF^{I}, and with respect to an interpretation I if for all rules in the ground version of P whose head is A, at least one of the following condition is satisfied:

1. A positive atom in the body of the rule is absent in I.

2. A negative literal in the body of the rule is present in I.

For the semantic structure, the partial interpretation, the corresponding NAF, called NAF^{<T,F >} is defined as: An atom can be assume false about a program P and with respect to an interpretation < T, F >, using NAF^{<T,F >}, if for all rules in the ground version of P whose head is A, at least one of the following condition is satisfied:

1. A positive atom in the body of the rule is present in F.

2. A negative literal in the body of the rule is present in T.

The negative information accumulator, for x ∈ {I, < T, F >}, is then defined as: N_{X}^{x}(Y) = { C : C can be assumed false about P using NAF^{x} and the information state X ∪ Y.}

4.2.2 NAF with respect to < D, F >

When the semantic structure is a state < D, F >, then the corresponding NAF, called NAF^{<D,F_{0}>} is defined as: An atom can be assume false about a program P and with respect to an interpretation < D, F >, using NAF^{<D,F_{0}>}, if for all rules in the ground version of P of the type A ∨ E ← B_{1} ∧ ⋯ ∧ B_{m} ∧ ¬C_{1} ∧ ⋯ ∧ ¬C_{n}, at least one of the following condition is satisfied:

1. E ∨ C_{1} ∨ ⋯ ∨ C_{n} ∈ D

2. ∃i, 1 ≤ i ≤ m|B_{i} ∈ F

A stronger version of NAF^{<D,F_{0}>}, called NAF^{<D,F_{−1}>} is defined by restricting the interaction between atoms in the head of the rule and literals in the body of the rule. This is done by splitting the condition 1 above to two different conditions: 1.1. E ∈ D 1.2. C_{1} ∨ ⋯ ∨ C_{n} ∈ D

The corresponding negative information accumulator, for y ∈ {0, −1} is then defined as: N_{X}^{<D,F_{y}>}(Y) = { C : C can be assumed false about P using NAF^{<D,F_{y}>} and the information state X ∪ Y.}

4.2.3 GNAF with respect to < D, C >

The usual negation as failure rule can not infer falsity of conjunction of atoms without deciding on the falsity of the individual atoms in the conjunction. In this subsection and the next subsection we introduce the concept of generalized negation as failure to infer the falsity of conjunction of atoms, even when the falsity of the individual atoms in the conjunction is not known.

According to GNAF^{<D,C_{0}>} we can assume the conjunction of atoms A_{1} ∧ ⋯ ∧ A_{k} to be false with respect to a program P and state < D, C > 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,

1. E_{1} ∨ ⋯ ∨ E_{k} ∨ B_{1m+1} ∨ ⋯ ∨ B_{1n} ∨ ⋯ ∨ B_{km+1} ∨ ⋯ ∨ B_{kn} ∈ D, or

2. ¬B_{11} ∨ ⋯ ∨ ¬B_{1m} ∨ ⋯ ∨ ¬B_{k1} ∨ ⋯ ∨ ¬B_{km} ∈∼ C In the stronger version of GNAF^{<D,C_{0}>} the interaction between atoms in

the head and literals in the body are restricted. In this stronger version called GNAF^{<D,C_{−1}>}, condition 1 is split into two conditions: 1.1. E_{1} ∨ ⋯ ∨ E_{k} ∈ D, or 1.2. B_{1m+1} ∨ ⋯ ∨ B_{1n} ∨ ⋯ ∨ B_{km+1} ∨ ⋯ ∨ B_{kn} ∈ D.

The corresponding negative information accumulator, for y ∈ {0, −1} is then defined as: N_{X}^{<D,C_{y}>}(Y) = { C : C can be assumed false about P using NAF^{<D,C_{y}>} and the information state X ∪ Y.}

4.2.4 GNAF with respect to g-states

Using GNAF^{Dl_{0}} (also denoted as GNAF^{<Dl,C_{0}>}) ^{2} 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 conjunctions that can be assumed false with respect to a program P and g-state S using GNAF^{<Dl,C_{0}>} is called GNAF^{<Dl,C_{0}>}(P, S). The following example explains GNAF^{<Dl,C_{0}>}(P, S) in more detail.

2A g-state < Dl, C_{0} > in the pair notation is equivalent to Dl ∪ ∼ C_{0} in the original notation of the g-state.

Example 4.3 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^{<Dl,C_{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.

2. 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. 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. 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^{<Dl,C_{0}} > (P_{1}, S). □

GNAF^{<Dl,C_{−1}>} is a stronger version of GNAF^{<Dl,C_{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^{<Dl,C_{−1}>}.

According to GNAF^{<Dl,C_{−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,

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

2. B_{1m+1} ∨⋯∨B_{1n} ∨⋯∨B_{km+1} ∨⋯∨B_{kn} ∨¬B_{11} ∨⋯∨¬B_{1m} ∨⋯∨¬B_{k1} ∨ ⋯ ∨ ¬B_{km} ∈ 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, or 2.2: ¬B_{11} ∨ ⋯ ∨ ¬B_{1m} ∨ ⋯ ∨ ¬B_{k1} ∨ ⋯ ∨ ¬B_{km} ∈ S. We refer this stronger version of GNAF as GNAF^{<Dl,C_{−2}>}.

The corresponding negative information accumulator, for y ∈ {0, −1, −2} is then defined as: N_{X}^{<Dl,C_{y}>}(Y) = { C : C can be assumed false about P using NAF^{<Dl,C_{y}>} and the information state X ∪ Y.}

4.2.5 Negative information at ω

Proposition 4.3 Let x be an semantic structure. N_{X}^{x} is monotonic. i.e. If Y_{1} ⊆ Y_{2} then N_{X}^{x}(Y_{1}) ⊆ N_{X}^{x}(Y_{2}). □

Definition 4.2 N_{X}^{x} ↓ 0 = CHB(P); N_{X}^{x} ↓ (n + 1) = N_{X}^{x}(N_{X}^{x} ↓ n) N_{X}^{x} = ⋂_{n<ω} N_{X}^{x} ↓ n □

Proposition 4.4 The transfinite sequence {N_{X}^{x} ↓ n} is monotonically increasing and the set N_{X}^{x} is the least fixpoint of the operator N_{X}^{x} based on reverse ordering. □

4.3 Semantics with only the prioritized part

Semantics that have only the prioritized part, are defined based on an accumulating function that accumulates positive and negative information ussing two different accumulators. Formally, The accumulating function F^{x} with respect to the semantic structure x is defined as follows: F^{x}(X) = X ∪ (P_{X}^{x}, N_{X}^{x})

Theorem 1 Let x be any semantic structure that is more general than an interpretation and is mentioned in Section 2. F^{x} is monotonic. □

Definition 4.3 Let M_{0}^{x} = ∅; For successor ordinals, M_{α+1}^{x} = F^{x}(M_{α}^{x}) and for limit ordinal α, M_{α}^{x} = ⋃_{β<α} M_{β}^{x}. □

Since the sequence {M_{α}^{x}} is monotonically increasing there exists a smallest countable ordinal δ such that M_{δ}^{x} is the fixpoint of the operator F^{x}. We call this fixpoint M_{P}^{x} refer to it as the x-well-founded semantics of P.

Theorem 2 Let x be any semantic structure that is more general than an interpretation and is mentioned in Section 2. For a normal disjunctive logic program P, M_{P}^{x} is consistent and is the least fixpoint of F^{x}. □

Theorem 3 For normal programs x-well-founded semantics is equivalent to well-founded semantics, when x is a partial interpretation, state or a g-state and for all version of the NAF and GNAF. □

5 The Classical Part

Compared to the prioritized part the definition of the classical part is much simple. Due to lack of space we just give a model theoretic characterization of the classical part. Syntactic characterization of the classical part will be given in the full paper. Interested reader might refer to [3, 2] for syntactic characterization of the classical part of GWFS and GDWFS.

Let x be the semantic structure and let x_{p} the positive part of the semantic structure and x_{n} be the negative part of the semantic structure. Let X be the meaning accumulated so far. Then, P_{X}^{Cl,x} is defined as all structures of the type x_{p} that are true in all those minimal models of P that agree with X. Similarly, N_{X}^{Cl,x} is defined as all structures of the type x_{n} that are false in all those minimal models of P that agree with X.

Example 5.1 Consider the program {p ← a, p ← b, a ← ¬b, b ← ¬a, q ← a ∧ b}. With respect to the semantic structure < T, F >, P_{X}^{Cl,<T,F >} = {p} and N_{X}^{Cl,<T,F >} = {q}. But P_{X}^{Cl,<D,C>} = {p, a ∨ b} and N_{X}^{Cl,<D,C>} = {q, a ∧ b}, as a ∨ b is true in all minimal models of the program and a ∧ b is false in all minimal models of the program. □

5.1 Semantics with both classical and prioritized part

The semantics with both classical and prioritized part is defined as the iterated fixpoint of the operator F^{x,y}, where x is the semantic structure used in the prioritized part and y is the semantic structure used in the classical part. F^{x,y}(W) = W ∪ (P_{W}^{x} , N_{W}^{x}) ∪ (P_{W}^{Cl,y}, N_{W}^{Cl,y}).

But we have to be careful about programs like: {p ← ¬p}. Assume that < T, F > is the semantic structure that is being used. A semantics that has both classical and prioritized part, will infer p to be true using the classical part in the first iteration. But in the next iteration it will infer p to be false using the prioritized part and the initial meaning that p is true. To avoid such inconsistencies we redefine P_{W}^{x} and N_{W}^{x} so that they only assign truth value to structures that are not assigned the value true or false until that iteration. Because of this modification F^{x,y} is not monotonic and its iterated fixpoint may not be the least fixpoint. In the rest of the paper when we discuss F^{x,y}, we mean the modified version of it.

Definition 5.1 Let M_{0}^{x,y} = ∅; For successor ordinals, M_{α+1}^{x,y} = F^{x,y}(M_{α}^{x,y}) and for limit ordinal α, M_{α}^{x,y} = ⋃_{β<α} M_{β}^{x,y}. □

Since the sequence {M_{α}^{x,y}} is monotonically increasing there exists a smallest countable ordinal δ such that M_{δ}^{x,y} is the fixpoint of the operator F^{x,y}. We call this fixpoint M_{P}^{x,y} refer to it as the x, y-generalized well-founded semantics of P.

6 Classification of Existing Semantics

In this section we classify some of the existing semantics in the literature based on the general schema presented in the paper. To make the direction of iteration explicit we have added ↑ and ↓ by the side of the semantic structures. Except Fitting and Jacob’s semantics the direction of iteration is same for all other semantics: positive information is obtained by upward iteration and negative information is obtained by downward iteration. In Fitting and Jacob’s semantics positive and negative information is obtained alternatively by upward iterations. Hence, the difference in notation between well-founded semantics and Fitting and Jacob’s semantics. It should be note that extensions to Fitting and Jacob’s semantics using different semantic structures can easily be constructed. We now enumerate the notation of accumulating functions of the various semantics in the literature. Two of these semantics (DWFS and WF^{3} semantics) are new and are developed using the general scheme presented in this paper. Due to lack of space they are not discussed in this paper. They are described in detail in our thesis [1].

1. van Emden and Kowalski’s T_{P} operator: F^{I↑}

2. Minker and Rajasekar’s T_{P}^{I} operator: F^{D↑}

3. Well-founded Semantics [9] : F^{<T ↑,F ↓>}

4. GWFS [3] : F^{<T ↑,F ↓><T,F >}

5. GDWFS [2] : F^{<D↑,F_{−1}↓><D,C>}

6. WF^{3} semantics [1] : F^{<D↑,C_{−1}↓><D,C>}

7. DWFS [1] : F^{<Dl↑,C_{0}↓>}

8. Stationary Semantics [12] ^{3} : F^{<D↑,C_{−1}↓>}

9. Fitting and Jacob’s semantics [8]: F\overline{<T ↑,F ↑>}

7 Conclusion

In this paper we have presented a general scheme of semantics of logic programs based on the iterated fixpoint approach. We hope that this will change the direction of research in logic programming semantics from “what my semantics does is most intuitive” to “how to get a semantics that agrees with most of my intuition”. We have considered the iterated fixpoint approach because of its success with finding equivalent procedural methods. To find a general procedural method that can mimic any iterated fixpoint semantics derivable from the scheme presented in this paper is our next goal.

3This is based on our understanding of Stationary semantics. We are still in the process of substantiating our belief.

Another general scheme of semantics based on the idea of stable models is defined in [4]. Their it is shown that various orderings on strict stable classes can generate various semantics including the stable model semantics [10], stable class semantics [5] and well-founded semantics. But the possibility of having equivalent procedural methods based on these ordering (besides the well-founded semantics) is still an open problem.

References

[1] C. Baral. Issues in Knowledge Representation: Semantics and Knowledge Combination. Ph.D thesis, University of Maryland, August 1991.

[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] C. Baral, J. Lobo, and J. Minker. Generalized well-founded semantics for logic programs. In 10th International Conference on Automated Deduction, West Germany, 1990.

[4] C. Baral and V. S. Subrahmanian. Duality between alternative semantics of logic programs and nonmonotonic formalisms. To be presented the International Workshop in logic programming and nonmonotonic reasoning.

[5] C. Baral and V. S. Subrahmanian. Stable and Extension Class Theory for Logic Programs and Default Logics. Technical Report CS-TR-2402, Dept of Computer Science, University of Maryland, February 1990. To appear in Journal of Automated Reasoning.

[6] A. Chandra and D. Harel. Horn Clause Queries and Generalizations. Journal of Logic Programming, 2(1):1–15, April 1985.

[7] K. L. Clark. Negation as Failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293–322. Plenum Press, New York, 1978.

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

[9] Van Gelder, K. Ross, and Schlipf. 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.

[10] M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In R.A. Kowalski and K.A. Bowen, editors, Proc. 5^{th} International Conference and Symposium on Logic Programming, pages 1070–1080, Seattle, Washington, August 15-19, 1988.

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

[12] T. Przymusinski. Stationary semantics for disjunctive logic programs and deductive databases, 1990. Research report, University of texas at El Paso.

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

[14] T.C. Przymusinski. Perfect Model Semantics. In R.A. Kowalski and K.A. Bowen, editors, Proc. 5^{th} International Conference and Symposium on Logic Programming, pages 1081–1096, Seattle, Washington, August 15-19, 1988.

[15] M.H. van Emden and R.A. Kowalski. The Semantics of Predicate Logic as a Programming Language. J.ACM, 23(4):733–742, 1976.