On the Partial Semantics for

Disjunctive Deductive Databases

Thomas Eiter, Nicola Leone, Domenica Saccà

Christian Doppler Labor für Expertensyteme Technische Universität Wien Paniglgasse 16, 1040 Wien

August 19, 1995

CD-TR 95/82

ON THE PARTIAL SEMANTICS FOR DISJUNCTIVE DEDUCTIVE DATABASES

T. Eiter  N. Leone  D. Saccà
Christian Doppler Lab.  ISI-CNR  DEIS
Technische Universitat Wien  c/o DEIS-UNICAL,  Università della Calabria,
1040 Vienna, Austria  87030 Rende, Italy  87030 Rende, Italy

eiter@dbai.tuwien.ac.at    nik@si.deis.unical.it   sacca@si.deis.unical.it

preliminary report

Abstract

Partial stable models for deductive databases, i.e., normal function-free logic programs (also called datalog programs), have two equivalent definitions: one based on 3-valued logics and another based on the notion of unfounded set. The notion of partial stable model has been extended to disjunctive deductive databases using 3valued logics. In this paper, a characterization of partial stable models for disjunctive datalog programs is given using a suitable extension of the notion of unfounded set.

Two interesting subclasses of partial stable models, M-stable (Maximal-stable) (also called regular models, preferred extension, and maximal stable classes) and Lstable (Least undefined-stable) models, are then extended from normal to disjunctive datalog programs. L-stable models are shown to be the natural relaxation of the notion total stable model; on the other hand the less strict M-stable models, endowed with a nice modularity property, may be appealing from the programming and computational point of view. M-stable and L-stable models are also compared with the regular models for disjunctive datalog programs recently proposed in the literature.

1 Introduction

Deductive databases comprise explicit data and logical rules for computing queries on the data, which amount to a logic program without function symbols, i.e., datalog programs (extended with negation) [34, 5]. The need for representing disjunctive information led to disjunctive deductive databases [23], which fertilized also work on disjunctive logic programming [22, 24]. In this paper, we address disjunctive deductive databases, which are identified with disjunctive function-free logic programs [18], and refer to them simply as programs.

To date, the total stable (or 2-valued stable) model semantics [16, 26] is a dominant semantics for both normal and disjunctive programs. It is widely acknowledged that the total stable semantics is the natural meaning to be assigned to a (disjunctive) program, provided that it admits some stable models. However, a drawback of this semantics is that several meaningful programs do not admit any total stable model, which results in a loss of information. To handle these cases, Przymusinski defined the notion of partial stable (or 3-valued stable) model for both normal and disjunctive programs [26]. Partial stable models exist for a wider class of programs (actually, for normal programs they always exist). Moreover, on the class of (disjunctive) stratified programs, partial stable models coincide with total stable models. For normal programs, partial stable models have been also defined using the notion of unfounded set [29, 30].

A first contribution of this paper is an equivalent definition of partial stable semantics for such programs which singles out partial stable models without the need to resort to 3-valued logics. To this end, we present a new notion of unfounded set for disjunctive programs, which generalizes the analog notion given for normal (i.e., nondisjunctive) programs in [36] (moreover, on total interpretations, it coincides with the definition given in [20] for disjunctive programs). Intuitively, as for normal programs, the notion of unfounded set can be seen as a form of CWA rule: if a set X of undefined atoms is an unfounded set w.r.t. an interpretation I, then the truth value of the atoms in X can be switched to false without violating any rule of the program.

Once defined unfounded sets, we provide an appealing characterization of 3-valued stable models in terms of unfounded sets. In particular, we show that an interpretation is a 3-valued stable model if and only if its true atoms are ”justifiable“ (see below) and the set of its false atoms is a maximal unfounded set. The proof of this equivalence is to be considered a relevant part of the contribution of this paper. To our knowledge, this is the first characterization of 3-valued stable models in terms of unfounded sets. It extends similar studies conducted in [36, 29, 30, 20], which investigated the relationships between unfounded sets and stable models in more restricted domains.

Despite their relevance, several objections to partial stable models came from the observation that every 3-valued model theoretic approach should satisfy two basic principles: justifiability (also called foundedness) and minimal undefinedness [37, 38]. Intuitively, the principle of justifiability, which is intimately related to the concept of labeling-based justification in Doyle’s truth maintenance system [8], states that every positive literal which is true must be derived from the rules of the program possibly using negative literals as additional axioms. The principle of minimal undefinedness prescribes that the undefined truth value should be used only when necessary (i.e., a “good” semantics should tend to minimize the set of undefined atoms).

Partial stable models meet the principle of justifiability but do not satisfy the principle of minimal undefinedness. This observation led several researchers to investigate on refinements of 3-valued stable model semantics which reduce the degree of undefinedness. For normal programs, these efforts led to the definition of several notion of partial models: M-stable models [29, 32, 31]^{1}, regular models [37, 38], preferred extensions [9], maximal stable classes [3, 39], and L-stable models [32, 31]. Interestingly, even if all these semantics have been independently defined, M-stable models, preferred extensions, regular models, and maximal stable classes exactly coincide, as proven in [17] and [39]. In the more general case of disjunctive programs, to our knowledge no subclass of 3-valued stable models minimizing undefinedness has been proposed. (Regular models have been extended to the disjunctive case in [38]; but, differently from the case of normal programs, a regular model is not guaranteed to be a partial stable model.)

Another contribution of this paper is the proposal of two refinements of the partial stable semantics for disjunctive programs, namely, the M-stable (Maximal stable) and the L-stable (Least undefined stable) semantics, generalizing the analogous semantics presented in [32, 31] for normal programs. Both semantics extend the partial stable semantics in the spirit of the principle of minimal undefinedness of [37, 38].

Since several researchers recognized M-stable models as an important semantics for normal programs [3, 9, 29, 32, 31, 37, 38], we start by extending M-stable models to the domain of disjunctive programs.

The M-stable models are the partial stable models which are maximal under set inclusion (where a partial model is represented by the set of ground literals true in the model). They present the following main characteristics:

1. On normal programs, M-stable models coincide with the preferred extensions of [9], the regular models of [37], the maximal stable classes of [3], and the M-stable models of [32, 31].

2. On the class of stratified (disjunctive) programs, M-stable models exactly coincide with total stable models.

3. M-stable semantics has a lower degree of undefinedness compared to 3-valued stable semantics.

Even if M-stable models reduce the degree of undefinedness of partial stable models, they do not fully agree with total stable models (i.e., even for program admitting total stable models, an M-stable model may be not total stable). A further refinement of the notion of M-stable model yields the L-stable models, which fully agree with total stable models when a program admit such models.

1Note that M-stable models are called P-stable models in [29].

The L-stable models are the M-stable models with the minimal degree of undefinedness. They have the following peculiarities:

1. On normal programs, L-stable models coincide with the L-stable models of [32, 31].

2. On the class of stratified (disjunctive) programs, L-stable models exactly coincide with total stable models.

3. L-stable semantics has a lower degree of undefinedness compared to M-stable semantics (and also to 3-valued stable semantics).

4. On the class of programs admitting some total stable model, the L-stable models exactly coincide with the total stable models.

Thus, L-stable semantics has an even lower degree of undefinedness than M-stable semantics. Moreover, the fact that L-stable semantics may differ from total stable semantics only on (unstratified) programs having no total stable model, is highly desirable to approximate the total stable semantics and candidates L-stable models as the natural relaxation of total stable models.

We compare both M-stable and L-stable models with another attempt to ”approximate“ total stable models for disjunctive programs due to You and Yuan [38]. In that paper, the authors extend the regular model semantics from normal to disjunctive programs. Regular models exist for every disjunctive program and are “more defined” (i.e., with a lower degree of undefinedness) than 3-valued stable models. However, a regular model is in general not a partial stable model and, even if the program admits total stable models, regular model semantics does not coincide with total stable semantics. Because of the latter drawback, regular models can not be considered a “good approximation” of total stable semantics (in case that a program has total stable models, it is widely recognized that they are the intuitive meaning of the program and every semantics should coincide on these programs).

A careful analysis of regular models reveals that a reason for their disagreement to stable models is that, differently from all the dominant semantics for datalog (and also from M-stable and L-stable semantics), they do not fully satisfy the closed world assumption. We individuate the lack of this property as a drawback of the regular model semantics and discuss the main consequences of that.

A final issue of this paper is the investigation of modularities properties of which partial semantics for disjunctive programs are endowed with. In particular, extending similar studies conducted in [34, 33, 28] for normal programs and, for disjunctive programs, in [7] and [11], we prove that both M-stable and regular models for disjunctive programs are endowed with an appealing modularity property. This modularity property allows us to enlarge the class of programs on which M-stable and regular models are known to coincide. Furthermore, the modularity property permits to derive that, for normal programs, both M-stable and regular models can be computed bottom-up following the dependencies between the predicates of the program (in a process similar to the computation of stratified programs [34]). The latter computational property is particularly relevant in the context of deductive databases, where it is very important to reduce the amount of data to be dealt with at a time.

The main contributions of this paper can be summarized as follows.

• We present a new notion of unfounded set, which extends the classical definition of Van Gelder et al. [36] from normal to disjunctive programs.

• We provide a declarative characterization of 3-valued stable models in terms of unfounded sets. In particular, we show that an interpretation is a 3-valued stable model if and only if it is founded (i.e., all its true atoms are justifiable) and its false atoms form a maximal unfounded set.

• We extend the notions of M-stable and L-stable models from normal to disjunctive programs.

• We carry out a comparison between M-stable, L-stable and regular semantics for disjunctive programs and propose L-stable models as the natural relaxation of the notion of total stable model.

• We investigate modularity properties which hold for partial semantics. This analysis allows us to enlarge the class of programs on which M-stable and regular models are known to coincide and permits to derive useful computational properties for both M-stable and regular models.

The sequel of the paper is organized as follows. After some preliminary on disjunctive deductive databases, Section 2 presents the notion of unfounded set and provides our definition of P-stable (Partial stable) model in terms of unfounded sets. Section 3 demonstrates the equivalence between P-stable models and the 3-valued stable models of [26]. M-stable and L-stable models are defined in Section 4. In Section 5, M-stable and L-stable models are compared with the regular models for disjunctive programs [38]. In Section 6, we demonstrate some modularity properties for M-stable and regular models and apply these results to derive both semantic and computational properties of M-stable and regular semantics. Finally, Section 7 addresses some further issues and concludes the paper.

2 Partial Stable Models

Disjunctive Deductive Databases

Deductive databases are described in a logical language using variables from a set V, predicates of nonnegative arity from a countable set Π, and constants from a finite set Λ.

An atom is of form a(t_{1}, …, t_{n}), where a is a predicate of arity n in Π each t_{1}, …, t_{n} is either a constant in Λ or a variable in V. A literal is either a positive literal p or a negative literal ¬p, where p is an atom. We use often an upper-case letter, say L, to denote either a positive or a negative literal. Two literals are complementary if they are of the form p and ¬p, for some atom p. Given a literal L, ¬.L denotes its complementary literal, and given a set A of literals, ¬.A denotes the set {¬.L | L ∈ A}. A rule r is a clause of the form

a_{1} ∨ ⋯ ∨ a_{n} ← b_{1}, ⋯, b_{k}, ¬b_{k+1}, ⋯, ¬b_{m}, n ≥ 1, m ≥ 0.

where a_{1}, ⋯, a_{n}, b_{1}, ⋯, b_{m} are atoms. The disjunction a_{1} ∨ ⋯ ∨ a_{n} is the head of r, while the conjunction b_{1}, …, b_{k}, ¬b_{k+1}, …, ¬b_{m} is the body of r. We denote by H(r) the set {a_{1}, …, a_{n}} of the head atoms, and by B(r) the set {b_{1}, …, b_{k}, ¬b_{k+1}, …, ¬b_{m}} of the body literals. Moreover, B^{+}(r) and B^{−}(r) denote the set of positive and negative literals occurring in B(r), respectively. A disjunctive deductive database (simply program hereafter) is a finite set of rules. Thus, a disjunctive deductive database is a disjunctive datalog program [11]. A distinction between extensional (database) predicates and intensional (derived) predicates can be made as usual [34, 18]; for simplicity, we do not extend on this in detail.

