Stable and Extension Class Theory for Logic Programs and Default Logics

Chitta R. Baral and V.S. Subrahmanian Department of Computer Science A.V. Williams Building University of Maryland College Park, MD 20742, U.S.A. chitta@konark.cs.umd.edu , vs@mimsy.umd.edu

January 12, 1995

Abstract

The stable model semantics (cf. Gelfond and Lifshitz [GL88]) for logic programs suffers from the problem that programs may not always have stable models. Likewise, default theories suffer from the problem that they do not always have extensions. In such cases, both these formalisms for non-monotonic reasoning have an inadequate semantics. In this paper, we propose a novel idea – that of extension classes for default logics, and of stable classes for logic programs. It is shown that the extension class and stable class semantics extend the extension and stable model semantics respectively. This allows us to reason about inconsistent default theories, and about logic programs with inconsistent completions. Our work extends the results of Marek and Truszczynski [MT89b] relating logic programming and default logics.

1 Introduction and Motivation

There has recently been intense interest in the relationship between logic program semantics and non-monotonic reasoning (cf. [MS88, GL88, Prz89a, Prz89b, YL89, MT89b, BF88, Elk89, Gel87]). Most of this work has proceeded in the following way:

1. Given a logic program P, a translation is established by which P is translated into either a default logic theory or into an auto-epistemic logic theory, or into a circumscriptive theory.

2. After this, an equivalence is proved between certain kinds of models for logic programs and certain kinds of structures for the translation of the logic program into autoepistemic or default logic. For example, one may establish a one-one correspondence between supported models of the program and expansions of the auto-epistemic translation of the program (cf. Marek and Subrahmanian [MS88, Gel87]). Or one might establish a one-one correspondence between the stable models of the program and extensions of the default logic translation of the program (cf. [MT89b, BF88, Prz89a]).

However, this approach fails to address an issue that is of importance. For instance:

1. There are logic programs that possess no stable models. In such cases, the one-one correspondence between stable models and extensions of a default logic translation of the program is not very meaningful.

2. there are auto-epistemic theories that possess no expansions.

3. there are default theories with no extensions, and also default theories with no weak extensions.

Despite the fact that such programs, default theories, and auto-epistemic theories exist, many of these programs, default theories, and auto-epistemic theories have a perfectly reasonable meaning. Thus, stable models, extensions and expansions are not powerful enough to characterize the meaning of arbitrary logic programs, default theories and autoepistemic theories, respectively. Our principal aim, in this paper, is to:

1. We first introduce the notion of stable class of a logic program, and demonstrate that every logic program has a stable class. We show that for stratified logic programs the stable class semantics agrees with the stable model semantics. In addition, this notion of stable class characterizes the meaning of logic programs that have inconsistent completions. As we shall demonstrate shortly, such programs can easily arise – and in many cases, they have a reasonable meaning.

2. Analogous to the notion of stable class, we introduce the notions of extension class and weak extension class for default logic.

3. We then demonstrate various equivalences between the stable-class semantics, and the extension class and weak extension class semantics.

In addition to providing a new semantics for default logic that characterizes the meaning of default logic theories that lack extensions, this paper develops strong connections between logic programming and default logics. In addition, we are able to characterize the meaning of logic programs that possess inconsistent completions. We do not deal with auto-epistemic logic in this paper.

2 Stable Classes

Given a set S of sentences, classical logic decrees that the meaning of S is its set of models. In the case of pure logic programs, the set of ground atomic consequences of the program’s completion can be characterized by a single Herbrand model of the program, viz. the least Herbrand model. For general logic programs (cf. Lloyd [Llo84]), the situation is complicated by the fact that the completion of the program may have no model^{1}. Alternatively, it may have several minimal models, but in general, there may be no unique least model.

In order to address this issue, the stable model semantics for logic programs was introduced by Gelfond and Lifschitz [GL88]. Geffner [Gef89] and Baral, Lobo and Minker [BLM89b, BLM89a] also suggested using a class of models as the meaning of a program. The stable class semantics we are going to introduce advocates a class of interpretations (not necessarily models) as the meaning of a logic program. In particular, when programs have stable models, then the stable class semantics captures the stable model semantics as a special case. Furthermore, this approach is applicable to arbitrary programs.

Throughout this paper, we assume, as do Gelfond and Lifshitz [GL88] that P is a (possibly infinite) set of ground clauses. There is no loss of generality in making this assumption since any logic program in the sense of Lloyd [Llo87] may be viewed as such a set of clauses by instantiating all variables occurring in clauses. In addition, we assume that in all program clauses, the negative literals occur after the positive literals. This assumption is also just for the sake of convenience.

1Fitting [Fit86] proves that every logic program has a three valued model using the semantics for three valued logic developed by Kleene. One cause for concern about this semantics is that p is not a logical consequence of the program {p ← q , p ← ¬q , q ← q}. The reason for this is that in three valued logic, tautogies of first order logic are not preserved. Furthermore, connections betweens Fitting’s three valued semantics and non-monotonic logics have not been established, though Przymusinski has established connections between a different three valued logic and non-monotonic reasoning formalisms.

Let M be any Herbrand interpretation. Since we are considering 2-valued interpretations, M is a subset of the Herbrand Base of the language we are considering. P^{M}, the Gelfond-Lifschitz transformation of P with respect to interpretation M, is the logic program P^{M} obtained from P as follows:

(1) eliminate from P each clause whose body contains a negated atom present in M;

(2) from the body of each remaining clause in P, delete all negative literals.

P^{M} is a definite program and hence has a unique least model which is given by T_{P^{M}} ↑ ω. M is said to be a stable model of program P, iff M = T_{P^{M}} ↑ ω.

Example 2.1 If P is the program:

p ← q & ¬s
p ← ¬r

and I = {r} is an Herbrand interpretation, then P^{I} = {p ← q}. □

Definition 2.1 Let A be a set of indices. Let S = {I_{i} | i ∈ A} be a set of interpretations, P^{I_{i}} be the Gelfond-Lifschitz transformation of P w.r.t. interpretation I_{i} and M(P^{I_{i}}) be the unique least Herbrand model of P^{I_{i}}. S is said to be a stable class of program P iff S = {M(P^{I_{i}}) | i ∈ A}.

Some intuition is appropriate here. Suppose, given a program P, we associate an operator F_{P} that maps Herbrand interpretations to Herbrand interpretations such that F_{P} (I) = M(P^{I}). The concept of stable model [GL88] is defined in terms of the fixed point of this operator, i.e. I is a stable model of P iff F_{P} (I) = M(P^{I}) = I. However, this operator may not always have fixed points. Stable model semantics may be viewed as an instance of default logic: if we regard I as a context, then M(P^{I}) corresponds precisely to the set of ground atoms that can be proved (w.r.t. context Cn(I ∪\overline{I})) from the default theory obtained by translating program P using one of the translations of Marek and Truszczysnki [Mar89].

Thus, intuitively, the operator F_{P} computes the set of such provable ground atoms. The basic behind a stable class is that even though F_{P} may have no fixed-points (i.e. F_{P} does not cycle around a single point), there might be a collection of points so that F_{P} cycles around this collection of points.

Example 2.2 Suppose P is the general logic program below:

a ← ¬a
p ←

Then P has two stable classes: S_{0} which is the empty collection of interpretations and S_{1} = {I_{1}, I_{2}} where:

I_{1} = {p}

I_{2} = {a, p}

Thus, P has a unique non-empty stable class, viz. S_{1}, and p is true in all interpretations contained in S_{1}. □

Definition 2.2 S is said to be a strict stable class of a logic program P iff no proper non-empty subset of S is a stable class of P.