A program is normal if it contains only normal clauses, i.e., the head contains exactly one atom (n = 1). A ¬-free (resp. ∨-free) program is called positive (resp. normal). An atom, a literal, a rule or program is ground if no variable appears in it. As common, we assume that the sets Π and Λ are implicitly given by the predicates and constants occurring in the considered program.

Interpretations

We denote by B_{LP} the Herbrand Base of LP, i.e. the set of all ground atoms constructible from the predicates appearing in the rules of LP and the constants occurring in LP.

We denote by ground(LP) the set of all ground instances of the rules occurring in LP, where a ground instance of a rule r is obtained by any substitution σ that maps each variable X in r to a constant occurring in in LP. By Lit_{LP} we denote the set of all literals involving atoms from ground(LP), i.e. Lit_{LP} = B_{LP} ∪ ¬.B_{LP}.

An (Herbrand) interpretation I of a program LP is a consistent set of ground literals, i.e. I ⊆ Lit_{LP} such that I ∩ ¬.I = ∅. A ground literal L is true (resp. false) w.r.t. I if L ∈ I (resp. L ∈ ¬.I). If a ground literal is neither true nor false w.r.t. I then it is undefined w.r.t. I. A (possibly empty) conjunction of ground literals C is true in I if every literal in C is in I, false in I if there exists some literal A in C for which ¬A ∈ I and undefined in I otherwise. We denote by I^{+} and I^{−} the set of positive and negative literals occurring in I, respectively. \overline{I} denotes the set of undefined atoms w.r.t. I (that is, \overline{I} = B_{LP} − (I^{+} ∪ ¬.I^{−})). The interpretation I is total if \overline{I} is empty (that is, I^{+} ∪ ¬.I^{−} = B_{LP}); otherwise, I is partial. A total model of LP is a total interpretation M which satisfies each rule r in ground(LP), i.e., if B(r) ⊆ M, then H(r) ∩ M ≠ ∅.^{2}

Unfounded Sets

Definition 1 (Unfounded Set) Let I be an interpretation for LP. A set X ⊆ B_{LP} of ground atoms is an unfounded set for LP w.r.t. I if, for each a ∈ X, at least one of the following conditions holds for each rule r ∈ ground(LP) such that a ∈ H(r):

1. B(r) ∩ (¬.I ∪ X) ≠ ∅, or

2. H(r) ⊈ (¬.I ∪ X).

An unfounded set X is consistent w.r.t. I if X ∩ I^{+} = ∅.

For normal programs unfounded sets have been introduced to draw negative inferences for the constructive definition of the well-founded model [36] (recall that the well-founded model is indeed defined as the limit of the sequence I_{0} = ∅, I_{n} = T_{P} (I_{n−1}) ∪ ¬.U_{P} (I_{n−1}), where T_{P} is the immediate consequence operator and U_{P} (I) denotes the greatest unfounded set w.r.t. I). Thus, they can be seen as a sort of CWA rule allowing to derive negative information (i.e., the falsity of some atoms).

Unfounded sets for disjunctive programs play essentially the same role. Indeed, if X is a consistent unfounded set (i.e., I ∪ ¬.X is an interpretation), for every rule r having an element of X in the head, either the body of r is false w.r.t. I ∪ ¬.X (Condition 1 of Definition 1), or the head of r is not false w.r.t. I ∪ ¬.X (Condition 2 of Definition 1). Thus, if if we think in terms of classical (2-valued) interpretations, it is possible to extend I by assuming that all atoms in X are false,^{3} without explicitly violating r; in fact, rule r is still satisfiable: if Condition 1 applies, then r is definitely satisfied (as the body is false), and if Condition 2 applies, r can be satisfied by assuming that the atoms in H(r) − X are true. Since the atoms in X are “defined” only by such rules r (under the intended assignment-based reading of rules), intuitively every atom in X should be false, since the assumption that it is true is not much founded, according to a principle of closed world assumption. (For a more elaborate discussion on this, see Section 5.)

Example 1 Consider the program LP = {a ∨ b ←} and the interpretation I = ∅. The set X = {a} is a (consistent) unfounded set of LP w.r.t. I. Indeed, the unique rule of ground(LP) (with a in the head) satisfies Condition 2 of Definition 1, as H(r)−(X∪¬.I) = {b}. Likewise, we can easily verify that Y = {b} is a (consistent) unfounded set for LP w.r.t. I (as H(r) − (Y ∪ ¬.I) = {a}). For the program LP = { a ∨ b ← ; a ← b ; b ← a } and the interpretation I = {a, b} the only unfounded set is ∅.

2In the context of classical (2-valued) logic, where interpretations are total, (total) models are identified with their positive parts. Within the context of partial (3-valued) interpretations, however, their negative parts are mentioned as well, to stay consistent with the framework.

3Note that assuming false a literal which is in I^{+} would cause inconsistency.

We remark that a first attempt for generalizing the notion of unfounded set may lead to adopt for Condition 2 the stronger requirement (H(r)−X)∩I^{+} ≠ ∅, i.e., an atom from the head of r apart from X is true in I. This definition has been adopted in [20], where it unfounded set are used to characterize 2-valued stable models. However, this (stronger) condition turns out to be too strong to capture unfoundedness appropriately with respect to 3-valued semantics of rules that we consider later. Namely, if the head of a rule as well as its body is undefined in I, i.e., neither definitely true nor false, we nevertheless can conclude that –in the extremal case– all atoms in the head except one can be false, without definitely violating the rule (which happens if the body is true and the head is false). Arriving at such a conclusion is essential, however, in a form of the closed world assumption which is inherent to 3-valued stable semantics.

It is worth pointing out that the above definition generalizes the standard definition of unfounded set given for normal programs in [36]: X is a (standard) unfounded set for a normal program LP w.r.t. I if, for each a ∈ X, for each rule with head a, B(r)∩(¬.I∪X) ≠ ∅ holds.

Proposition 1 Let LP be a normal program and I an interpretation for LP. X ⊆ B_{LP} is an unfounded set for LP w.r.t. I according with Definition 1 if and only if it is a standard unfounded set for LP w.r.t. I.

Proof. For a normal program, Condition 2 of Definition 1 is never satisfied since H(r) ⊆ X, as H(r) is made of a single element which belongs to X. Thus, for a normal program, Definition 1 reduces to the standard definition of unfounded set.

It is known that for normal programs, the union of two unfounded sets is an unfounded set as well. This property does not extend to disjunctive programs.

Example 2 Consider again the program LP = {a ∨ b ←} and the interpretation I = ∅. In Example 1 we have seen that both {a} and {b} are unfounded sets for LP w.r.t. I, but we can easily verify that the union X = {a, b} is not. Indeed, take any element in X, say a; although a is not false w.r.t. I, b is not unfounded as a is also in X (so that Condition 2 of Definition 1 does not hold). Intuitively, this represents the fact that we can falsify either a or b, but at least one of them must remain not false (otherwise the rule a ∨ b ← becomes unsatisfiable).

Since the union of all unfounded sets is not necessarily an unfounded set, we cannot define the greatest unfounded set of an interpretation; instead, we next provide a notion of maximal unfounded set.

A consistent unfounded set X w.r.t. I is a maximal unfounded set for LP w.r.t. I if no proper superset Y of X is a consistent unfounded set for LP w.r.t. I.

Example 3 Let LP = {a ∨ b ←}. Both X_{1} = {a} and X_{2} = {b} are maximal unfounded sets for LP w.r.t. I = ∅.

X_{1} is the only maximal unfounded set for LP w.r.t. the interpretation {b} (note that X_{2} is not a consistent unfounded set w.r.t. {b}).

Let LP_{1} be the following program:

\begin{aligned}a ∨ b & ← \\ d & ← ¬d, ¬b \\ a ∨ c & ← ¬d \end{aligned}

M_{1} = {a, ¬b, ¬c} has the single maximal unfounded set X_{1} = {b, c}; M_{2} = {b, c, ¬a, ¬d} has the single maximal unfounded X_{2} = {a, d}.

Intuitively, a maximal unfounded set X is a maximal set of atoms that can be assumed false without violating the satisfiability of the rules of the program that contain some atom from X. Consistency of the unfounded set X ensures that the assumption of the falsity of the literals in X is consistent with I (that is, I ∪ ¬.X is an interpretation).

For instance, we have seen in the above examples that for the program LP = {a∨b ←} both {a} and {b} are (consistent) unfounded sets w.r.t. I = ∅ while {a, b} is not an unfounded set. Indeed, we can assume the falsity of either a or b without violating the satisfiability of a ∨ b ← (which can be satisfied by making true b or a, respectively); but we cannot assume the falsity of both a and b at the same time, as in the latter case we would have no way to satisfy rule a ∨ b ←.

P-Stable Models

Once we provided a notion of unfounded set for disjunctive programs, we define P-stable models for such programs by extending the respective definition given in [32, 31] for normal programs.

To proceed, we need the concept of foundedness of an interpretation. Foundedness, called justifiability in [37, 38], basically prescribes that every positive literal in an interpretation must be be derived from the rules possibly using negative literals as additional axioms.

Let for any positive (i.e., ¬-free) program P denote MM(P) the set of the minimal total models of P [23], where a total model M is minimal iff there does not exist a total model N of P such that N^{+} ⊂ M^{+}. Moreover, let for any program LP and interpretation I be LP(I) the program obtained from ground(LP) as follows: (i) remove all rules r having a negative literal ¬p ∈ B(r) such that ¬p ∉ I^{−}, and (ii) by remove all negative literals from the remaining rules.

Definition 2 An interpretation I of a program LP is founded iff I^{+} = M^{+} for some M ∈ MM(LP(I)).

Notice that LP(I) is essentially the 2-valued Gelfond-Lifschitz transform [16], carried out in the context of partial interpretations.

Example 4 Consider the program LP_{1} of Example 3. Interpretation M_{1} = {a, ¬b, ¬c} is founded. Indeed, LP_{1}(M_{1}) is the following program:

a ∨ b ←

and there exists a minimal total model N of LP_{1}(M_{1}) such that N^{+} = M_{1}^{+}, namely N = {a, ¬b}. For M_{2} = {b, c, ¬a, ¬d}, LP_{1}(M_{2}) is as follows:

\begin{aligned}a ∨ b & ← \\ a ∨ c & ← \end{aligned}

Also M_{2} is founded, since N = {b, c, ¬a} is a minimal total model of LP_{1}(M_{2}) and N^{+} = M_{2}^{+}.

For total interpretations foundedness alone is sufficient to characterize (2-valued) stable models, which are indeed defined as the total founded interpretations of the program [16, 26]. However, as for normal programs [29], foundedness alone is not sufficient to single out 3-valued stable models, as some conditions on the false literals are needed. Intuitively, what must be imposed on the false literals for a founded interpretation I to be a (partial) stable model is the consistency with the closed world assumption. In other words, every false literal in I must be definitely not derivable from the rules of the program (assuming I), and no further literal must be declarable false without violating some rule of the program. As we informally observed above, this consistency with the CWA is precisely formalized by the notion of maximal unfounded set.

Definition 3 (P-stable Model) Let LP be a program and M an interpretation of it. Then M is a P-stable (partial stable) model of LP if the following conditions hold:

(a) M is founded,

(b) ¬.M^{−} is a maximal unfounded set for LP w.r.t. M.