Lemmas 1 and 2 given below are immediately proved.

Lemma 1 I is a stable model for P iff the singleton set {I} is a stable class of P. □

Lemma 2 The arbitrary union of stable classes is a stable class. □

We will say more about intersection of stable classes later. In the following definition we define a preference relation between stable classes. We use this preference relation to rule out some stable classes while considering the meaning of a logic program. The main intuition is that some stable classes contain very “large” interpretations. These stable classes should be eliminated, as otherwise, little negative information may be deduced. This leads to the question: What constitutes a “large” interpretation ? The answer is simple and is captured by the super-set relation. Thus, we say a stable class S_{1} is “larger” than a stable class S_{1} iff for each interpretation I_{1} ∈ S_{1} there is a larger interpretation I_{2} ∈ S_{2}. The technical definition is given below. We also demonstrate the usefulness of this relation while describing the stable class semantics of program P_{2} in Example 2.4.

Definition 2.3 (Relation between stable classes) Let S_{1} and S_{2} be stable classes. We say S_{1} ⪯ S_{2} iff (∀c ∈ S_{1}) (∃d ∈ S_{2}) : c ⊆ d. The definition of the relations ≺, ≻ and ⪰ is defined in terms of ⪯ in the usual way.^{2}

A non-empty stable class S is ⪯-minimal iff there is no non-empty stable class S′ ≺ S.

We believe the meaning of a logic program P is the class S(P), where S(P) is the union of all ⪯-minimal strict stable classes of P. A formula is inferred to be true from P if it is true in all interpretations in S(P) and it is inferred to be false from P if it is false in all interpretations in S(P) and otherwise it is assumed to be unknown.

Theorem 1 Every logic program has a non-empty stable class.

Proof.^{3} Consider, F_{P} (I) to be the function M(P^{I}). Because of the nature of the Gelfond-Lifschitz transformation, F_{P} is antimonotonic. i.e. I_{1} ⊆ I_{2} ⇒ F_{P} (I_{2}) ⊆ F_{P} (I_{1}). This is true because if I_{1} ⊆ I_{2} then P^{I_{2}} ⊆ P^{I_{1}}, and since both P^{I_{2}} and P^{I_{1}} are Horn programs, M(P^{I_{2}}) ⊆ M(P^{I_{1}}).

Since, F_{P} is antimonotonic, F_{P}^{2} the function that applies F_{P} twice is monotonic. Let a be the least fixpoint of F_{P}^{2} and b be the greatest fixpoint of F_{P}^{2}. From [Llo87] we know a = glb{x : F_{P}^{2}(x) ≤ x} and b = lub{x : x ≤ F_{P}^{2}(x)}. Let A be the set {x : F_{P}^{2}(x) ≤ x} and B to be the set {x : x ≤ F_{P}^{2}(x)}. Since a ∈ A, F_{P}^{2}(a) ≤ a. i.e. F_{P} (a) ≤ F_{P} (F_{P}^{2}(a)). Hence, F_{P} (a) ∈ B. Since b is an upper bound of B, hence F_{P} (a) ≤ b —(1) By antimonotonicity of F_{P} we have F_{P} (b) ≤ F_{P}^{2}(a). Since a is a fixpoint of F_{P}^{2}, F_{P} (b) ≤ a —(2) Similarly, since b ∈ B, b ≤ F_{P}^{2}(b). i.e. F_{P} (F_{P}^{2}(b)) ≤ F_{P} (b). Hence, F_{P} (b) ∈ A. Since a is a lower bound of A, hence a ≤ F_{P} (b)) —(3) By antimonotonicity of F_{P} we have F_{P}^{2}(b) ≤ F_{P} (a). Since b is a fixpoint of F_{P}^{2}, b ≤ F_{P} (a) —(4) From (2) and (3) we have a = F_{P} (b) and from (1) and (4) we have b = f(a). Hence, {a, b} is a non empty stable class of P. □

Theorem 1 demonstrates that every logic program has a non-empty stable class. In addition, Lemma 1 tells us that if P is any logic program and I is a stable model of P, then the singleton set {I} is a stable class of P. Thus, the stable class semantics is defined for all logic programs that have a stable model, as well as for a logic programs that do not. (as there are many logic programs that do not possess any stable model).

2i.e. a ≺ b iff a ⪯ b and b ⪯̸ a

3This proof was suggested by M. Fitting.

In the following lemmas (Lemmas 3, 4, 5 below), we assume P to be a stratified stratified program and M_{P} to be its unique stable model, where a stratification of P is

P = P_{1} ˙⋃ P_{2} ˙⋃ … ˙⋃P_{n}

Let M_{0} = ∅ and for 1 ≤ i ≤ n, M_{i} = T_{P_{i}} ↑ ω(M_{i−1}). ( as defined in Apt, Blair and Walker [ABW88])

Lemma 3 Suppose k < n. For any interpretation I_{j}, (P_{1} ∪ ⋯ ∪ P_{k})^{I_{j}∩HB(P_{1}∪···∪P_{k})} = (P_{1} ∪ ⋯ ∪ P_{k})^{I_{j}} = {r| head of r is in HB(P_{1} ∪ ⋯ ∪ P_{k}) and r ∈ (P_{1} ∪ ⋯ ∪ P_{k+1})^{I_{j}} } Here, HB(P_{1} ∪ ⋯ ∪ P_{k}) denotes the Herbrand Base of (P_{1} ∪ ⋯ ∪ P_{k}).

Proof.

r ∈ (P_{1} ∪ ⋯ ∪ P_{k})^{I_{j}∩HB(P_{1}∪···∪P_{k})} ⇔ There exists a rule of the form X ← A_{1}, ⋯, A_{u}, ¬B_{1}, ⋯, ¬B_{s} in P_{1} ∪ ⋯ ∪ P_{k},

such that {B_{1}, ⋯, B_{s}} ∩ (I_{j} ∩ HB(P_{1} ∪ ⋯ ∪ P_{k})) = ∅ and r is X ← A_{1}, ⋯, A_{u}. ⇔ There exists a rule of the form X ← A_{1}, ⋯, A_{u}, ¬B_{1}, ⋯, ¬B_{s} in P_{1} ∪ ⋯ ∪ P_{k},

such that {B_{1}, ⋯, B_{s}} ∩ I_{j} = ∅ (Since P is stratified, B_{1}, ⋯, B_{s} must be defined in P_{1} ∪ ⋯ ∪ P_{k}. Hence, {B_{1}, ⋯, B_{s}} ⊆ HB(P_{1} ∪ ⋯ ∪ P_{k})) and r is X ← A_{1}, ⋯, A_{u}.

⇔ r ∈ (P_{1} ∪ ⋯ ∪ P_{k})^{I_{j}} ⇔ There exists a rule of the form X ← A_{1}, ⋯, A_{u}, ¬B_{1}, ⋯, ¬B_{s} in P_{1} ∪ ⋯ ∪ P_{k+1}

such that {B_{1}, ⋯, B_{s}} ∩ I_{j} = ∅ and r is X ← A_{1}, ⋯, A_{u} and head of r is in HB(P_{1} ∪ ⋯ ∪ P_{k}) (by the definition of stratification)

⇔ head of r is in HB(P_{1} ∪ ⋯ ∪ P_{k}) and r ∈ (P_{1} ∪ ⋯ ∪ P_{k+1})^{I_{j}}

□

Lemma 4 For any interpretation I_{j}, T_{(P_{1}∪···∪P_{k})^{I_{j} ∩HB(P_{1}∪···∪P_{k})}} ↑ ω = (T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω) ∩ HB(P_{1} ∪ ⋯ ∪ P_{k})

Proof:

x ∈ (T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω) ∩ HB(P_{1} ∪ ⋯ ∪ P_{k})

⇔ x ∈ HB(P_{1} ∪ ⋯ ∪ P_{k}) and x ∈ T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω ⇔ There exists a rule r of the form x ← A_{1}, ⋯, A_{u} in (P_{1} ∪ ⋯ ∪ P_{k+1})^{I_{j}} such that

head of r is in HB(P_{1} ∪ ⋯ ∪ P_{k}) and {A_{1}, ⋯, A_{u}} ⊆ T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω ⇔ (By the equality of the first and third expressions in Lemma 3) There exists a rule r of the form x ← A_{1}, ⋯, A_{u} in (P_{1} ∪ ⋯ ∪ P_{k})^{I_{j}}

such that head of r is in HB(P_{1} ∪ ⋯ ∪ P_{k}) and by stratification A_{1} ⋯ A_{u} are defined in P_{1} ∪ ⋯ ∪ P_{k} and hence {A_{1}, ⋯, A_{u}} ⊂ T_{(P_{1}∪···∪P_{k})^{I_{j}}} ↑ ω

⇔ x ∈ T_{(P_{1}∪···∪P_{k})^{I_{j}}} ↑ ω ⇔ (using the equality of the first and second expressions in Lemma 3 )

x ∈ T_{(P_{1}∪···∪P_{k})^{I_{j} ∩HB(P_{1}∪···∪P_{k})}} ↑ ω □

Lemma 5 If S = {I_{j}}_{j∈G} is a stable class for (P_{1} ∪ ⋯ ∪ P_{k+1}) then {I_{j} ∩ HB(P_{1} ∪ ⋯ ∪ P_{k})}_{j∈G} is a stable class for P_{1} ∪ ⋯ ∪ P_{k}.

Proof: Consider {T_{(P_{1}∪···∪P_{k})^{I_{j} ∩HB(P_{1}∪···∪P_{k})}} ↑ ω|j ∈ G} Using Lemma 4, this is equal to {(T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω) ∩ HB(P_{1} ∪ ⋯ ∪ P_{k}) |j ∈ G} which is equal to {I_{j} ∩ HB(P_{1} ∪ ⋯ ∪ P_{k})|j ∈ G} (since S is a stable class for P_{1} ∪ ⋯ ∪ P_{k+1}, S = {T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω|j ∈ G}) □

Theorem 2 If P is a stratified logic program then the stable model and the stable class semantics coincide.

Proof. Let P be a stratified logic program and M_{P} be its unique stable model. Since P is stratified let

P = P_{1} ˙⋃ P_{2} ˙⋃ … ˙⋃P_{n}

be a stratification and let M_{0} = ∅ and for 1 ≤ i ≤ n, M_{i} = T_{P_{i}} ↑ ω(M_{i−1}). (as defined in Apt et al. [ABW88])

Without loss of generality we assume P_{1} to be a definite, i.e. negation-free, logic program (possibly empty). We now prove by induction that for all k such that 1 ≤ k ≤ n, {M_{k}} is the unique ⪯-minimal strict stable class of P_{1} ∪ ⋯ ∪ P_{k}.

Base Case (i = 1): Since P_{1} is definite {M_{1}} is the unique ⪯-minimal strict stable class associated with P_{1}.

Induction Hypothesis: (i ≤ k): P_{1} ∪ ⋯ ∪ P_{i} has the unique ⪯-minimal strict stable class {M_{i}}.

Induction: (i = k + 1) We want to show that P_{1} ∪ ⋯ ∪ P_{k+1} has the unique ⪯-minimal strict stable class {M_{k+1}}.

Let S = {I_{j}}_{j∈G} be any strict stable class for P_{1} ∪⋯∪P_{k+1}. It suffices to show that ∀j ∈ G M_{k+1} ⊆ I_{j}.

Consider {I_{j} ∩ HB(P_{1} ∪ ⋯ ∪ P_{k})}_{j∈G} By Lemma 5 this is a stable class for P_{1}∪⋯∪P_{k}. Since by the induction hypothesis {M_{k}} is the unique stable class of P_{1}∪⋯∪P_{k}, we may conclude that ∀j ∈ G(I_{j} ∩HB(P_{1}∪⋯∪P_{k}) = M_{k}). (1)

Let A ∈ M_{k+1} − M_{k}. (From (1) we know that M_{k} ⊆ I_{j}). This means that there exists an integer u such that A ∈ T_{P_{k+1}} ↑ u(M_{k}). We prove by induction on u that ∀j ∈ G(A ∈ I_{j}).

Base Case (u = 1): i.e. A ∈ T_{P_{k+1}} ↑ 1(M_{k}). This means that there exists a rule of the form A ← B_{1}, ⋯, B_{r}, ¬D_{1}, ⋯, ¬D_{m} in P_{k+1} where {B_{1}, ⋯, B_{r}} ⊆ M_{k} and {D_{1} ⋯, D_{m}} ∩ M_{k} = ∅. (2a) For any j ∈ G, {D_{1} ⋯, D_{m}} ∩ I_{j} = {D_{1} ⋯, D_{m}} ∩ I_{j} ∩ HB(P_{1} ∪ ⋯ ∪ P_{k}) (since by stratification {D_{1} ⋯, D_{m}} ⊆ HB(P_{1} ∪ ⋯ ∪ P_{k})) = {D_{1} ⋯, D_{m}} ∩ M_{k} (from (1)) = ∅ (from 2a). This means (∀j ∈ G)A ← B_{1} ⋯, B_{r} is in (P_{1} ∪ ⋯ ∪ P_{k+1})^{I_{j}}. By using Lemma 5 we have that {B_{1}, ⋯, B_{r}} ⊆ M_{k} ⊆ I_{j}, for all j ∈ G. Therefore (∀j ∈ G)A ∈ T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω. As S is a stable class we have {I_{j}}_{j∈G} = {T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω}_{j∈G}. Hence (∀j ∈ G)A ∈ I_{j}.

Induction: (u = v + 1) i.e. A ∈ T_{P_{k+1}} ↑ (v + 1)(M_{k}). This means that there exists a rule of the form A ← B_{1}, ⋯, B_{r}, ¬D_{1} ⋯, ¬D_{m} in P_{k+1} where {B_{1}, ⋯, B_{r}} ⊆ T_{P_{k+1}} ↑ v(M_{k}) and {D_{1} ⋯, D_{m}}∩ T_{P_{k+1}} ↑ v(M_{k}) = ∅; and hence {D_{1} ⋯, D_{m}} ∩ M_{k} = ∅. (2b) For any j ∈ G, {D_{1} ⋯, D_{m}} ∩ I_{j} = {D_{1} ⋯, D_{m}} ∩ I_{j} ∩ HB(P_{1} ∪ ⋯ ∪ P_{k}) (since by stratification {D_{1} ⋯, D_{m}} ⊆ HB(P_{1} ∪⋯∪P_{k})) = {D_{1} ⋯, D_{m}}∩M_{k} (from (1)) = ∅ (from 2b). This means (∀j ∈ G)A ← B_{1} ⋯, B_{r} is in (P_{1} ∪ ⋯ ∪ P_{k+1})^{I_{j}}. By the induction hypothesis, (∀j ∈ G){B_{1}, ⋯, B_{r}} ⊆ I_{j}. Therefore (∀j ∈ G)A ∈ T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω. As S is a stable class we have {I_{j}}_{j∈G} = {T_{(P_{1}∪···∪P_{k+1})^{I_{j}}} ↑ ω}_{j∈G}. Hence (∀j ∈ G)A ∈ I_{j}.