Note that Condition (a) characterizes the true atoms of M, imposing that they have to be “justified” [37], while condition (b) characterizes the false atoms of M, requiring that they must be all and only the atoms that can be assumed false consistently with M and with the rules of the program (further negative assumptions would make some rule unsatisfiable).

Example 5 Consider the program LP_{1} of Example 3. Both M_{1} = {a, ¬b, ¬c} and M_{2} = {b, c, ¬a, ¬d} are P-stable models of LP_{1}. Indeed, we have seen in Example 4 that M_{1} and M_{2} are founded, and Example 3 showed that ¬.M_{1}^{−} and ¬.M_{2}^{−} are maximal unfounded sets w.r.t. M_{1} and M_{2}, respectively. On the other hand, the interpretation M_{3} = {a, ¬d} is not a P-stable model of LP_{1}. While M_{3} is founded (note that LP_{1}(M_{3}) = {a ∨ b ← , a ∨ c ← }), ¬.M_{3}^{−} is not a maximal unfounded set w.r.t. M_{3}; indeed, M_{3} has the single maximal unfounded set X = {b, c}.

We close this section justifying that Definition 3 coincides on normal programs with the definition given in [32].

Proposition 2 Let LP be a normal program. M is a P-stable model for LP according with Definition 3 if and only if M is a P-stable model according with [32].

Proof. In [32] an interpretation M is a P-stable model if it is founded (according to the definition there) and ¬.M^{−} = GUS_{LP}(M), i.e., the greatest unfounded set of LP w.r.t. M (which always exists for a normal program). Our notion of foundedness amounts on normal programs to the notion in [32]. Moreover, for normal programs it is easily checked that any unfounded set X w.r.t. a founded interpretation I satisfies X ∩ I = ∅, and hence each unfounded set X w.r.t. I is consistent. Therefore, if M is founded, ¬.M^{−} = GUS_{LP}(M) if and only if ¬.M^{−} is a maximal unfounded set for LP w.r.t. M. Consequently, the two definitions coincide.

As a corollary we obtain the following result.

Corollary 1 Let LP be a normal program. M is a P-stable model for LP if and only if it is a 3-valued stable model for LP according with [26].

Proof. In [30] it is proven that on normal programs the P-stable models of [32] coincide with the 3-valued stable models of [26]. Thus, the result follows from Proposition 2.

Corollary 1 shows that P-stable models coincide with 3-valued stable models on normal programs. The next section proves that this equivalence result extends to disjunctive programs.

3 P-stable and 3-Valued Stable Models

In this section we show that the definition of P-stable model (Definition 3) is equivalent to the definition of 3-valued stable model as given in [26]. To this end, following [26], we define a 3-valued logic with T (True), F (False), and U (Undefined), ordered as F < U < T. Given a program LP, an interpretation I of LP, and a ground literal L,