Hence we have ∀j ∈ G, M_{k+1} ⊆ I_{j}. (3)

□

We now prove the stronger statement “If P is a stratified logic program with the unique stable model M then {M} is its unique strict stable class.”

Consider the function F_{P_{1}∪···∪P_{k+1}}. ^{4} By antimonotonicity of F_{P_{1}∪···∪P_{k+1}} and by using (3) above, we have ∀j ∈ G, F_{P_{1}∪···∪P_{k+1}}(I_{j}) ⊆ M_{k+1}. (Since P_{1} ∪ ⋯ ∪ P_{k+1} is a stratified program, M_{k+1} is its stable model and hence F_{P_{1}∪···∪P_{k+1}}(M_{k+1}) = M_{k+1}). Since we initially assume {I_{j}}_{j∈G} to be a stable class of P_{1} ∪ ⋯ ∪ P_{k+}, this means ∀j ∈ G, I_{j} = F_{P_{1}∪···∪P_{k+1}}(I_{k}) for some F_{P_{1}∪···∪P_{k+1}}(M_{k+1}) = M_{k+1}). Since we initially assume {I_{j}}_{j∈G} to be a stable class of P_{1} ∪ ⋯ ∪ P_{k+}, this means ∀j ∈ G, I_{j} = F_{P_{1}∪···∪P_{k+1}}(I_{k}) for some k ∈ G. Hence ∀j ∈ G, I_{j} ⊆ M_{k+1}. (4)

From (3) and (4) we have that ∀j ∈ G, I_{j} = M_{k+1}. Hence, {M_{k+1}} is the only stable class of P_{1} ∪ ⋯ ∪ P_{k+1}.

□ F_{P_{1}∪···∪P_{k+1}}(M_{k+1}) = M_{k+1}).

Since we initially assume {I_{j}}_{j∈G} to be a stable class of P_{1} ∪ ⋯ ∪ P_{k+}, this means ∀j ∈ G, I_{j} = F_{P_{1}∪···∪P_{k+1}}(I_{k}) for some k ∈ G. Hence ∀j ∈ G, I_{j} ⊆ M_{k+1}. (4)

From (3) and (4) we have that ∀j ∈ G, I_{j} = M_{k+1}. Hence, {M_{k+1}} is the only stable class of P_{1} ∪ ⋯ ∪ P_{k+1}.

□

There is a consensus on what the meaning of a stratified logic program should be. Theorem 2 demonstrates the equivalence of the stable class semantics with the consensus semantics of stratified logic programs.

Example 2.3 Consider the program P in Example 2.2. Consider the class {I_{1}, I_{2}} where I_{1} = {p, a} and I_{2} = {p} . M(P^{I_{1}}) = {p} = I_{2} and M(P^{I_{2}}) = {p, a} = I_{1}. Also M(P^{{a}}) = {p} = I_{2} and M(P^{{}}) = {p, a} = I_{1}. Hence the class {I_{1}, I_{2}} is the only non-empty stable class of P, and based on it we can infer p to be true and a to be unknown.

There is a simple graph theoretic intuition that captures stable classes. Define a directed graph whose vertices are the interpretations of our language. Draw an arc from interpretation I_{1} to I_{2} iff I_{2} = M(P^{I_{1}}). In our case, this graph is shown in Figure 1. The strict stable classes correspond precisely to the cycles of our graph. □

4We denote the function M(P^{I}) by F_{P} (I).

{a } {p } ∅ {a, p}

Figure 1: Graphical Representation of Stable Classes

Example 2.4 Consider the programs

P_{1} = {a ← ¬a; p} and
P_{2} = {a ← ¬b; b ← ¬a; p ← a; p ← b}.

Our intuition tells us that p should be true according to the semantics of P_{1}, while a’s truth value should be unknown. Likewise, our intuition tells us that p should be true in the semantics of P_{2}, while both a and b should have an unknown truth value. These are exactly the truth values assigned by the stable class semantics. Figure 1 and Figure 2 show the graphs associated with P_{1} and P_{2}.

Let us now see what actually happens when we consider different semantical characterizations of P_{1} and P_{2}

P_{1} does not have a 2-valued stable model although intuitively p should be true. Thus, the stable model semantics does not capture the precise meaning of P_{1}. P_{2} has two 2-valued stable models {p, a} and {p, b}, which agrees with our intuition. Thus, the stable model semantics captures the intended meaning of P_{2}.

P_{1} has a 3-valued stable model (cf. Przymusinski [Prz90]) which assigns true to p and

{p}  {b} {a} ∅  {p, b} {p, a} {p, a, b}

Figure 2: Graphical Representation: Program P_{2}

unknown to a. This agrees with our intuition. But, P_{2} has three 3-valued stable models M_{1}, M_{2}, M_{3}. The assignment of truth values made by them are:

M_{1}(p) = true , M_{1}(a) = true , M_{1}(b) = false M_{2}(p) = true , M_{2}(a) = false , M_{2}(b) = true M_{3}(p) = M_{3}(a) = M_{3}(b) = unknown

Thus, p is not true in all these three 3-valued stable models, and hence, we cannot conclude, using Przymusinski’s three valued stable semantics, that p is true. Hence, the three valued stable model semantics of P_{2} does not correctly capture our intuition about the meaning of P_{2}.

Hence, neither the stable model semantics, nor the three valued stable model semantics capture the intended meaning of both P_{1} and P_{2}. However, the stable class semantics captures precisely the intended meaning in both cases.

Since the well-founded semantics is equivalent to the three valued stable model semantics [Prz90], the well-founded semantics is also not able to characterize the intuitive meaning of both P_{1} and P_{2}.

P_{1} has a unique ⪯-minimal strict stable class, viz. {{a}, {p, a}}. P_{2} has three strict stable classes, viz. {{p, a}}, {{p, b}} and {∅, {p, a, b}}. Of these, the first two are ⪯-minimal stable classes. Hence, the stable class semantics characterizes the intuitive meaning of P_{2}.

In brief, of the following four semantics: well-founded semantics, stable model semantics, three valued stable model semantics, and stable class semantics, the only semantics which adequately characterizes the meaning of both P_{1} and P_{2} is the stable class semantics. □

Example 2.5 (Van Gelder, [VRS88]) Consider the program, P: q ← ¬r r ← ¬q p ← ¬p p ← ¬r This program has a unique stable model {p, q}. However, it is not intuitively clear that p and q should be true and r should be false in this program. The well-founded model for this program assigns the value “unknown” to p, q and r. We now consider the meaning of the program attributed by S(P), i.e. by the stable class semantics. Let I_{0} = ∅, I_{1} = {p}, I_{2} = {q}, I_{3} = {r}, I_{4} = {p, q}, I_{5} = {p, r}, I_{6} = {r, q}, I_{7} = {p, q, r}. Then: M(P^{I_{0}}) = {p, q, r}. M(P^{I_{1}}) = {p, q, r}. M(P^{I_{2}}) = {p, q}. M(P^{I_{3}}) = {p, r}. M(P^{I_{4}}) = {p, q}. M(P^{I_{5}}) = {r}. M(P^{I_{6}}) = {p}. M(P^{I_{7}}) = {}. This program has three strict stable classes, C_{1}, C_{2} and C_{3} where C_{1} = {{q, p}} = {I_{4}}, C_{2} = {∅, {p, q, r}} = {I_{0}, I_{7}} and C_{3} = {{r}, {r, p}} = {I_{3}, I_{5}}. (See Figure 3). Since C_{1} ⪯ C_{2} and C_{3} ⪯ C_{2} and C_{1} ⪯̸ C_{3} and C_{3} ⪯̸ C_{1}, C_{1} and C_{3} are the ⪯-minimal strict stable classes of P. Hence, their union, S(P) is {{r}, {r, p}, {q, p}}. From this, we may infer q ∨ r to be true in P and p to be unknown in P. □

We now quickly formalize the graph theoretic intuitions behind the notion of stable class.

Definition 2.4 Suppose P is a logic program. Then graph(P) is a directed graph which is defined as follows:

{p,r} {r} {p,q} {q}  ∅ {p,q,r} {p} {r,q}

Figure 3: Graphical Representation of Stable Classes, Example 2.5

1. The vertices of graph(P) are the interpretations of our language.

2. There is an arc from interpretation I to interpretation J iff M(P^{I}) = J.

If P has a finite Herbrand Base, then graph(P) is a finite graph. The following proposition is easy to prove.

Proposition 2.1 Suppose P is any logic program with a finite Herbrand Base, and I is a non-empty, strict stable class of P. Then we can express I as the set

{I_{0}, …, I_{n}} = I

where I_{1} = M(P^{I_{0}}), …, I_{n} = M(P^{I_{n−1}}) and I_{0} = M(P^{I_{n}}).

Proof. Proceed as follows. Suppose I has (n + 1) elements where n ≥ 0. First, pick any element of I and designate it as I_{0}. This is possible as I is non-empty. Now set I_{1} = M(P^{I_{0}}), I_{2} = M(P^{I_{1}}) and so on. Observe that for all 1 ≤ j < n, M(P^{I_{j}}) ∉ {I_{0}, …, I_{j}}. (If it was, then M(P^{I_{j}}) = I_{k} for some 0 ≤ k ≤ j and then {I_{k}, …, I_{j}, M(P^{I_{j}})} ⊂ {I_{0}, …, I_{n}} would be a stable class thus contradicting our assumption that I is strict). As I is a stable class, M(P^{I_{n}}) ∈ {I_{0}, …, I_{n}}. As I_{0} ∉ {M(P^{I_{0}}), …, M(P^{I_{n−1}})}, and because I is a stable class I_{0} ∈ {M(P^{I_{0}}), …, M(P^{I_{n}})}, it follows that I_{0} = M(P^{I_{n}}). □

Theorem 3 Let P be a program with a finite Herbrand Base. Then: I = {I_{1}, …, I_{n}} is a non-empty strict stable class of P iff I is a cycle in graph(P).

Proof. Without loss of generality, we may assume that I_{s} = M(P^{I_{s−1}}) for 2 ≤ s ≤ n and that I_{1} = M(P^{I_{n}}).

(→) Immediate from definitions.

(←) Again, it is immediate from the definition that I is a stable class if I is a cycle in graph(P). We only need to show that I is strict. Suppose I is not strict. Then there is a non-empty stable class I′ ⊂ I (here I′ is a strict subset of I). As I′ is a stable class, by (→) above, it follows that there is a cycle of the form

I_{r}, …, I_{k}

such that 1 ≤ r ≤ k ≤ n and

I_{r+1} = M(P^{I_{r}})
I_{r+2} = M(P^{I_{r+1}})
⋯
I_{k} = M(P^{I_{k−1}})
I_{r} = M(P^{I_{k}}).

Thus, M(P^{I_{k}}) = I_{r} and M(P^{I_{k}}) = M(P^{I_{r}}) which is impossible. □

Theorem 4 Suppose I and J are non-empty, strict stable classes of a logic program P that has a finite Herbrand Base. Then

I ∩ J ≠ ∅ iff I = J .

Proof. (←) Immediate consequence of the fact that I and J are non-empty stable classes.

(→) Suppose I ∩ J ≠ ∅. Let I ∈ I ∩ J. Then by Proposition 2.1, it follows that I = {I_{0}, …, I_{n}} = J where {I_{0}, …, I_{n}} is defined as in Proposition 2.1. □

The following result follows immediately from the preceding results.

Corollary 2.1 Suppose P is a logic program with a finite Herbrand Base and I a nonempty stable class of P. Then I may be written as the disjoint union

I = I_{1} ˙∪ ⋯ ˙∪ I_{n}

where I_{i} is a non-empty, strict stable class for all 1 ≤ i ≤ n. □

Using these results, we can now establish that the intersection of any two stable classes is a stable class.

Theorem 5 Suppose P is any logic program with a finite Herbrand Base, and that I and J are stable classes. Then I ∩ J is a stable class.

Proof. If I or J is the empty stable class, then I ∩J = ∅ which is a stable class. Likewise, if I and J are disjoint, then I ∩ J = ∅ is a stable class.

Hence, suppose that I and J are non-empty stable classes and that they have a non-empty intersection. As P has a finite Herbrand Base, I ∩ J must be finite. Let

I ∩ J = {I_{1}, …, I_{k}}.

By Corollary 2.1, I and J may be written as disjoint unions of the form:

I = I_{1} ˙∪ ⋯ ˙∪ I_{n}
J = J_{1} ˙∪ ⋯ ˙∪ J_{m}.

where the I_{r}’s and J_{s}’s are non-empty, strict, stable classes. As I_{1}, …, I_{k} are all in I ∩ J, for each 1 ≤ i ≤ k, there are integers, 1 ≤ α(i) ≤ n and 1 ≤ β(i) ≤ m such that

I_{i} ∈ I_{α(i)}

and

I_{i} ∈ J_{β(i)}.

As the I_{i}’s and J_{i}’s are non-empty, strict stable classes, and as I_{i} ∈ I_{α(i)} ∩ J_{β(i)}, it follows by Theorem 4 that I_{α(i)} = J_{β(i)} for all 1 ≤ i ≤ k. Hence, I ∩ J is equal to

I_{α(1)} ∪ ⋯ ∪ I_{α(k)}.

As each I_{α(i)} is a stable class, it follows by Lemma 2 that I ∩ J is a stable class. □

Theorem 5 and Lemma 2 together imply that if P is any logic program with a finite Herbrand Base, then the set of stable classes of P forms a lattice with union as the LUB operator, and intersection as the GLB operator. However, Theorem an infinite Herbrand Base. For such programs, we have been unable to determine whether intersection of stable classes is a stable class. However, we show below that for such programs, the family of stable classes forms a complete lattice anyway under suitably defined LUB and GLB operations.

Theorem 6 Suppose P is any logic program. Then the family of stable classes of P forms a complete lattice.

Proof. We need to show that arbitrary sets of stable classes have least upper bounds and greatest lower bounds.

Suppose (S_{i})_{i∈B} is a family of stable classes. Then ⋃_{i∈B} S_{i} is a stable class by Lemma 2. Take union to be the LUB operator.

Let INT (P) = {X |X is a stable class of P and X ⊆ ⋂_{i∈B} S_{i}}. Then, INT (P) is non-empty as ∅ ∈ INT (P). Now take

GLB({S_{i} | i ∈ B}) = ⋃_{X∈INT (P)} X.

Each X ⊆ ⋂_{i∈B} S_{i}, and hence ⋃_{X∈INT (P)} X ⊆ ⋂_{i∈B} S_{i}. ⋃_{X∈INT (P)} X is a stable class by Lemma 2. Furthermore, ⋃_{X∈INT (P)} X is bigger thanb every other lower bound for (S_{i})_{i∈B}.

This establishes that the set of stable classes of P always form a complete lattice. □