value_{I}(L) = \{ \begin{matrix}T, & if L ∈ I; \\ F, & if L ∈ ¬.I; \\ U, & otherwise (i.e., L ∈ \overline{I} ∪ ¬.\overline{I}). \end{matrix}

The value of a conjunction C = L_{1}, …, L_{n} of ground literals is the minimal value of the literals in the conjunction (i.e., value_{I}(C) = min({value_{I}(L_{i}) | 1 ≤ i ≤ n}) ); if C is empty, then we assume value_{I}(C) = T. The value of a disjunction D = L_{1} ∨ ⋯ ∨ L_{n} of ground literals is the maximum value of the literals in the disjunction (i.e., value_{I}(D) = max({value_{I}(L_{i}) | 1 ≤ i ≤ n}) ). A ground rule r is satisfied by I if value_{I}(H(r)) ≥ value_{I}(B(r)).

Definition 4 (3-valued Model)[26] Let LP be a program and M be an interpretation for LP. Then, M is a 3-valued model for LP if every rule r in ground(LP) is satisfied by M.

The definition of 3-valued stable model involves a 3-valued version of the Gelfond-Lifschitz (GL) transformation [26] and resorts to the notion of 3-valued program that we report next. A 3-valued program is a program LP where the constants T, U and F may occur as body literals in the rules of LP. We assume that in every interpretation I the literal T is true, the literal F is false, and the literal U is undefined. Thus, such literals can be thought of as already interpreted ground literals.

Given an interpretation I for a program LP, the GL-transformation \frac{LP}{I} of LP w.r.t. I is the positive 3-valued program obtained from ground(LP) by replacing in the body of every rule all negative literals which are true (resp. undefined, false) by T (resp. U, F). An interpretation M for LP is a 3-valued model for \frac{LP}{I} if it satisfies every rule in \frac{LP}{I}. A 3-valued model M for \frac{LP}{I} (resp. LP) is minimal if there does not exist a 3-valued model M_{1} ≠ M for \frac{LP}{I} (resp. LP) such that M_{1}^{+} ⊆ M^{+} and M_{1}^{−} ⊇ M^{−}. In [26] it has been proven that \frac{LP}{I} has at least one minimal 3-valued model.

Definition 5 (3-Valued Stable Model)[26] Let LP be a program and M be a 3-valued model for LP. Then, M is a 3-valued stable model for LP iff M is a minimal 3-valued model of \frac{LP}{M}.

Notice that each 3-valued stable model of LP is a 3-valued model of LP, and in fact a minimal 3-valued model [26].

Even if Definitions 5 and 3 are apparently quite different (the former relies on three valued logic, while the latter is based on unfounded sets), they yield exactly the same notion of stable model.

Example 6 Consider the program LP_{1} of Example 3:

\begin{aligned}a ∨ b & ← \\ c & ← a, d \\ d & ← ¬c \end{aligned}

We have seen in Example 5 that M_{1} = {a, ¬b, ¬c} is a P-stable model for LP_{1}. It is easy to see that M_{1} is also a 3-valued stable model for LP_{1}. Indeed, \frac{LP_{1}}{M_{1}} is the following 3-valued program:

\begin{aligned}a ∨ b & ← \\ d & ← U, T \\ a ∨ c & ← U, \end{aligned}

and M_{1} is a minimal 3-valued model of \frac{LP}{M_{1}} . Similarly, M_{2} = \{b, c, ¬a, ¬d\}, which has been proven to be a P-stable model of LP_{1} in Example 5, is a 3-valued stable model for LP_{1}, as it is a minimal 3-valued model of \frac{LP_{1}}{M_{2}} , which is as follows:

\begin{aligned}a ∨ b & ← \\ d & ← T, F \\ a ∨ c & ← T. \end{aligned}

However, the interpretation M_{3} = {a, ¬d} is not a 3-valued stable model of LP_{1}; in fact, M_{3} is not a 3-valued model of LP_{1} (it violates the rule d ← ¬d, ¬b), and hence it can not be a 3-valued stable model of LP_{1}.

The sequel of the section is devoted to formally demonstrate the equivalence between Definitions 5 and 3. The proof of this equivalence requires some preliminary result.

Lemma 1 Let M be a P-stable model for a program LP. Then, M is a 3-valued model for both LP and \frac{LP}{M}.

Proof. It is immediately recognized that M is a 3-valued model for LP if and only if it is a 3-valued model for \frac{LP}{M}. It is thus sufficient to prove that M is a 3-valued model for LP. Let r be a rule in ground(LP). We have to prove that: (a) value_{M}(H(r)) = F ⇒ value_{M}(B(r)) = F, and (b) value_{M}(H(r)) = U ⇒ value_{M}(B(r)) ≠ T. (a). If value_{M}(H(r)) = F then all atoms in the head of r are false. Since M is a P-stable model, from Definition 3, ¬.M^{−} is an unfounded set w.r.t. M. Therefore, r (whose head contains elements in ¬.M^{−}) must satisfy at least one of the unfoundedness conditions of Definition 1 for X = ¬.M^{−} w.r.t. M. Now, Condition 2 cannot be verified, as H(r) ⊆ ¬.M^{−}. Therefore, B(r) ∩ ¬.M ≠ ∅, and, as a consequence, value_{M}(B(r)) = F (note that, since X = ¬.M^{−}, ¬.M ∪ X = ¬.M). (b). We prove the contrapositive: value_{M}(B(r)) = T ⇒ value_{M}(H(r)) ≠ U. Let value_{M}(B(r)) = T hold. Then, the rule r′ obtained from r by deleting all negative body literals is in LP(M), as all negative body literals of r are true w.r.t. M. The body of r′ is true w.r.t. M (as B(r′) ⊆ B(r) ⊆ M). Since M is founded, by Definition 3 M^{+} = N^{+} for some N ∈ MM(LP(M)); consequently, B(r′) ⊆ M implies that H(r′)∩M ≠ ∅. Therefore, value_{M}(H(r)) = T (hence, value_{M}(H(r)) ≠ U), as H(r′) = H(r).

We are now in the position to prove that every P-stable model is a 3-valued model.

Theorem 1 Let M be a P-stable model for a program LP. Then, M is a 3-valued stable model for LP.

Proof. From Definition 5, we have to demonstrate that M is a minimal 3-valued model for \frac{LP}{M}. By Lemma 1, it remains to prove only the minimality of M. We proceed by contradiction. Assume that M_{1} ≠ M is a 3-valued model for \frac{LP}{M} such that M_{1}^{+} ⊆ M^{+} and M_{1}^{−} ⊇ M^{−}. We proceed as follows: we first prove that (a) M_{1}^{+} cannot be a proper subset of M^{+} and after that, using (a), we show that (b) M_{1}^{−} cannot be a proper superset of M^{−}.

(a). Assume that M_{1}^{+} ⊂ M^{+} and let N be the total interpretation of LP(M) such that N^{+} = M_{1}^{+} (and N^{−} = B_{LP} − M_{1}^{+}). We demonstrate that N is a total model for LP(M), which contradicts the foundedness of M given for M by Definition 3. Let r be any rule in LP(M), let r′ be a rule in ground(LP) from which r comes (i.e., r′ is the rule H(r) ← B^{+}(r)), and r′′ be the GL-transformed of r′ in \frac{LP}{M}. Observe first that, since r is in LP(M), all negative literals in B(r′) are true w.r.t. M and, as a consequence, they have been replaced in r′′ by T (and they do not appear in r). Therefore, the body of r is true w.r.t. N (i.e., B(r) ⊆ N) iff the body of r′′ is true in M_{1} (i.e., value_{M_{1}}(r′′) = T).

Now, if B(r) ⊈ N then r is satisfied by N, as its body is false. On the other hand, if B(r) ⊆ N, then B(r′′) is true w.r.t. M_{1} (i.e., value_{M_{1}}(r′′) = T); since M_{1} is a 3-valued model for \frac{LP}{M}, H(r′′) is true w.r.t. M_{1}, i.e., H(r′′) ∩ M_{1}^{+} ≠ ∅. As H(r) = H(r′′), it follows that r is satisfied by N. Hence, N is a total model for LP(M) such that N^{+} ⊆ M^{+}. This raises a contradiction to the fact that M is founded. (b). From point (a) above, we know that M_{1}^{+} = M^{+}. We next prove that ¬.M_{1}^{−} is an unfounded set w.r.t. M. Thus, if M_{1}^{−} is a proper superset of M^{−}, then Condition (b) of Definition 3, i.e. the maximality of the unfounded set M^{−}, is contradicted.

To demonstrate that ¬.M_{1}^{−} is an unfounded set w.r.t. M, we have to prove that, given any rule r in ground(LP) having an atom a from ¬.M_{1}^{−} in the head, r satisfies at least one of the conditions of Definition 1 for X = ¬.M_{1}^{−} w.r.t. M. Let r′ be the GL-transformed of r in \frac{LP}{M}. If the body of r′ is false w.r.t. M_{1}, then r satisfies Condition 1 of Definition 1 for X w.r.t. M. Otherwise (i.e., the body of r′ is not false w.r.t. M_{1}), since M_{1} is a 3-valued model for \frac{LP}{M}, the head of r′ contains some literal which is not false w.r.t. M_{1} (that is, H(r′) − ¬.M_{1}^{−} ≠ ∅). Therefore, as H(r′) = H(r) and X ∪ ¬.M^{−} = ¬.M_{1}^{−}, r satisfies Condition 2 of Definition 1 for X w.r.t. M. Thus, ¬.M_{1}^{−} is an unfounded set w.r.t. M. Consequently, M_{1}^{−} cannot be a proper superset of M^{−}. (We are done.)

The proof of the converse of Theorem 1 is divided in the following two lemmata.

Lemma 2 Every 3-valued stable model is founded.

Proof. Let M be a 3-valued stable model for LP. By contradiction, assume that the total interpretation N of LP(M) such that N^{+} = M^{+} is not a minimal total model of LP(M). Then, there exists a total model N1 for LP(M) such that N1^{+} is a proper subset of M^{+}. We show that the interpretation J = N1^{+} ∪ M^{−} is a 3-valued model for \frac{LP}{M}; this implies that M is not a minimal 3-valued model of \frac{LP}{M}, and hence contradicts that M is a 3-valued stable model of LP.

Let r be any rule in \frac{LP}{M} and r′ be a rule in ground(LP) from which r is obtained. We show by considering the three possible values of B(r) in J that r is satisfied in J, which means that J is a 3-valued model of \frac{LP}{M}, and raises the desired contradiction: (a) B(r) is false in J: Then, r is clearly satisfied by J. (b) B(r) is true in J: Then, all negative literals of the body of r′ must be true in M. Thus, a rule r′′ in LP(M) exists such that B(r′′) = B^{+}(r′) and H(r′′) = H(r′). B(r′′) is clearly true w.r.t. N1; hence, H(r′′) is true in N1 (as N1 is a model of LP(M)), and, since H(r) = H(r′′) and J^{+} = N1^{+}, H(r) is true w.r.t. J. Thus, r is satisfied in J. (c) B(r) is undefined w.r.t. J: Assume that H(r) is false w.r.t. J. Then, H(r) ⊆ ¬.M^{−}. Therefore, H(r′) is false w.r.t. M. Since M is a 3-valued stable model for LP, it is a 3-valued model of LP and hence B(r′) is false w.r.t. M. Thus, B(r) is false w.r.t. J, as either it contains the constant F (if a negative literal of r is false w.r.t. M) or it contains a positive literal which is in M^{−} (which coincides with J^{−}). Hence, by (a)–(c), r is satisfied in J. (We are done.)

Lemma 3 If M is a 3-valued stable model, then ¬.M^{−} is a maximal unfounded set w.r.t. M.

Proof. Let M be a 3-valued stable model for LP. It is easy to see that ¬.M^{−} is an unfounded set for LP w.r.t. M. Indeed, since M is a 3-valued model for LP, every rule with a literal from ¬.M^{−} in the head either has a false body (if all head literals are false) or its head contains some literal which is not in ¬.M^{−}. To see that ¬.M^{−} is a maximal unfounded set, i.e., there does not exist an X with ∅ ≠ X ⊆ \overline{M} such that X ∪ ¬.M^{−} is an unfounded set w.r.t. M, we demonstrate that the existence of such an X entails J = ¬.X ∪ M is a 3-valued model for \frac{LP}{M}, which contradicts the minimality of M for \frac{LP}{M} and hence that fact that M is a 3-valued stable model of LP. To this end, consider any rule r in \frac{LP}{M}, which is obtained from a rule r′ in ground(LP). We show that r is satisfied in J. As a consequence, J is a 3-valued of \frac{LP}{M}, which raises the desired contradiction.

Clearly, value_{J}(B(r)) ≤ value_{M}(B(r)). To show that r is satisfied in J, it thus suffices to show that value_{J}(H(r)) < value_{M}(H(r)) implies value_{J}(B(r)) = F. Under the hypothesis, H(r) ∩ X ≠ ∅. Since J^{+} = M^{+}, it follows that value_{J}(H(r)) = F. Since X ∪ ¬.M^{−} is an unfounded set w.r.t. M and H(r) = H(r′), it follows by Condition 1 of Definition 1 that B(r′) ∩ (¬.M ∪ X ∪ ¬.M^{−}) ≠ ∅, i.e. B(r′) ∩ ¬J ≠ ∅ (note that J = M ∪ ¬.X∪M^{−}). Consequently, B(r′) is false in J, which clearly means that value_{J}(B(r)) = F. Thus, r is satisfied in J. (We are done.)

We can finally state the main theorem of this section.

Theorem 2 M is a P-stable model for a program LP if and only if M is a 3-valued stable model for LP.

Proof. Follows from Theorem 1 and Lemmata 2 and 3.

Thus, Definition 3 can be seen as a characterization of 3-valued stable models which does not resort to 3-valued logic.

4 Partial Stable Models which Minimize Undefinedness

A major objection against P-stable models is the fact that they leave more atoms undefined than necessary [37, 38].

The simplest way to select the P-stable models which are closer to the principle of minimal undefinedness is to discard those properly included in some other P-stable.

Definition 6 (M-stable Model) A P-stable model M is M-stable (Maximal stable) if there exists no P-stable model N of LP which is a proper superset of M.

Example 7 Consider the following program LP.

\begin{aligned}a & ← ¬b \\ b & ← ¬a \\ c ∨ d & ← a \\ d & ← c \end{aligned}

The P-stable models of LP are:

\begin{aligned}M_{1} & = \{b, ¬a, ¬c, ¬d\}, \\ M_{2} & = \{a, d, ¬b, ¬c\}, \\ M_{3} & = \{¬c\} \end{aligned}

M_{1} and M_{2} are also M-stable models, while M_{3} is not (as it is a subset of the P-stable model M_{1}, as well as of M_{2}).

The M-stable models of the program LP_{1} in Example 3 are M_{1} = {a, ¬b, ¬c} and M_{2} = {b, c, ¬a, ¬d}.

A principal aspect of M-stable models is that they coincide with several concepts of acceptable models for a normal program.

Proposition 3 On a normal program LP, Definition 6 coincides to the definitions of M-stable models of [29, 32, 31], preferred extensions of [9], the regular models of [37] and the maximal stable classes of [3].^{4}

Proof. Let LP be a normal program and M be an interpretation for LP. As a consequence of Proposition 2, M is M-stable according with Definition 6 if and only if it is M-stable according with [29, 32, 31]. Therefore, the statement follows from the results in [17] and [39].

M-stable models, however, are only a first step to minimize undefinedness. The class of P-stable models which completely fulfills minimal undefinedness is that of L-stable models.

Definition 7 (L-stable Model) A P-stable model M is L-stable (Least-undefined stable) if the set of its undefined atoms is minimal, i.e., there exists no P-stable model N of LP such that \overline{N} ⊂ \overline{M}.

Example 8 Consider the program LP of Example 7. Both M-stable models M_{1} = {b, ¬a, ¬c, ¬d} and M_{2} = {a, d, ¬b, ¬c} are also L-stable models for LP.

For the program LP_{1} in Example 3, the M-stable model M_{2} = {b, c, ¬a, ¬d} is also L-stable; on the other hand, M_{1} = {a, ¬b, ¬c} is M-stable but it is not L-stable.

4Note that maximal stable classes are formally defined in [38] by slightly modifying the stable classes presented in [3].

Let PS_{LP}, MS_{LP}, LS_{LP}, and TS_{LP} be the sets of models of a program LP that are P-stable, M-stable, L-stable and T-stable, respectively. We shall omit the subscript LP whenever LP is understood from the context.

Proposition 4 Let LP be a program. Then

(a) TS ⊆ LS ⊆ MS ⊆ PS;

(b) (TS ≠ ∅) ⇒ TS = LS

Proof. Part (a). MS ⊆ PS holds by Definition 6. Moreover, by Definition 7 it is clear that LS ⊆ MS. On the other hand, a T-stable model M is L-stable as well, since there exists no P-stable model N of LP such that \overline{N} ⊂ \overline{M}, as \overline{M} = ∅. Part (b). Let (TS ≠ ∅) and N ∈ TS. From the proof of Part (a) it remains to prove only that TS ⊇ LS, that is, every L-stable model is T-stable as well. Let M ∈ LS. Since N is also a P-stable model, from Definition 7, \overline{N} ⊂ \overline{M} does not hold. Therefore, \overline{M} = ∅, as \overline{N} = ∅. Thus, M is in TS as well.

Thus a T-stable model is also L-stable, an L-stable model is also M-stable which is in turn P-stable, but the converse implications do not in general hold. Finally, whenever there exists a T-stable model, the definitions of T-stability and L-stability coincide.

As somehow expected, on the class of (even locally) stratified disjunctive programs, the families of P-stable models collapse into a single one.

A program LP is (locally) stratified [25] if to each ground atom p of B_{LP} can be associated a positive integer l(p) such that, for each rule r ∈ LP having p ∈ H(r) and ground atom q appearing in r, the following holds: (i) if q appears in H(r), then l(p) = l(q); (ii) if q appears in B^{−}(r), then l(p) > l(q); and (iii) if q appears in B^{+}(r), then l(p) ≥ l(q).

In particular, if all ground atoms with the same predicate have the same number associated, then LP is globally stratified.

The following proposition is an immediate consequence of Proposition 2 and the coincidence of 2-valued and 3-valued stable models on locally stratified programs [26].

Proposition 5 Let LP be a program. If LP is (locally) stratified, then PS_{LP} = MS_{LP} = LS_{LP} = TS_{LP}.

Proof. It is known that on locally stratified programs, 2-valued and 3-valued stable models coincide [26]. Therefore, from Theorem 2, TS = PS. Thus, the statement follows from Proposition 4.(a).

We close the section with a short discussion aimed at exemplifying the differences between the various stable models.

Example 9 We have seen that the various stable model semantics differ only on unstratified programs. Unstratified negation is usually employed to specify some constraints that the stable models have to satisfy.

For instance, consider an undirected graph G = ⟨V, E⟩ represented by two predicates v and e whose instances specify the nodes and the edges of the graph, respectively, where e is assumed to be symmetric. We want to individuate the partitions ⟨A, B⟩ of V, i.e. disjoint nonempty subsets A and B of V with A ∪ B = V, such that no edge connects any node in A with any node in B.

The solutions to this problem can be easily found by a program using the total stable semantics. Consider the following program LP^{G}.

\begin{matrix}r_{1} : & a(X) ∨ b(X) ← v(X) \\ r_{2} : & abs(X) ← a(X), b(Y), e(X, Y), ¬abs(X) \\ r_{3} : & non empty ← a(X), b(Y) \\ r_{4} & non empty ← ¬non empty \end{matrix}

Intuitively, rule r_{1} “guesses” a partition ⟨A, B⟩ of V (i.e, a two sets of atoms with predicates a and b); the (unstratified) rule r_{2} enforces the constraint on disjointness of ⟨A, B⟩ 5, r_{3} and r_{4} enforce the constraint on nonemptiness of ⟨A, B⟩. It is worth noting how disjointness is enforced by r_{2}: if no node x in A is connected to a node y in B (that is, for X = x, the conjunction a(X), b(Y), e(X, Y) is false for any instantiation of Y), then A∪B is a total stable model, since all instances of r_{2} have a false body. If, on the contrary, a node x in A is connected to a node in y in B, an inconsistency arises in an instance of r_{2} (as the conjunction a(x), b(y), e(x, y) is true) and ⟨A, B⟩ does not yield a total stable model.

Rules r_{3} and r_{4} enforce that the partition is not trivial: because of r_{4}, non empty must be true in every stable model, and, since it must necessarily be derived from rule r_{3}, both A and B must contain at least one element.

Thus, every total stable model is a partition of the graph G and vice versa. That is, the total stable models of LP^{G} single out all and only the solutions of the given problem.

If the problem has no solution (i.e., there exists no non-trivial partition of the nodes, which satisfies disjointness), then LP^{G} has no stable model. In this case, it can be interesting to individuate the maximal (disjoint) partial partitions of the graph, i.e., the solution of the problem where the constraint A ∪ B = V is relaxed to A ∪ B ⊆ V. This is not possible with the program LP^{G} under total stable semantics. To solve this new (somewhat harder) problem, we modify rule r_{1} of LP^{G} by adding the literal ¬abs(X) in its body. The resulting program LP_{1}^{G} is reported below.

\begin{aligned}r′_{1} : & a(X) ∨ b(X) & ← & v(X), ¬abs(X) \\ r′_{2} : & abs(X) & ← & a(X), b(Y), e(X, Y), ¬abs(X) \\ r′_{3} : & non empty & ← & a(X), b(Y) \\ r′_{4} & non empty & ← & ¬non empty. \end{aligned}

Under total stable semantics, nothing changes, that is, there is a one-to-one correspondence between the total stable models of LP_{1}^{G} and the (total) solutions of the given problem. However, the L-stable models of LP_{1}^{G} allow us to identify the partial solutions of the problem. Intuitively, under partial stable semantics, if a node x of A is connected to some node in B in the “guessed” partition, then the choice of x (for A) is “annulled” by the presence of ¬abs(x) in r′_{1} which is necessarily undefined (because of rule r′_{2}). Thus, every P-stable model M represents a (possibly empty) disjoint partition of the graph, given by the atoms on a and b that are true in M. Let us see this in more detail. Let M be a P-stable model. To show that M is a disjoint partition, we have to demonstrate that if a(x) is in M, then e(x, y) does not hold, for any y such that b(y) ∈ M (that is, x ∈ A is not connected to any y ∈ B). Now, if a(x) ∈ M, then abs(x) must necessarily be false, and, as a consequence, no y is such that both b(y) and e(x, y) are true, since abs(x) could not be false in the latter case. Hence, for each x ∈ A (i.e., s.t. a(x) ∈ M), there does not exist y ∈ B (i.e., s.t. b(x) ∈ M) such that there is an edge from a to b. Therefore, M represents a disjoint partition of the graph (note that, since the e predicate is symmetric, we do not need to prove that there is no edge from B to A). Therefore, every P-stable model M represents a disjoint partition of the graph and, in particular, every L-stable model M represents a maximal disjoint partition of the graph.

5Note that abs may also be a 0-ary predicate, we have used a unary predicate to minimize the changes to the program for the next example.

On the other hand, it is soon recognized that if ⟨A, B⟩ is a maximal disjoint partition, then the interpretation

\begin{aligned}M = & \{a(x) | x ∈ A\} ∪ \{b(x) | x ∈ B\} ∪ \{¬b(x) | x ∉ A\} ∪ \{¬a(x) | x ∈ B\}∪ \\ & \{¬abs(x) | x ∈ A ∪ B\} ∪ N, \end{aligned}

is an L-stable model of the program, where N is either ∅ or {non empty} according whether ⟨A, B⟩ is trivial or not.

Since, by virtue of Proposition 4.(b), L-stable semantics differs from total stable semantics only if there is no total stable models, we have that L-stable semantics shows the following behavior:

• If the problem admits some “exact” solution (i.e., graph G admits some total partition), then there is a one-to-one correspondence between the L-stable models of LP_{1}^{G} and the total partitions of the graph.

• If the problem admits no “exact” solution (i.e., graph G admits no total partition), then, there is a one-to-one correspondence between the L-stable models of LP_{1}^{G} and the maximal partial partitions of the graph. (Note that in case the problem admits only trivial partitions, LP_{1}^{G} has only some L-stable models representing them, where non empty is not true).

Thus, L-stable semantics gives exactly what one is looking for, since we are interested in partial partitions (approximate solutions) only if there is no total partition (as in presence of exact total solutions of the problem, we would like that the program singles out only them).

In other words, L-stable semantics allows us to find “approximate” (i.e., maximal partial) solutions of the problem in case where the problem admits no exact solution, giving the exact solutions if they exist.

It is worth observing the behavior of M-stable semantics in this case. Every M-stable model of LP_{1}^{G} is a partition of the graph but, differently from L-stable models, it is not necessarily a maximal partition. The problem is that it may happen that a P-stable model describes a partition which can not be extended to a maximal partition. For instance, consider the following graph:

[figure: 3; 2; 1]

The graph has three vertices 1–3, and only one edge, which connects 2 and 3. Then, the following interpretation is a P-stable model of the program:

M = {a(1), ¬b(1), ¬abs(1), ¬a(2), b(2), ¬abs(2), ¬b(3), non empty}

This corresponds to the partition A = {1} and B = {2}. Now, it is not possible to extend this model M by adding atom b(3), to arrive at a model corresponding to the partition A = {1}, B = {2, 3} which is maximal (note that this is possible with L-stable semantics).

The problem is that the ’b-atoms’ which are not in the current set B, must be false and hence can not be included in a larger P-stable model. Thus, in order to obtain the maximal partitions under M-stable semantics we have to prevent that ’b-atoms’ which are not in the current set B are made false even if they are not in the set A. To this end, consider the program LP_{2}^{G} = LP_{1}^{G} ∪ {b(X) ← abs(X)}. Due to the inclusion of the latter rule, if a node x is neither in A nor in B, then both a(x) and b(x) are undefined in every P-stable model of LP_{2}^{G} (note that b(x) is false in the P-stable models of LP_{1}^{G}). In this way, if a P-stable model M of LP_{2}^{G} describes a partition which is not maximal, then M is not M-stable, as it can be extended to a larger stable model which represents the maximal partition.

Hence, the maximal partitions of the graph can be singled out also by M-stable semantics, but the appropriate program is less intuitive. Moreover, in case that the problem admits total partitions (i.e., LP_{2}^{G} admits total stable models), differently from the L-stable semantics, M-stable semantics gives also the partial maximal partitions of the graph (which are unwanted in this case).

Example 9 confirms our claim that L-stable model is the natural relaxation of the notion of total stable model and that L-stable semantics is the best way to ”approximate“ T-stable semantics. One may now ask why we presented M-stable models also. The reason for that is mainly twofold:

• First, on normal programs the concept of M-stable model turned out to be important, since it coincides with several proposals for the intended models of a program, which have been for formulated in quite different settings [3, 9, 29, 32, 31, 39]. Thus, the generalization of this concept to the class of disjunctive programs is natural, similar as the generalization of stable models or regular models for normal programs to disjunctive programs [26, 38].

• Second, as shown in Section 6.1, M-stable models present some desirable modularity properties which make them amenable from the methodological and computational point of view, especially in the context of deductive databases.

5 Comparison with Regular Models

The notion of regular model [37, 38] is similar in spirit to M-stable model, but is based on a weaker concept of model than P-stable model.

Definition 8 (Regular Model)[38] Let LP be a program and M an interpretation of it. M is a regular model of LP if the following conditions are satisfied.

(a) M is a 3-valued model of LP,

(b) M is founded, and

(c) no founded 3-valued model N of LP such that N ⊃ M.

(Observe that Condition (b) is called justifiability in [37, 38].) Thus, regular models are very close to M-stable models. At a first glance, one can even think that the two definitions coincide: both regular and M-stable are founded 3-valued models, and maximal under set inclusion. This is in fact the case for normal programs (cf. Proposition 3). However, a closer look to the definitions reveals that Definition 8 is different from Definition 6. Let RS_{LP} and FS_{LP} denote the family of regular and founded 3-valued models of LP, respectively. In general, we have the following relation between RS_{LP} and MS_{LP}.

Proposition 6 Let LP be a program. Then, for every M-stable model M ∈ MS_{LP} there exists a regular model N ∈ RS_{LP} such that M ⊆ N.

Proof. By Definition 6, every M-stable is a maximal element in PS. On the other hand, by Definition 3, every P-stable is founded and, by virtue of Theorem 1, is also a 3-valued model. Therefore, PS ⊆ FS. Since M-stable are maximal elements of PS and regular models are maximal elements of FS, the statement follows.

Proposition 6 does not exclude the possibility that the RS = MS (actually, as we will see later, the equality holds for a meaningful class of programs). However, the difference between the two families is soon recognized by the observation that every program admits a regular model [38], while there are programs that lack M-stable models (this is an immediate consequence of the fact that some programs miss 3-valued stable models [26]). The following example from [26] makes this point clear.

Example 10 Let LP be the program below.

work ∨ sleep ∨ tired ←
work ← ¬tired
sleep ← ¬work
tired ← ¬sleep

It is easy to see that LP has no P-stable model (cf. [26]), and hence no M-stable and L-stable model. On the other hand, {work}, {sleep}, and {tired} are (all the) regular models of LP.

At a first glance, the behavior of regular semantics can appear even more intuitive than that of M-stable semantics. However, as announced in the introduction, this behavior is somehow the proof that regular models do not respect the closed world assumption. The closed world assumption (CWA), introduced by Reiter in [27], informally states that an atom must be assumed false if it is not entailed from the theory. In logic programming the first explicit CWA rule, called Generalized CWA (GCWA), is due to Minker [23]. According with GCWA, if an atom a is false in every (total) minimal model of the program, then ¬a is assumed true. The closed world assumption has been the inspiring principle of the semantics of negation in logic programming and led to minimize the set of positive conclusions maximizing the negative ones. Since the semantics of a program LP is usually identified by a set of ”preferred” models for LP (e.g., the set of stable models or the wellfounded model), which can be seen as alternative meanings of LP, in the framework of normal programs, CWA can be restated as the following property that each preferred model M of a given semantics should satisfy:

“If every rule with A in the head has a false body w.r.t. M, then A must be false in M.”

It is easy to see that (at least in this weak form) the CWA is satisfied by many wellknown semantics for datalog. For instance, stratified models [2], Fitting’s models [15], well-founded models [36], both total and partial stable models [16, 26], and regular models [37] for normal programs satisfy the principle of CWA. Since it is widely acknowledged that inferences from disjunctive rules must follow a minimality criterion, the CWA can be suitably extended to disjunctive programs as follows:

“If every rule with A in the head has a false body or contains in the head an atom different from A that is true w.r.t. M, then A must be false in M.”

Minker’s minimal models [23] and both total and partial stable models [26] for disjunctive programs satisfy the CWA. As a consequence, both L-stable and M-stable models satisfy the CWA as well. On the contrary, regular models for disjunctive programs do not satisfy the CWA. To see the latter point, observe the above example and consider its regular model M = {sleep}: There are two rules with tired in the head, the former (work∨sleep∨ tired ←) contains the true atom sleep in the head, the other rule (tired ← ¬sleep) has a false body. Thus, according with the CWA rule, tired should be false in M; nevertheless, this atom is undefined. Hence, the existence of regular models for disjunctive programs which do not have M-stable models may be explained by the violation of the above closed world assumption by such regular models. Moreover, it is important to point out that regular models may not agree with M-stable models also for programs where M-stable models do exist.

[figure: .; .; .; .; .; TS; MS; LS; RS; PS; FS]

Figure 1: Relation between partial model semantics

Example 11 Consider the following extension LP′ of the program shown in Example 10.

adult ∨ child ←
work ∨ sleep ∨ tired ← adult
work ← ¬tired, adult
sleep ← ¬work, adult
tired ← ¬sleep

LP′ has a unique total stable model M = {child, ¬adult, ¬sleep, tired, ¬work}, which is also the unique P-stable, M-stable and L-stable model. Nevertheless, LP′ admits besides M three other regular models, namely {adult, ¬child, sleep}, {adult, ¬child, work}, and {adult, ¬child, tired}.

From Example 11, we derive that, differently from L-stable semantics, even if the program has some T-stable model, regular semantics does not necessarily agree with Tstable semantics.

Proposition 7 Let LP be a program. Then, TS ≠ ∅ ⇏ TS = RS.

In Example 11, where a unique total stable model exists, regular semantics does not coincide to total stable semantics, while P-stable and M-stable and L-stable do coincide. Unfortunately, for P-stable and M-stable models this desirable behavior cannot be generalized to all cases of existence of total stable models. On the contrary, as shown in Proposition 4.(b), L-stable models do always coincide to total stable models if some total stable exists. This property is very important, as it is generally acknowledged that if total stable models exist, they are the natural meaning of the program, and candidates L-stable models as the best “approximation” of total stable models.

The Hasse diagram of the inclusion order between different sets of partial models is displayed in Figure 1.

Thus, in general, the concepts of models are different. The two following propositions identify simple classes of programs where the models coincide. An immediate result is that all families of models coincide on the class of stratified programs.

Proposition 8 Let LP be a stratified program. Then PS_{LP} = MS_{LP} = LS_{LP} = TS_{LP} = RS_{LP}.

Proof. From [38], on stratified programs we have that TS_{LP} = RS_{LP}. Thus, the statement follows immediately from Proposition 5. .

Another known equivalence between M-stable and regular models holds for normal programs as already mentioned in Proposition 3.

Proposition 9 [39] Let LP be a normal program. Then MS_{LP} = RS_{LP}.

From the results of Propositions 8 and 9, a natural question arises: is it possible to enlarge the class of normal programs on the one hand and stratified disjunctive programs on the other, by possibly combining such programs, ensuring that MS = RS still holds? An answer to this issues is provided by corollaries to the results in the next section. Informally, if we start from a normal or disjunctive program, and impose on top a (another) normal program that uses the relations computed by the “lower” program like input relations, then M-stable and regular models coincide. Notice that this class greatly extends stratified disjunctive programs to programs that allow for unstratified rules.

6 Modularity Property of Partial Semantics

In this section we first derive some modularity properties for partial semantics. Then, we apply the results to enlarge the class of programs on which M-stable and regular models are known to coincide. Moreover, we also derive useful computational properties for for both M-stable and regular models. Similar modularity properties for normal programs have been considered in [34, 33, 28] and, for disjunctive programs, in [7] and [11].

Let LP_{1} and LP_{2} be programs. We write LP_{2} ▷LP_{1} iff no predicate occurring in LP_{1} occurs in the head of any rule of LP_{2} [11]. Moreover, given an interpretation M for LP_{1}, we denote by LP_{2}^{M} the program

LP_{2} ∪ \{a ← | a ∈ M^{+}\} ∪ \{a ← ¬a | a ∈ \overline{M}\} ∪ \{a ← a | ¬a ∈ M^{−}\}

(note that both M^{+} and \overline{M} are subsets of B_{LP_{1}}). Intuitively, if LP_{2}▷LP_{1}, then every atom occurring in the head of a rule in LP_{2} has no influence on any atom from LP_{1}, and cannot be used for any derivation in LP_{1}. The rules added to LP_{2} in order to construct LP_{2}^{M} provide the interpretation M as input to LP_{2}, where P-stable (and regular) semantics assures that the value of the atoms from B_{LP_{1}} in a P-stable (resp. regular) model of LP_{2}^{M} coincides with its value in M. (In particular, the rules a ← a) serve to guarantee that atom a belongs to B_{LP}M_{2} , and is assigned false as in M.)