3 Extension Classes in Default Logic

Default logic introduced by Reiter [Rei80] forms one of the most important formalisms for non-monotonic reasoning. Recently, the relationship between default logics and other forms of non-monotonic reasoning have been studied intensely (in particular the work of Konolige [Kon88] and the work of Marek and Truszczynski [MT89a, Mar89] show that default and auto-epistemic logics are not that different after all). More recently, the relationship between logic program semantics and non-monotonic logics has been studied by Przymusinski [Prz89b], Marek and Truszczynski [MT89b] and by Marek and Subrahmanian [MS88]. In all these cases, correspondences are established between certain structures called extensions in default logic, and certain classes of models of logic programs. However, default theories may not always have extensions. In such cases, these correspondences are not very meaningful. In this section, we introduce a new concept in default logic called an extension class. All default theories possess extension classes. After that, we show various correspondences between extension classes and stable classes of logic programs.

We assume that we have a fixed language L, whose ground atoms are denoted by AT. A (propositional) default is a triple d = (p(d), j(d), c(d)), where p(d) and c(d) are formulas of L = L(AT)^{5}, and j(d) is a finite subset of L. p(d) is called the prerequisite of d, j(d) the justification of d, and c(d) the consequent, or conclusion of d. Default d is usually denoted by \frac{p(d):j(d)}{c(d)}. A default theory is a pair (D, W), where W ⊆ L and D is a collection of defaults.

Given a default theory (D, W) and a set E of formulas (called the context), we can define an operator R^{E,D} which maps sets of formulas to sets of formulas in the following way:

R^{E,D}(S) = Cn(S ∪ {c(d) : d ∈ D, p(d) ∈ S, ¬j(d) ∩ E = ∅}).

Here, Cn denotes the familiar Tarskian consequence operator and ¬j(d) denotes the set {¬β | β ∈ j(d)}. However, we abuse notation in the following way: if I is an interpretation, we also use Cn(I) to denote the set of all formulas satisfied by the interpretation I. The operator R^{E,D}(S) was initially defined by Reiter and is related to the notion of strong default proof discussed in [MT89a]. Starting with Cn(W), the least fixpoint of this operator above Cn(W) is the set of formulas that have a strong proof [MT89a] from W using D and with respect to the context E. More formally,

Definition 3.1 Suppose (D, W) is a default theory, and E is a set of formulas, called the context. Then:

R_{0}^{E,D}(W) = Cn(W).

R_{n+1}^{E,D}(W) = R^{E,D}(R_{n}^{E,D}(W))

R_{∞}^{E,D}(W) = ⋃_{n=0}^{∞} R_{n}^{E,D}(W) □

Example 3.1 Suppose (D, W) is the default theory

W = \{p → q\} , D = \{\frac{q : ¬w}{p} , \frac{: ¬s}{q}\}

and E is the context E = Cn({r}). Then:

R_{0}^{E,D}(W) = Cn(W) R_{1}^{E,D}(W) = Cn(W ∪ {q}) R_{2}^{E,D}(W) = Cn(W ∪ {q, p}) = R_{∞}^{E,D}(W) □

The most important structures of default logic are extensions, which are formally defined as follows.

5L(AT) is the propositional language generated by considering the ground atoms in AT to be propositional symbols.

Definition 3.2 E is an extension of a default theory (D, W) iff E = R_{∞}^{E,D}(W). □

If a particular default theory (D, W) has a unique extension then the meaning of that theory is considered to be the set of formulas present in the extension. Note that extensions are always closed under propositional consequence.

However, many default theories may have multiple extensions or no extensions at all. Our goal is to explore the meaning of the default theory (D, W) in such a case.

When a default theory (D, W) has multiple extensions, one way to assign meaning to formulas, with respect to the theory (D, W) is by assigning a formula ϕ the truth value true (resp. false) iff it is true (resp. false) in all extensions of the theory (D, W). If it can not be assigned one of these two values then it is assigned the truth value “unknown”. Although this a reasonable solution for theories having multiple extensions, it can not characterize the meaning of theories that do not have any extensions.

Example 3.2 Consider the default theory (D, W), where W = \{p\} and D = \{\frac{:¬q}{q} \}. The two possible extensions are: E_{1} = Cn({p}) and E_{2} = Cn({p, q}). But R_{∞}^{E_{1},D} = Cn({p, q}) ≠ E_{1} and also R_{∞}^{E_{2},D} = Cn({p}) ≠ E_{2}. Hence, neither E_{1} nor E_{2} are extensions of this default theory and hence this default theory has no extensions. Intuitively we feel that p should be true in this default theory (and of course, ¬p should not be true in this theory). Hence, we feel that extensions are not enough to capture the meaning of a default theory. □

Example 3.3 Przymusinski introduces three-valued interpretations of default theories and successfully handles the above default theory. However, consider the default theory (D, W) below:

W = \{p ← q, p ← r\} D = \{\frac{:¬q}{r} , \frac{:¬r}{q} \}

According to Przymusinski’s semantics p is not true in all 3-valued extensions of this default theory. But this default theory has two extensions, E_{1} = {p, q, p ← q, p ← r} and E_{1} = {p, r, p ← q, p ← r}. Since p is true in these two extension our intuition tells us that p should be true in this default theory. This intuition is not supported by Przymusinski’s three-valued formalism. □

We now define a structure called Extension Class using which we are able to handle the semantics of default logics when they have multiple or no extensions.

Definition 3.3 A family, E = (E_{i})_{i∈A} of sets of formulas is an extension class of (D, W) iff E = {R_{∞}^{E_{i},D}(W) | E_{i} ∈ E.}

As defined above an extension class is a set of sets of formulas. A formula F is assigned true (resp. false) by an extension class E = (E_{i})_{i∈A} of a default theory (D, W) iff F is true (res. false) in each E_{i}, i ∈ A.

Example 3.4 We again consider the default theory (D, W), where W = {p} and D = \{\frac{:¬q}{q} \}. This default theory has an extension class

{Cn({p}), Cn({p, q})}.

Since, p is true in all sets of formulas of this extension class we can assume p to be true in the extension class semantics of this default theory. q is assumed to be “unknown” as it can neither be assumed true nor false, based on this extension class. □

Extension classes are very similar to stable classes.

Theorem 7 Suppose AT is a finite set of ground atoms. Every propositional default theory has a non-empty extension class.

Proof. The proof proceeds in the same way as the proof of Theorem 1. □

Theorem 8 Suppose (D, W) is any default theory. Then: E is an extension of (D, W) iff the singleton set {E} is an extension class of (D, W). □

4 Relationship between Stable Classes and Extension Classes

Marek and Truszczynski [MT89b] present three different translation of logic programs to default logic and show the relationship between the stable models of the original program and the extensions of the default theories generated by the different translations of the original program. Keeping with their terminology two of the transformations are :

tr_{1} : Let C = a ← b_{1} & ⋯ b_{k} & ¬c_{1} & ⋯ & ¬c_{r}. tr_{1}(C) = \frac{b_{1}∧···∧b_{k}:¬c_{1},···,¬c_{r}}{a}. If P is a program tr_{1}(P) = (D_{1}(P), W_{1}(P)) is a default theory corresponding to P, where W_{1}(P) = ∅ and D_{1}(P) = {tr_{1}(C) : C ∈ P }.^{6}

tr_{2} : Let C = a ← b_{1} ⋯ b_{k}, ¬c_{1} ⋯ ¬c_{r}. tr_{2}(C) = \frac{:¬c_{1}···¬c_{r}}{b_{1}∧···∧b_{k}⇒a}. If P is a program tr_{2}(P) = (D_{2}(P), W_{2}(P)) is a default theory corresponding to P, where W_{2}(P) = ∅ and D_{2}(P) = {tr_{2}(C) : C ∈ P }.

We will now study the relationship between stable classes of a logic program P and the extension classes of the above two translations of P to a default theory.

Marek and Truszczynski [MT89b] have the following theorem relating between stable model of a logic program P and the extensions of the translated default theory (D_{1}(P), W_{1}(P)).

Theorem 9 (Marek and Truszczynski [MT89b]) Let P be a logic program and let M be a set of ground atoms.

1. M is a stable model of P iff Cn(M) is an extension of tr_{1}(P).

2. R_{n+1}^{E,D_{1}(P)}(W_{1}(P)) = Cn(T_{P^{M}} ↑ n), for all n, where (D_{1}(P), W_{1}(P)) = tr_{1}(P) and E = Cn(M).

3. R_{∞}^{Cn(M),D_{1}(P)}(W_{1}(P)) = Cn(T_{P^{M}} ↑ ω) where (D_{1}(P), W_{1}(P)) = tr_{1}(P). □

Theorem 10 M is a stable class of a program P iff E = {Cn(M_{i}) | M_{i} ∈ M} is an extension class of tr_{1}(P).

Proof: ⇒ Let M be a stable class for program P. By definition of a stable class, M = {T_{P^{M_{i}}} ↑ ω | M_{i} ∈ M}. Then E = {Cn(M_{i}) | M_{i} ∈ M }. = {Cn(T_{P^{M_{i}}} ↑ ω) | M_{i} ∈ M } (as M is a stable class) = {R_{∞}^{Cn(M_{i}),D_{1}(P)}(W_{1}(P)) | M_{i} ∈ M} (by part 3 of Theorem 9) = {R_{∞}^{E_{i},D_{1}(P)}(W_{1}(P)) | E_{i} ∈ E} (by our initial assumption about E). Hence E is an extension class of tr_{1}(P). ⇐ Let E = {Cn(M_{i}) | M_{i} ∈ M} (1) be an extension class of tr_{1}(P). Hence, E = {R_{∞}^{E_{i},D_{1}(P)}(W_{1}(P)) | E_{i} ∈ E} = {R_{∞}^{Cn(M_{i}),D_{1}(P)}(W_{1}(P)) | Cn(M_{i}) ∈ E} ={R_{∞}^{Cn(M_{i}),D_{1}(P)}(W_{1}(P)) | M_{i} ∈ M} (from (1)) = {Cn(T_{P^{M_{i}}} ↑ ω) | M_{i} ∈ M } (by part 3 of Theorem 9) (2) ¿From (1) and (2) {M_{i} | M_{i} ∈ M} = {T_{P^{M_{i}}} ↑ ω | M_{i} ∈ M } ⇒ M = {T_{P^{M_{i}}} ↑ ω | M_{i} ∈ M } Hence, M is a stable class. □

6tr_{1} was first introduced in [BF88].

Now we will study the relationship between stable classes of P and extension classes of tr_{2}(P). The following two lemmas of Marek and Truszczynski [MT89b] are useful to us. These lemmas use a function, called int(P), defined as follows. int(P) = {b_{1} ∧ ⋯ ∧ b_{k} ⇒ a : a ← b_{1} ∧ ⋯ ∧ b_{k} ∈ P }.

Lemma 6 [MT89b] Suppose M is a set of ground atoms. Then Cn(int(P^{M})) ∩ AT = T_{P^{M}} ↑ ω. □

Lemma 7 [MT89b] Let E ⊆ L and P be a logic program. Then R_{∞}^{E,D_{2}(P)}(W_{2}(P)) = Cn(int(P^{E∩AT})). □

Theorem 11 Suppose M is a collection of interpretations. M is a stable class of program P iff there exists an extension class E of tr_{2}(P), such that M = {E_{i} ∩ AT | E_{i} ∈ E} is an extension class of tr_{2}(P).

Proof : ⇒ Let M be a stable class. Hence, M = {T_{P^{M_{i}}} ↑ ω | M_{i} ∈ M }. Let E = {Cn(int(P^{M_{i}})) | M_{i} ∈ M }.

(a) We first show that the above definition of E satisfies the condition M = {E_{i} ∩ AT | E_{i} ∈ E}. M = {T_{P^{M_{i}}} ↑ ω | M_{i} ∈ M }(as M is assumed to be a stable class) = {Cn(int(P^{M_{i}})) ∩ AT | M_{i} ∈ M }(by Lemma 6) = {E_{i} ∩ AT | E_{i} ∈ E}(by our assumption that E = {Cn(int(P^{M_{i}})) | M_{i} ∈ M })

(b)We now show that E is an extension class. E = {Cn(int(P^{M_{i}})) | M_{i} ∈ M } = {Cn(int(P^{T_{P^{M_{i}}} ↑ω})) | M_{i} ∈ M } (as M is a stable class) = {Cn(int(P^{Cn(int(P^{M_{i}})∩AT)})) | M_{i} ∈ M } (by Lemma 6) = {Cn(int(P^{E_{i}∩AT})) | E_{i} ∈ E }(by our initial assumption about E) = {R_{∞}^{E_{i},D_{2}(P)}(W_{2}(P)) : E_{i} ∈ E} (by Lemma 7) Hence, E is an extension class of tr_{2}(P).

⇐ Let E be an extension class of tr_{2}(P). Hence, E = {R_{∞}^{E_{i},D_{2}(P)}(W_{2}(P)) | E_{i} ∈ E} = {Cn(int(P^{E_{i}∩AT})) | E_{i} ∈ E}(by Lemma 7) = {Cn(int(P^{M_{i}})) | M_{i} ∈ M} (1) (since M is defined to be {E_{i} ∩ AT | E_{i} ∈ E} in the statement of the theorem.) Considering M, M = {E_{i} ∩ AT | E_{i} ∈ E} = {Cn(int(P^{M_{i}})) ∩ AT | M_{i} ∈ M}(using the value of E in (1)) = {T_{P^{M_{i}}} ↑ ω | M_{i} ∈ M } (by Lemma 6) Hence M is a stable class for program P. □

5 Weak Extension Classes and Stable Classes

It is well known ([MT89a, MT]) that under Konolige’s translation of a default theory (D, W) into an auto-epistemic theory tr_{K}(D, W), extensions of (D, W) do not correspond to expansions of tr_{K}(D, W). In order to find a suitable correspondence, Marek and Truszczynski [MT89a] introduced the concept of weak extensions of default theories. They demonstrated that weak extensions of (D, W) correspond precisely to expansions of tr_{K}(D, W).

We now introduce the notion of a weak extension class of a default theory. We then demonstrate that there is a precise correspondence between stable classes and weak extension classes under the translation tr_{2}.

Given a set D of defaults, we write c(D) to denote the set {c(d) | d ∈ D}, i.e. c(D) is the set of all conclusions of defaults occurring in D.

Definition 5.1 E is said to be a weak extension of a default theory (D, W) iff E = Cn(W ∪ \{c(d) | \frac{p(d) : j(d)}{c(d)} is a default in D and p(d) ∈ E and ¬j(d) ∩ E = ∅\}).

Definition 5.2 A collection (E_{i})_{i∈A} of sets of formulas is said to be a weak extension class of the default theory (D, W) iff \{E_{i} | i ∈ A\} = \{Cn(W ∪ \{c(d) | \frac{p(d) : j(d)}{c(d)} is a default in D and p(d) ∈ E_{j} and ¬j(d) ∩ E_{j} = ∅}) | j ∈ A}.