Example 12 Consider LP_{1} and LP_{2}:

\begin{aligned}LP_{1} : & d ∨ b ← & a \\ & a ← & ¬b \end{aligned}  \begin{aligned}LP_{2} : & e ← & d, ¬e \\ & f ← & d \end{aligned}

Here, LP_{2} ▷ LP_{1}. For M = {a, ¬b}, we have LP_{2}^{M} = LP_{2} ∪ { a ←, b ← b, d ← ¬d }.

The next proposition tells us that the regular models of a program LP, which consists of a normal program LP_{2} on top of an arbitrary disjunctive program LP_{1} can be built bottom up, i.e., by first building the regular models of LP_{1} and then by extending each such model M, considered like input data, to regular models of LP by computing the regular models of LP_{2}^{M}. This yields all and only the regular models for LP. A similar result has been reported in [11] for T-stable models.

Proposition 10 Let LP_{1} and LP_{2} be programs such that LP_{2} is a normal program and LP_{2} ▷ LP_{1}. Let LP = LP_{1} ∪ LP_{2}. Then,

1. for each M ∈ RS_{LP}, M ∩ Lit_{LP_{1}} ∈ RS_{LP_{1}}.

2. RS_{LP} = ∪_{M_{1}∈RS_{LP_{1}}} RS_{LP}{M_{1} \atop 2} .