Example 5.1 For instance, consider the default theory (D, W) below:

W = ∅ D = \{ \frac{:}{q} , \frac{: ¬p}{p}\}

In this case, (D, W) has no weak extension. However, it seems intuitively clear that q should be a consequence of this default theory. In this case, (D, W) has exactly one weak extension class, viz.

{Cn({q}), Cn({p, q})}.

q is true in both these sets, and hence, according to the weak extension class semantics, q is true w.r.t. (D, W). On the other hand, p’s truth value is unknown. □

Recall that given a logic program clause

C ≡ a ← b_{1} & … & b_{n} & ¬c_{1} & ⋯ & ¬c_{m},

tr_{2}(C) is the default:

\frac{: ¬c_{1}, …, ¬c_{m}}{b_{1} & ⋯ & b_{n} ⇒ a}.

Given a logic program P, tr_{2}(P) = {tr_{2}(C) | C ∈ P }.

Remark 1 Note that if I is any interpretation, and A any ground atom, then:

1. A ∈ Cn(I) iff A ∈ I and

2. ¬A ∈ Cn(I) iff A ∉ I.

Recall from Section 3 that we abuse notation by using Cn(I) when I is an interpretation to denote the set of all wffs satisfied by interpretation I.

Theorem 12 Let P be a logic program, and let (I_{j})_{j∈A} be a set of Herbrand interpretations. Then: (I_{j})_{j∈A} is a stable class of P iff {Cn(I_{j}) | j ∈ A} is a weak extension class of tr_{2}(P). □

Proof. Let tr_{2}(P) = (D_{2}(P), W_{2}(P)). All defaults in tr_{2}(P) have empty pre-conditions. By a result of Marek and Truszczynski [MT89a], we know that Cn(W_{2}(P) ∪ \{c(d) | \frac{: j(d)}{c(d)} is a default in D_{2}(P) and ¬j(d) ∩ E = ∅}) = R_{∞}^{E,D_{2}(P)}(W_{2}(P)) for all contexts E. The result now follows immediately from Theorem ??. □

We are grateful to an anonymous referee for suggesting the above simplified proof.

The above theorem establishes a one-one correspondence between the stable classes of a logic program P and the weak extension classes of the default theory tr_{2}(P). Whenever P consists of a finite set of ground clauses, P is guaranteed to have a non-empty stable class and hence this result is meaningful.

6 Conclusions

The operator associated with a logic program is often non-monotonic when program clauses are allowed to contain negated atoms in their body. In view of this non-monotonic feature of logic program semantics, various researchers have developed logic program semantics based on non-monotonic logics.

The best known semantics under this category is the stable model semantics due to Gelfond and Lifschitz [GL88]. This semantics elegantly characterizes the meaning of a large class of logic programs. However, not all programs have stable models. Hence, the stable model semantics is not universally applicable.

In this paper, we have proposed a new semantics for logic programming based on stable classes. The stable class semantics is applicable to all programs for which the stable class semantics is applicable (cf. Lemma 1), as well as to logic programs that might not have a stable model cf. Theorem 1. For stratified logic programs the stable class semantics agrees with the stable model semantics.

We have shown via various examples (cf. Examples 2.3, 2.4, 2.5) that the stable class semantics is often more appropriate than the well-founded semantics of Van Gelder, Ross and Schlipf [VRS88].

In addition, the ideas underlying stable class theory induce a definition of extension class for default theories. The extension class semantics for default logics extends the extension-based semantics for default logics by now providing a precise characterization of the semantics of default theories that do not have an extension. Similar ideas apply also to the concept of weak extension.

We have demonstrated that there is a one-one correspondence between the stable class semantics of logic programs, and the extension class semantics for default logic, as well as the weak extension class semantics for default logic. We hope that such correspondences enable us to get a clearer picture of the relationship between logic programming and nonmonotonic reasoning.

In ongoing work, we are extending the concept of classes to auto-epistemic logic also.

Acknowledgements

We wish to express our appreciation to the National Science Foundation for their support of our work under grant number IRI-86-09170 and the Army Research Office under grant number DAAG-29-85-K-0-177.

References

[ABW88] K.R. Apt, H.A. Blair, and A. Walker. Towards a Theory of Declarative Knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–148. Morgan Kaufmann Pub., Washington, D.C., 1988.

[BF88] N. Bidoit and C. Froidevaux. General Logical Databases and Programs: Default logic semantics and Stratification. Journal of Information and Computation, 1988. (in print).

[BLM89a] C. Baral, J. Lobo, and J. Minker. Generalized disjunctive well-founded semantics for logic programs. Technical report, Dept of Computer Science, University of Maryland, College Park Md 20742, 1989.

[BLM89b] C. Baral, J. Lobo, and J. Minker. Generalized well-founded semantics for logic programs. Technical report, Dept of Computer Science, University of Maryland, College Park Md 20742, 1989.

[Elk89] C. Elkan. A Rational Reconstruction of Nonmonotonic TMSs. Artificial Intelligence, 1989. (in print).

[Fit86] M. Fitting. A Kripke-Kleene Semantics for Logic Programs. Journal of Logic Programming, 3:93–114, 1986.

[Gef89] H. Geffner. Default Reasoning, Minimality and Coherence. In Proc. of First International Conference on Knowledge Representation and Reasoning , pages 137–147, 1989.

[Gel87] M. Gelfond. On Stratified Autoepistemic Theories. In Proc. AAAI-87, pages 207–211, 1987.

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

[Kon88] Kurt Konolige. On the relation between default and autoepistemic logic. Artificial Intelligence, 35:343–382, 1988.

[Llo84] J.W. Lloyd. Foundations of Logic Programming. Springer–Verlag, 1984.

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

[Mar89] W. Marek. Stable theories in autoepistemic logic. Fundamenta Informaticae, 12:243–254, 1989.

[MS88] W. Marek and V.S. Subrahmanian. The Relationship Between Stable, Supported, Default and Auto-Epistemic Semantics for General Logic Programs. Technical Report 128-88, Computer Science Department, University of Kentucky, Lexington, Kentucky, 1988. Submitted to Theoretical Computer Science. A preliminary version appears in: Proc. 6th International Conference on Logic Programming, MIT Press. .

[MT] W. Marek and M. Truszczynski. Autoepistemic logic. to appear in JACM.

[MT89a] W. Marek and M. Truszczynski. Relating autoepistemic and default logics. Technical report, Department of Computer Science, University of Kentucky at Lexington, 1989.

[MT89b] W. Marek and M. Truszczynski. Stable semantics for logic programs and default theories. In Proceedings of NACLP 89, pages 243–256, 1989.

[Prz89a] T. Przymusinski. Non-Monotonic Formalisms and Logic Programming . In Proc. 6th International Conference on Logic Programming, Lisbon, pages 655– 674, 1989.

[Prz89b] T. Przymusinski. Three-valued Formalizations of Non-monotonic Reasoning and Logic programming. In Proceedings of First International Conference on Knowledge Representation and Reasoning, 1989.

[Prz90] T. Przymusinski. Three valued stable models and well-founded models of logic programs. Technical report, Dept of Computer Science, University of Texas at El Paso, 1990.

[Rei80] R. Reiter. A Logic for Default Reasoning. Artificial Intelligence, 13(1 and 2):81– 132, April 1980.

[VRS88] A. Van Gelder, K. Ross, and J.S. 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.

[YL89] J. You and L. Li. Supported Circumscription and Its Relation to Logic Programming with Negation. In Proc. of the North American Conference on Logic Programming, Cleveland, pages 291–312, 1989.