This property is somewhat surprising. It is intuitive that the regular models of LP = LP_{1}∪LP_{2} must be obtained by extending founded models M_{1} of LP_{1} to regular models of LP_{2}; however, due the principle of minimal undefinedness, which endows in maximization of founded models, it seems that one loses regular models by extending only regular, i.e. maximal founded models M_{1} of LP_{1} to regular models of LP_{2}.

Before providing the formal proof of Proposition 10, we demonstrate the proposition on the previous example.

Example 13 Let LP = LP_{1} ∪ LP_{2}, where LP_{1} and LP_{2} are the programs reported in Example 12. The regular models of LP are: M_{1} = {¬b, a, d, f} and M_{2} = {¬d, ¬f, ¬e}. The hypotheses of Proposition 10 are verified, as LP_{2} is normal and LP_{2} ▷ LP_{1}. Indeed, according with Proposition 10.1, both M′_{1} = M_{1} ∩ Lit_{LP_{1}} = {¬b, a, d} and M′_{2} = M_{2} ∩ Lit_{LP_{1}} = {¬d} are regular models for LP_{1}. Moreover, M′_{1} and M′_{2} are the only regular models for LP_{1}, and, according with Proposition 10.2, we have that RS_{LP} = RS_{LP}{M′_{1} \atop 2} ∪

RS_{LP}{M′_{2} \atop 2} . Indeed, M_{1} is the only regular model of LP_{2}^{M′_{1}} = LP_{2} ∪ \{a ← , d ←, b ← b\},

and M_{2} is the only regular model of LP_{2}^{M′_{2}} = LP_{2} ∪ {a ← ¬a, b ← ¬b, d ← d}.

We next provide the formal proof of the statement.

Proof. (of Proposition 10) part 1. Let M_{1} = M ∩ Lit_{LP_{1}}. We have to show that M_{1} is a regular model of LP_{1}, i.e., (i) M_{1} is a founded model of LP_{1}, and (ii) no founded model N_{1} of LP_{1} exists such that N_{1} ⊃ M_{1}.

(i) M_{1} is a founded model. M_{1} is a 3-valued model for LP_{1}, as ground(LP_{1}) ⊆ ground(LP) and a rule in ground(LP_{1}) is satisfied w.r.t. M_{1} iff it is satisfied w.r.t. M (since no literal appearing in ground(LP_{1}) occurs in M − M_{1}). By deriving a contradiction, we show that M_{1} is founded. Assume that M_{1} is not founded for LP_{1}. Hence, there exists a total model M_{2} of LP_{1}(M_{1}) such M_{2}^{+} ⊂ M_{1}^{+}. Since no literal appearing in ground(LP_{1}) occurs in M − M_{1}, LP(M) = LP_{1}(M_{1}) ˙∪ LP_{2}(M), where ˙∪ denotes disjoint union. Therefore, the total interpretation N of LP(M) such that N^{+} = M_{2}^{+} ∪ (M^{+} − M_{1}^{+}) is a model of LP(M) (notice that this program is positive). However, N^{+} ⊂ M^{+}, and hence no M′ ∈ MM(LP(M)) exists such that M^{′+} = M^{+}; this implies that M is not a founded model of LP, and we reached a contradiction. Consequently, M_{1} is a founded model of LP_{1}. (ii) ∄N_{1} ⊃ M_{1} s.t. N_{1} is a founded model for LP_{1}. We proceed by contradiction. Let N_{1} be a founded model for LP_{1} such that N_{1} ⊃ M_{1}. We demonstrate that this implies the existence of a founded model N of LP such that N ⊃ M, contradicting the fact that M is a regular model of LP.

Let M_{2} be the (unique) minimal (total) model of the program LP_{0} = LP_{2}^{N_{1}}(M ∪ N_{1}), and choose N = M ∪ N_{1} ∪ M_{2}^{+}. Observe that LP_{0} is a positive normal program, which coincides with LP_{2}^{N_{1}}(N).

Clearly, N ⊃ M (notice that N_{1} − M ≠ ∅). Moreover, since N_{1} is a founded model of LP_{1} and LP_{2} ▷ LP_{1}, in order to show that N is a founded model of LP it suffices to show that N is a founded interpretation of LP_{0} and that N is a model of LP.

First, we show that N is an interpretation of LP, i.e., a consistent set of ground literals from B_{LP}. It is easy to see that M ∪ N_{1} is consistent, since M ∩ Lit_{LP_{1}} = M_{1} ⊂ N_{1}. Thus, to prove the consistency of N, it suffices to show the following:

Claim: No atom a from M_{2}^{+} is false in M ∪ N_{1}.

The claim is proven by induction on the derivation of a from LP_{0} using the immediate consequence operator T_{LP_{0}}(·). (Recall that M_{2}^{+} = T_{LP_{0}}^{∞}.) Assume that a is obtained in the i-th step.

(Base) i = 1: Hence, the rule a ← is in ground(LP_{0}). If a ∈ B_{LP_{1}}, then a ∈ N_{1} and hence a is not false in M ∪ N_{1}. Thus, assume that a ∉ B_{LP_{1}}. This implies that there exists some rule r in ground(LP_{2}) where H(r) = a, B^{+}(r) = ∅, and B^{−}(r) is true w.r.t M ∪ N_{1}. Consequently, each literal ¬b ∈ B^{−}(r) has in M either value true or undefined. Since M is a model of LP_{2}, it follows that a is not false in M. Thus, a is not false in M ∪ N_{1}.

(Induction) i > 1: a is derived from a rule H(r) ← B^{+}(r) in ground(LP_{0}), for some rule r from ground(LP_{2}) where H(r) = a, B^{+}(r) ≠ ∅ and B^{−}(r) is true in M ∪ N_{1}. From the inductive hypothesis, we have that no atom in B^{+}(r) is false in M ∪ N_{1}. Thus, it follows that B(r) is not false in M. Since M is a model of LP_{2}, it follows that a is not false in M. This proves the claim.

Thus, we have shown that N is an interpretation of LP. We next check that N is founded w.r.t. LP_{0}, i.e., N^{+} = A^{+} for some A ∈ MM(LP_{0}(N)).

We have that

LP(N) = LP_{1}(N) ˙∪LP_{2}(N) = LP_{1}(N_{1}) ˙∪LP_{2}(N).

Since N_{1} is a founded model of LP_{1}, N_{1}^{+} = L_{1}^{+} for some L_{1} ∈ MM(LP_{1}(N_{1})). From the definition of LP_{0}, it follows that M_{2} ∩ B_{LP_{1}} = N_{1}^{+}, and since M_{2} is the (unique) minimal model of LP_{0}, it follows that M_{2}^{+} = L_{2}^{+} for some L ∈ MM(LP(N)) = MM(LP_{1}(N_{1}) ˙∪LP_{2}(N)). It holds that M_{2}^{+} ⊇ M^{+} ∪ N_{1}^{+}: Clearly, from the construction of LP_{0} and LP_{0} = LP_{2}^{N_{1}}(N), we have N_{1}^{+} ⊆ M_{2}^{+}. On the other hand, since M is a founded model of LP and LP_{2} ▷ LP_{1}, the normal positive program LP_{3} = LP_{2}(M)∪ {a ← | a ∈ M_{1}^{+}} has a unique total minimal model M′, which satisfies M^{′+} = M^{+}. Since LP_{3} ⊆ LP_{0} and LP_{0} is normal (and positive), it follows M^{+} = M^{′+} ⊆ M_{2}^{+}. Thus, we have M_{2}^{+} ⊇ M^{+} ∪ N_{1}^{+}. This means N^{+} = M^{+} ∪ N_{1}^{+} ∪ M_{2}^{+} = M_{2}^{+}. This proves that N is founded w.r.t. LP_{0}.

It thus remains to show that N is a 3-valued model of LP. Clearly, N satisfies each rule in ground(LP_{1}). Consider now any rule r from ground(LP_{2}). We show that r is satisfied by N, by checking that r cannot be violated. For that, we need to check the cases where (1) H(r) is false in N, or (2) H(r) is undefined in N.

(1) If H(r) is false in N, then H(r) is false also in M. Since M satisfies r, B(r) is false in M. Thus, it follows that B(r) is also false in N as N ⊇ M. (2) If H(r) is undefined in N, then B(r) is not true in N. To show this, by contradiction suppose that B(r) is true in N. Then, B^{−}(r) is true in M ∪ N_{1}, and hence H(r) ← B^{+}(r) belongs to ground(LP_{0}). Since B^{+}(r) is true in N and, as shown already above, N^{+} = M_{2}^{+}, it follows that B^{+}(r) is true in M_{2}, and thus H(r) is true in M_{2}. By definition of N, it thus follows that H(r) is true in N. Thus we arrived at a contradiction.

We thus have that N is a model of LP. Now the founded model N of LP raises a contradiction to the fact that M is a regular model of LP. This concludes the proof of part 1.

part 2. (⊆) Let M ∈ RS_{LP}. Then, by part 1, M_{1} = M ∩Lit_{LP_{1}} is a regular model of LP_{1}. Suppose M is not a regular model of LP_{2}^{M_{1}}. Clearly, M is a founded model of LP_{2}^{M_{1}}. Hence, there exists a founded model N of LP_{2}^{M_{1}} such that N ⊃ M. From the definition of LP_{2}^{M_{1}} and the regularity of M_{1}, it follows that N is a founded model of LP. Thus, M is not a regular model of LP; we reached a contradiction. This proves the “⊆” inclusion. (⊇) Let N be a regular model of LP_{2}^{M_{1}} for some regular model M_{1} of LP_{1}. Suppose that N is not a regular model of LP. Then, it follows that there exists a founded model N′ of LP such that N′ ⊃ N. In particular, N′ ∩ Lit_{LP_{1}} = M_{1}, and as easy to check, N′ is a founded model of LP_{2}^{M_{1}}. This means that N is not a regular model of LP_{2}^{M}, however, and we thus reached a contradiction. This proves the “⊇” inclusion and completes the proof of the proposition.

The restriction of LP_{2} in Proposition 10 to normal programs is essential. If we allow disjunctive rules in LP_{2}, then the proposition fails. This is shown by the following example.

\begin{aligned}LP_{1} : & b ← & ¬a \\ & a ← & ¬b \end{aligned}  \begin{aligned}LP_{2} : & d ∨ e ← & c \\ & c ← & b \\ & c ← & a \end{aligned}

Clearly LP_{2} ▷LP_{1}. The interpretation M = {¬d} is a regular model of LP = LP_{1} ∪LP_{2}. However, M ∩ Lit_{LP_{1}} = ∅ is not a regular model of LP_{1}. In fact, the regular models of LP_{1} are M_{1} = {a, ¬b} and M_{2} = {¬a, b}.

For arbitrary LP_{2}, the following weaker form of Proposition 10 holds; we leave the proof, which can be extracted from the proof of Proposition 10, to the reader. (Recall that FS_{LP} denotes the founded models for LP.)

Proposition 11 Let LP_{1} and LP_{2} be programs such that LP_{2} ▷ LP_{1}. Let LP = LP_{1} ∪ LP_{2}. Then,

1. for each M ∈ RS_{LP}, M ∩ Lit_{LP_{1}} ∈ FS_{LP_{1}}.

2. RS_{LP} = max_{⊆} (∪_{M_{1}∈FS_{LP_{1}}} RS_{LP}{M_{1} \atop 2} ).

Here max_{⊆} denotes the maximal sets w.r.t. inclusion.

With a similar proof, we can derive that the modularity property for regular models holds for M-stable models as well.

Proposition 12 Let LP_{1} and LP_{2} be programs such that LP_{2} is a normal program and LP_{2} ▷ LP_{1}. Let LP = LP_{1} ∪ LP_{2}. Then,

1. for each M ∈ MS_{LP}, M ∩ Lit_{LP_{1}} ∈ MS_{LP_{1}}.

2. MS_{LP} = ∪_{M_{1}∈MS_{LP_{1}}} MS_{LP}{M_{1} \atop 2} .

Proof. (Outline) The proof is similar to the proof of Proposition 10. For part 1, one shows that M_{1} = M ∩ Lit_{LP_{1}} is a P-stable model of LP_{1}, and then shows by deriving a contradiction that no larger P-stable model N_{1} ⊃ M_{1} exists. Along the lines of the proof of Proposition 10, one constructs the founded model N ⊃ M of LP. Clearly, N is a founded model of LP_{2}^{N_{1}}. Thus, a regular model N′ ⊇ N of LP_{2}^{N_{1}} exists; notice that N′ ∩ Lit_{LP_{1}} = N_{1}. Since LP_{2}^{N_{1}} is a normal program, N′ is an M-stable model of LP_{2}^{N_{1}} by Proposition 9. Thus, as easily checked, N′ is a P-stable model of LP. N contradicts the fact that M is an M-stable model of LP; this proves part 1. Part 2 is shown analogous as in Proposition 10.

Analogously, the weak form of modularity in Proposition 11, with RS and FS replaced by MS and PS, respectively, holds for M-stable models.

We remark that for P-stable models, we obtain a stronger result on modularity than the one for M-stable models. In fact, the P-stable models of LP = LP_{2} ∪ LP_{1} with LP_{2} ▷ LP_{1} are obtained by extending all P-stable models of LP_{1} to P-stable models of LP_{2}.

Proposition 13 Let LP_{1} and LP_{2} be programs such that LP_{2} ▷ LP_{1}. Let LP = LP_{1} ∪ LP_{2}. Then,

1. for each M ∈ PS_{LP}, M ∩ Lit_{LP_{1}} ∈ PS_{LP_{1}}.

2. PS_{LP} = ∪_{M_{1}∈PS_{LP_{1}}} PS_{LP}{M_{1} \atop 2} .

Proof. Omitted.

As an immediate corollary of Proposition 13, we obtain that the same holds for Tstable models; the latter was reported in [11].

It is worth noting that Proposition 10 fails for L-stable models in place of regular models. This is not surprising, since a P-stable model might not be extendible to an L-stable model by adding literals. Consider the following example.

\begin{aligned}LP_{1} : & b ← & ¬a \\ & a ← & ¬b \\ & c ← & a, ¬c \end{aligned}  \begin{aligned}LP_{2} : & d ← & a \\ & d ← & ¬a, ¬d \end{aligned}

Here, the P-stable models of LP_{1} are ∅, {a, ¬b}, and {¬a, b, ¬c}; the last one of them is L-stable. The P-stable models of LP = LP_{1} ∪ LP_{2} are M_{1} = ∅, M_{2} = {a, ¬b, d}, and M_{3} = {¬a, b, ¬c}, from which the latter two are L-stable. Now {a, ¬b, d} ∩ Lit_{LP_{1}} = {a, ¬b} is not an L-stable model of LP_{1}. Thus, the condition 1.) fails. Moreover, M_{2} is an L-stable model of LP, but M_{2} is not an L-stable model of LP_{2}^{{¬a,b,¬c}}; this shows that also condition 2.) fails.

However, for L-stable models we have weaker properties, similar to the the properties of M-stable models for general LP_{1} and LP_{2}. The L-stable models of LP = LP_{1} ∪ LP_{2} such that LP_{2} ▷ LP_{1} are obtained by the least undefined models in the collection of all P-stable models of LP_{2}^{M_{1}}, where M_{1} is a P-stable of LP_{1}. Notice that if LP_{1} is stratified, then each L-stable model of LP is total on LP_{1}.

6.1 Application of Modularity

The modularity property of M-stable and regular models has interesting applications. First, it allows to identify an extended class of programs on which regular and M-stable semantics coincide. Second, an interesting consequence of practical relevance is that Mstable models of normal programs can be computed bottom-up in a process similar to the computation of the stratified model [2] of normal programs.

The modularity property of regular and M-stable models allows us to greatly extend the class of programs on which regular and M-stable models coincide. In particular, it extends the class of normal programs and the class of stratified (disjunctive) programs. This is an immediate corollary of the following theorem.

Theorem 3 Let LP be a program such that LP = LP_{1} ∪ LP_{2} and LP_{2} ▷ LP_{1}, where LP_{2} is a normal program. If RS_{LP_{1}} = MS_{LP_{1}}, then RS_{LP} = MS_{LP}.

Proof. By Proposition 10, each regular model M of LP is a regular model of LP_{2}^{M_{1}}, where M_{1} is some regular model of LP_{1}. Since LP_{2}^{M_{1}} is a normal program, its regular models coincide with its M-stable models by Proposition 9. By hypothesis, the regular models of LP_{1} coincide with the M-stable models of LP_{1}. Thus, by Proposition 12, M is an M-stable model of LP. The proof of the converse (each M-stable model of LP is a regular model) is analogous.

Corollary 2 Let LP be a program such that LP = LP_{1} ∪ LP_{2} and LP_{2} ▷ LP_{1}, where LP_{1} is (locally) stratified and LP_{2} is a normal program. Then, RS_{LP} = MS_{LP}.

Another important application of the modularity property concerns model computation. Importantly, a bottom up computation of the M-stable semantics of a normal program is possible. Every normal program LP may be broken up into its strongly connected components [34, 28] (denoted here by SCC(LP)), which are partially ordered by the dependency relation. Informally, the strongly connected components are the smallest subsets C of the rules, such that for each predicate p that occurs in the head of some rule in C, every rule that contains a predicate mutually recursive with p also belongs to C; they describe the finest-grained syntactical decomposition of the program P into hierarchically organized modules.

More formally, mutual recursiveness is as follows. Say that a predicate p depends on a predicate q if they are the same, or if there is a sequence of rules r_{0}, …, r_{k} such that p occurs in H(r_{1}), q occurs in B(r), and the predicate of H(r_{i}) occurs in B(r_{i−1}), for each i = 1, …, k. Then, predicates p and q are mutually recursive iff p depends on q and q depends on p. Notice that SCC(LP) can be computed efficiently from LP.

The dependency relation ≺ on the strongly connected components is given by the transitive closure of the natural relation ⊏ associated with them given by C ⊏ C′ iff C and C′ are different and some predicate p that occurs in the head of a rule of C occurs in the body of some rule of C′. Notice that the transitive and reflexive closure ⪯ of ⊏ is a partial order. The following proposition is easily verified from the definitions.

Proposition 14 Let LP be a normal program, and let C, C′ ∈ SCC(LP). If C ≺ C′, then C ▷ C′.

Consequently, by applying Proposition 12, we easily obtain the following result. For each subset C ⊆ SCC(LP), denote by LP_{≺C} the union of all strongly connected components of LP on which any C ∈ C depends, and by LP_{⪯C} the union of LP_{≺C} and all strongly connected components in C. If C contains a single component C, we write LP_{≺C} and LP_{⪯C} instead of LP_{≺{C}} and LP_{⪯{C}}, respectively.

Theorem 4 Let LP be a normal program and let C ⊆ SCC(LP) whose programs are mutually independent (i.e., no C ∈ C depends on any C′ ∈ C). Suppose that max_{≺}(C) = {C_{1}, …, C_{k}}. Then,

MS_{LP_{⪯C}} = ∪_{M∈MS_{LP_{≺C}}} MS_{(∪_{i=1}^{k}C_{i})^{M}}
= ∪_{M∈MS_{LP_{≺C}}} { M_{1} ∪ M_{2} ∪ ⋯ ∪ M_{k} | M_{i} ∈ MS_{C_{i}^{M}} , i = 1, …, k}.

In particular, if C = { C }, then MS_{LP_{⪯C}} = ∪_{M∈MS_{LP_{≺C}}} MS_{C^{M}} , and if C = SCC(LP), then

MS_{LP_{⪯C}} = MS_{LP} = ∪_{M∈MS_{LP−(C_{1}∪···∪C_{k})}}{ M_{1}∪M_{2}∪⋯∪M_{k} | M_{i} ∈ MS_{C_{i}^{M}} , i = 1, …, k}.

Proof. By Propositions 12 and 14, the equivalence of the first right hand side with the left hand side of the equation is immediate. The second right hand side is equivalent to the first, since each predicate is defined by one and only one strongly connected component. (Notice also that each predicate occuring in the body of a rule in C_{i} must be defined in LP_{⪯C_{i}}, i.e. in C_{i} or in a SCC on which C_{i} depends.)

Theorem 4 allows a bottom-up computation of the M-stable models of a program. First split the program LP into its strongly connected components SCC(LP). Then, take a linear ordering C_{1}, ⋯, C_{k} of the components of SCC(LP) compatible with the dependency relation ≺ of SCC(LP) (such an ordering always exists), and compute the M-stable models of LP bottom-up from C_{1} to C_{k}. In particular, the M-stable models of C_{1} are computed first; then at the i-th step of the computation, the M-stable models of C_{1} ∪ ⋯ ∪ C_{i} are computed by focusing on the rules of C_{i} only, using the previously computed M-stable models as input data. Notice that, by following the partial order ⪯ rather than a linearization of it, part of the bottom up evaluation of the strongly connected components can also be done in parallel; thus, performance increase by parallel processing is possible.

Modularized bottom up computation is important for practical concerns, as we experienced in some projects on the implementation of deductive databases systems, namely COMPLEX [14] and the ESPRIT projects KIWI [19] and KIWIS [21, 1]. Indeed, in the context of deductive databases, where a large amount of data is assumed, it is very important to reduce the number of relations to be dealt with at a time. Theorem 4 allows to minimize this number of relations, permitting a bottom-up computation on the strongly connected components of the program, which greatly reduces the amount of data needed in main-memory during the computation.

On the other hand, designing programs in a modular fashion is natural. M-stable semantics supports this feature, while L-stable semantics does not. This suggests that from the semantical side, M-stable models are besides L-stable an appealing approximation of T-stable models.

7 Conclusion

In this paper, we have extended the notion of unfounded set from normal programs to disjunctive programs. By using unfounded set, we presented the notion of P-stable model for acceptable partial models for a disjunctive program. These models satisfy two principles: First, the condition of foundedness (also called justifiability [38]), and second, the principle of CWA, extended in a natural way from normal programs to disjunctive programs.

We showed that P-stable models coincide with the 3-valued stable models of Przymusinski [26]. Hence, the definition of P-stable model, which does not resort to 3-valued logic, can be seen as a characterization of 3-valued stable models in terms of classical interpretations and unfounded sets.

We next investigated refinements of P-stable models under the principle of minimal undefinedness, which has been considered in the context of normal programs [37, 29] and, for disjunctive programs, in [38]. We have proposed and analyzed maximal P-stable (M-stable) models and the more restrictive concept of least undefined P-stable (L-stable) models, which had been investigated in the course of normal programs in [32, 31].

It appeared that M-stable models are similar in spirit to the regular models in [38]. However, while regular models respect the principles of foundedness and minimal undefinedness, they do not obey to the CWA.

We have shown, however, that on a large class of programs, extending previous results, M-stable models and regular models coincide. The modularity property used for deriving this result is interesting in its own right. In particular, we obtained as a result that the M-stable models of a normal program LP can be computed bottom-up. This property is important for practical concerns. L-stable models lack this property. Thus, while Lstable models are stricter approximations of T-stable models (and thus preferable from the semantical side), M-stable models can be more amenable from the computational and methodological point of view.

The following problems are left open here. First computational aspects; in particular, expressibility and complexity of the various semantics. This issue is dealt with in a companion paper [10].

Apart from this, the design of algorithms for efficient query evaluation under M-stable and L-stable semantics is another interesting issue. Finally, further aspects on the side of knowledge representation would merit investigation, as well as fixpoint operators for computing M-stable and L-stable models (like the alternating fixpoint operator for the well-founded model [4, 35]).

Acknowledgement Work partially supported by the EC-US033 project “DEUS EX MACHINA: Non-Determinism in Deductive Databases” and by a MURST grant (40% share) under the project “Sistemi formali e strumenti per basi di dati evolute.”

References

[1] Ahlsen, et al.. The KIWIS Knowledge Base Management System. Proc. third Int. Conf. CAiSE’91, Trondheim, Norway, May 1991.

[2] K.R. Apt, H. Blair, A. Walker. Towards a Theory of Declarative Knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pp. 89–148. Morgan Kaufman, Washington DC, 1988.

[3] V. Baral and V.S. Subrahmanian. Stable and extension class theory for logic programs and default logic. Journal of Automated Reasoning, 1992, pp. 345–366.

[4] C. Baral and V.S. Subrahmanian. Dualities Between Alternative Semantics for Logic Programming and Non-Monotonic Reasoning, Journal of Automated Reasoning, 10, 1993, pp. 399–420.

[5] S. Ceri and G. Gottlob and L. Tanca. Logical Programming and Databases. Springer-Verlag, 1990.

[6] J. Dix. Semantics of Logic Programs: Their Intuition and Formal Properties. An Overview. In A. Fuhrmann and H. Rott (eds.) Logic Actions and Information. Proceedings of the Konstanz Colloquium in Logic and Information, deGruyter, Berlin, 1993.

[7] J. Dix. Classifying Semantics of Disjunctive Logic Programs. In Proceedings ICLP-94, 1994, pp. 798–812.

[8] J. Doyle. A Truth Maintenance System. Artificial Intelligence, 12, 1979, pp. 231–272.

[9] P. Dung. Negation as Hypotheses: an abductive foundation for logic programming. Proc. 8th Conf. on Logic Programming, 1991, pp. 3–17.

[10] T. Eiter, N. Leone, D. Saccà. Expressive Power and Complexity of Partial Semantics for Disjunctive Deductive Databases. In preparation.

[11] T. Eiter, G. Gottlob and H. Mannila. Adding Disjunction to Datalog. Proceedings ACM PODS-94 , May 1994, pp. 267–278.

[12] T. Eiter and G. Gottlob. On the Computational Cost of Disjunctive Logic Programming: Propositional Case. Annals of Mathematics and Artificial Intelligence, 1995 (to appear).

[13] G. Gottlob, N. Leone, H. Veith. Second Order Logic and the Weak Exponential Hierarchies. Proc. MFCS’95, Prague, October, 1995 (to appear).

[14] S. Greco, N. Leone, P. Rullo. COMPLEX: An Object-Oriented Logic Programming System. IEEE TKDE, vol. 4, no. 4, August 1992.

[15] M. Fitting. A Kripke-Kleene Semantics for Logic Programs. Journal of Logic Programming, 2(4), pp. 295–312, 1985.

[16] M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In Proceedings Fifth Logic Programming Symposium, pp. 1070–1080, Cambridge Mass., 1988. MIT Press.

[17] A. Kakas, P. Mancarella. Preferred Extensions are Partial Stable Models. Journal of Logic Programming, 14, pp. 341-348, 1992.

[18] J.A. Fernández and J. Minker. Semantics of Disjunctive Deductive Databases. Proceedings 4th Intl. Conference on Database Theory (ICDT-92), pp. 21–50, Berlin, October, 1992.

[19] KIWI Team. A System for Managing Data and Knowledge Bases. ESPRIT Project 1117, in Proc. of the ESPRIT Technical Week, North-Holland eds., 1988.

[20] N. Leone, P. Rullo, F. Scarcello. Unfounded Sets, Fixpoint Semantics, and Computation of Disjunctive Stable Models. Technical Report ISI-CNR, TR 95/1, 1995.

[21] N. Leone, P. Rullo, A. Mecchia, G. Rossi. A Deductive Environment for Dealing with Objects and Non-Monotonic Reasoning. CRAI Tech. Report RI 94-06, Rende, Italy, 1994.

[22] J. Lobo, J. Minker, and A. Rajasekar. Foundations of disjunctive logic programming. The MIT Press, 1992.

[23] J. Minker. On Indefinite Data Bases and the Closed World Assumption. In Proceedings of the 6^{th} Conference on Automated Deduction (CADE-82), pp. 292–308, 1982.

[24] J. Minker. Overview of Disjunctive Logic Programming. Annals of Mathematics and Artificial Intelligence, 12, pp.1–24, 1994.

[25] T. Przymusinski. On the Declarative and Procedural Semantics of Stratified Deductive Databases. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pp. 193–216. Morgan Kaufman, Washington DC, 1988.

[26] T. Przymusinski. Stable Semantics for Disjunctive Programs. New Generation Computing, 9:401–424, 1991.

[27] R. Reiter. On Closed-World Data Bases. In Logic and Data Bases, H. Gallaire, J. Minker (eds.), Plenum Press, New York, 1978, pp. 55-76.

[28] K. Ross. Modular Stratification and Magic Sets for Datalog Programs with Negation. Journal of the ACM, 41(6):1216–1267, 1994.

[29] D. Saccà, C. Zaniolo. Stable Models and Nondeterminism in Logic Programs with Negation Proc. ACM Symposium on Principles of Database Systems 1990.

[30] D. Saccà, C. Zaniolo. Partial Models and Three-Valued Models in Logic Programs with Negation. Proc. 1st Int. Conf. on Logic Programs and Non-monotonic Reasoning, MIT Press, 1991, pp. 87–104.

[31] D. Saccà. The Expressive Powers of Stable Models for Bound and Unbound Queries. submitted for publication, 1994, (extended abstract in Proc. 1993 Workshop on ”Structural Complexity and Recursion-Theoretic Methods in Logic Programming.

[32] D. Saccà. Deterministic and Non-Deterministic Stable Model Semantics for Unbound DAT-ALOG Queries. In Proc. ICDT 95, Prague, January, 1995.

[33] J.S. Schlipf. The Expressive Powers of the Logic Programming Semantics. Proc. ACM PODS Symp., 1990, pp. 196-204. Full paper to appear in Journal of Computer and System Sceinces.

[34] J.D. Ullman. Principles of Database and Knowledge-Base Systems, Vol. 1 and 2, Computer Science Press, Rockville, Md., 1989.

[35] A. Van Gelder. The Alternating Fixpoint of Logic Programs With Negation. In Proceedings PODS-89, pages 1–10, 1989.

[36] A. Van Gelder, K. Ross, and J. Schlipf. The well-founded semantics for general logic programs. Journal of ACM, 38(3):620–650, 1991.

[37] J. You and L.Y. Yuan. Three-valued Formalization of Logic Programming: is it needed?. Proc. of ACM PODS Symp., 1990, pp. 172-182.

[38] J. You and L.Y. Yuan. A Three-valued Semantics for Deductive Databases and Logic Programs. Journal of Computer and System Sciences, 49, 334-361, 1994.

[39] J. You and L.Y. Yuan. On the Equivalence of Semantics for Normal Logic Programs. Journal of Logic Programming, pp. 211-222, 1995.