# Extending Well-Founded Semantics with Clark’s Completion for Disjunctive Logic Programs

Authors: Juan Carlos Nieves; Mauricio Osorio
Journal: Scientific Programming
 (2018)

---

## Abstract

In this paper, we introduce new semantics (that we call D3-WFS-DCOMP) and compare it with the stable semantics (STABLE). For normal programs, this semantics is based onsuitable integration of the well-founded semantics (WFS) and the Clark’s completion. D3-WFS-DCOM has the following appealing properties: First, it agrees with STABLE in the sense that it never defines a nonminimal model or a nonminimal supported model. Second, for normal programs it extends WFS. Third, every stable model of a disjunctive program P is a D3-WFS-DCOM model of P. Fourth, it is constructed using transformation rules accepted by STABLE. We also introduce second semantics that we call D2-WFS-DCOMP. We show that D2-WFS-DCOMP is equivalent to D3-WFS-DCOMP for normal programs but this is not the case for disjunctive programs. We also introduce third new semantics that supports the use of implicit disjunctions. We illustrate how these semantics can be extended to programs including explicit negation, default negation in the head of a clause, and a lub operator, which is a generalization of the aggregation operatorsetof over arbitrary complete lattices.


---

## Body

## 1. Introduction

One of the most well-known semantics for logic programming is the stable semantics (STABLE) [1, 2]. However, it is well known that very often STABLE is too strong, namely, that there are programs that do not possess stable models [3–5]. Let us consider the following example.Example 1.
LetP be a disjunctive logic program:d∨e←¬a.c←c.b←a.a←b.a←¬b,¬c.
In this program there are not stable models; however if we use our D3-WFS-DCOMP semantics there is a model of the programP, that is, {a,b}. We can argue that this intended model makes sense as follows: since a tautology such as c←c should not matter (in our point of view, what makes the given tautology to be specially harmless is that c does not occur in the head of any other clause), we can delete it getting a semantically equivalent program that we call P1. Then, since c does not appear in the head of any clause of P1, we can derive ¬c and so we can delete ¬c in the last clause to get a semantically equivalent program P3. (Note that what we have done so far in this example is accepted by the STABLE semantics.) Then, since we have thata←ba←¬b
are clauses inP3 and by reasoning by cases, we derive a. (Reasoning by cases is not accepted in STABLE.) Then, we derive b by simple modus ponens. Finally, d and e can be considered false since a is true.It has been even argued that STABLE does not define the intended models of a program [6]. It is also possible that there is not best semantics [7]:“The fact each approach to semantics of negation has its own strength and weakness suggests that there is probably not abest semantics for logic programs.”Nevertheless, STABLE satisfies interesting logic properties as it is shown in [1, 8]. In this paper we study the stable semantics and exhibit some properties that it satisfies. Also we point out some problems with this semantics. With this base, we study some variations to the semantics proposed by [9, 10]. The obtained semantics, that we call D3-WFS-DCOMP, satisfies the following main properties: First, it agrees with STABLE in the sense that it never defines a nonminimal model or a nonminimal supported model. Second, for normal programs it extends the well-founded semantics (WFS) [11]. Third, every stable model of a disjunctive program P is a D3-WFS-DCOM model of P. Fourth, it is constructed using logic program transformations accepted by STABLE.We also introduce two more logic programming semantics and prove some properties of them. Moreover, we show that our three proposed semantics are equivalent within the class of normal programs. In the last part of our paper, we highlight that the introduced logic programming semantics are suitable for modeling thesetof operator of PROLOG using negation as failure.The rest of the paper is structured as follows: In Section2, basic definitions on logic programming are presented. In Section 3, we prove some properties of stable model semantics and define our new semantics. In Section 4, we introduce an approach for modeling thesetof operator of PROLOG with our semantics using negation as failure; moreover, we present how to reduce programs with explicit negation to programs without it. Finally, in Section 5, we outline our conclusions and future work.


## 2. Background

In order to have a self-contained document, basic concepts on logic programming are introduced in this section. This section does not aim to be a tutorial. The interested reader can see [1] for a deep presentation of the concepts introduced in this section.A signatureL is a finite set of elements that we call atoms. A literal is an atom or the negation of an atom a that we denote as ¬a. Given a set of atoms {a1,…,an}, we write ¬{a1,…,an} to denote the set {¬a1,…,¬an}.A logic theory is built up using the logical constants∧,∨,→, and ¬. We may denote a (general) clause C as (1)a1∨⋯∨am⟵l1,…,ln,where l1,…,ln represents the formula l1∧⋯∧ln,m>0,n≥0, each ai is a propositional atom, and each li is a propositional literal. When n=0 the clause is considered as a1∨⋯∨am←true  (or the simple formula a1∨⋯∨am.), where true is a constant atom with its intended interpretation.Sometimes, a clauseC is denoted by A←B+,¬B-, where A contains all the head atoms, B+ contains all the positive body atoms, and B- contains all the negative body atoms. We also use body(C) to denote B+∪¬B-. When A is a singleton-set, the clause reduces to a normal clause. A definite clause ([12]) is a normal clause lacking of negative literals; that is, B-=∅. Apure disjunction is a disjunction consisting solely of positive or solely of negative literals. A (general) program is a finite set of clauses. We use HEAD(P) to denote the set of atoms occurring in the heads of the clauses of P. Given a signature L, we write ProgL to denote the set of all programs defined over L.We use⊨ to denote the consequence relation for classical first-order logic. We will also consider interpretations and models as usual in classical logic.Given two theoriesT1, T2 we denote T1≡IT2 to say that these theories are intuitionistically equivalent; that is, ∀α∈T2, then T1 proves (using intuitionistic logic) α and vice versa [13].It will be useful to map a program into a normal program. Given a clause(2)C≔A⟵B+,¬B-we write dis-nor(C) to denote the set of normal clauses: (3)a⟵B+,¬B-∪A∖a∣a∈A.We extend this definition to programs as follows. IfP is a program, let dis-nor(P) denote the normal program: ⋃C∈Pdis-nor(C). Given a normal program P, we write Definite(P) to denote the definite program that we obtain from P just by removing every negative literal in P. Given a definite program, by MM(P) we mean the unique minimal model of P (that always exists for definite programs, see [12]). We assume working with disjunctive programs, unless otherwise stated.We use an example to illustrate the above definitions. LetP be the program:p∨q←¬r.p←s,¬t.ThenHEAD(P)={p,q}, and dis-nor(P) consists of the clauses:p←¬r,¬q.q←¬r,¬p.p←s,¬t.D e f i n i t e ( dis-nor ( P ) ) consists of the clauses:p←true.q←true.p←s.M M ( D e f i n i t e ( dis-nor ( P ) ) ) = { p , q }.Since we are interested in disjunctive logic programs, the following question arise:What are the minimal requirements we want to impose on semantics for disjunctive programs?Certainly, we want that disjunctive facts, that is, clauses in the program with empty bodies, to be true. Dually, if an atom does not occur in any head, then its negation should be true. These ideas are straightforward generalizations of the case on normal programs. Following the ideas of [14], we propose the following definition.Definition 2 (semantics).
(i) Scenario semantics over a given signatureL is a function such that for every program P over L it associates a set of models.
(ii) The sceptical semantics induced by scenario semantics is the set of pure disjunctions true in every model of the scenario semantics. (The sceptical semantics derives every literal when its associated scenario semantics has no models.) For any programP we define(4)SEMminP≔a∣a⟵true∈P∪¬a∣a∈L,a∉HEADP.Given two theoriesP1, P2, we denote P1≡SEMP2 whenever the set of models of P1with respect to the scenario semantics SEM is equal to the set of models of P2with respect to the scenario semantics SEM.We introduce some well-accepted logic programming semantics from the state of the art. The first one is the logic programming semantics based on supported models.Definition 3 (supported model, [14]).
A two-valued modelI of a (disjunctive) logic program P is supported iff for every ground atom A with I⊨A there is a rule A←B+∧¬B- in P with A∈A, I⊨B+∧¬B-, and I⊭A∖{A}.Supported models are related to the so-called Clark’s completion [15]. In order to define the Clark’s completion of a logic program, let us introduce the following notation.Definition 4 (def, sup).
LetP be a normal program. Let a be an atom in a given signature L by the definition of a in P; we mean the set of clauses {a←body∈P} that we denote by def(a). We define(5)supa≔falseifdefa=∅body1∨⋯∨bodynotherwise,where def(a)={a←body1,…,a←bodyn}.Considering the previous notation, the Clark’s completionwith respect to a normal program is presented in the following definition. An extension of the Clark’s completion for capturing disjunctive logic programs is also presented in the following definition.Definition 5 (Clark’s completion:comp(P) ([15]), dcomp(P)).
(i) For any normal programP, we define comp(P) over a given signature L as the classical theory {a↔sup(a)∣a∈L}.
(ii) LetP be a disjunctive logic program. Let dcompP≔comp(dis-nor(P)).Let us observe that given a normal logic programP, comp(P)=dcomp(P). As was mentioned, there is a strong relation between supported models and the Clark’s completion. dcomp will play a key role in the definition of the logic programming semantics introduced in this paper. In particular, it will be used it for extending the well-founded semantics.Now the well-accepted STABLE semantics is presented.Definition 6 (stable, [2]).
The Gelfond-Lifschitz transformation (GL-transformation) of a logic programPwith respect to an interpretation M is obtained from P by deleting(i)
each rule that has a negative literal¬B in its body with B∈M,(ii)
all negative literals in the bodies of the remaining rules.
Clearly the programGL(P,M) resulting from applying the GL-transformation is negation-free, so GL(P,M) has at least one model. M is a stable model iff M is a minimal model of GL(P,M).It is worth mentioning that Pearce [8] generalized the stable semantics to any propositional theory based on intuitionistic logic. Pearce made the following statement [8]:“A formula is entailed by a program in the stable model semantics if and only if it belongs to every intuitionistically complete and consistent extension of the program formed by adding only negated atoms.”From this characterization of the stable semantics, the generalization of STABLE to arbitrary theories is immediate. From now on, we will assume this definition whenever we mention the stable semantics of some given theory.We introduce a set of transformation rules that will help to define different extension of the well-founded semantics. In particular, the following transformations are defined in [14] and generalize the corresponding definitions for normal programs.Definition 7 (basic transformation rules).
A transformation rule is a binary relation onProgL. The following transformation rules are called basic. Let a program P∈ProgL be given. RED+: replace a rule A←B+,¬B- by A←B+,¬(B-∩HEAD(P)).RED-: delete a clause A←B+,¬B- if there is a clause A′←true such that A′⊆B-.SUB: delete a clause A←B+,¬B- if there is another clause A1←B1+,¬B1- such that A1⊆A, B1+⊆B+, B1-⊆B-.The transformation rules introduced by Definition7 are illustrated in the following example:Example 8 (transformation).
LetL={a,b,c,d,e} and let P be the program:a∨b←c,¬c,¬d.a∨c←b.c∨d←¬e.b←¬c,¬d,¬e.
ThenHEAD(P)={a,b,c,d}, and SEMmin(P)={¬e}. We can apply RED+ to get the program P1:a∨b←c,¬c,¬d.a∨c←b.c∨d←true.b←¬c,¬d,¬e.
If we applyRED+ again, we get program P2:a∨b←c,¬c,¬d.a∨c←b.c∨d←true.b←¬c,¬d.
Now, we can apply SUB to get programP3:a∨c←b.c∨d←true.b←¬c,¬d.
A second set of transformations was defined by [14]. These transformations are as follows.
GPPE (Generalized Principle of Partial Evaluation). Suppose P contains A←B+,¬B- and we fix an occurrence of an atom g∈B+. Then we replace A←B+,¬B- by the n clauses (i=1,…,n)(6)A∪Ai∖g⟵B+∖g∪Bi+,¬B-∪¬Bi-, where Ai←Bi+,¬Bi-∈P (for i=1,…,n) are all clauses with g∈Ai. If no such clauses exist, we simply delete the former clause.
TAUT (Tautology). Suppose P contains a clause of the form: A←B+,¬B- and A∩B+≠∅, then we delete the given clause.LetCS1 be the rewriting system which contains, besides the basic transformation rules, the rules GPPE and TAUT. This system was introduced in [14] and is confluent and terminating as shown in [16]. We write resCS1(P) to denote the residual program of P with respect to the transformations rules CS1.ConsideringCS1, we define the following logic programming semantics.Definition 9 (D′-WFS).
Given a programP, we define (7)D′-WFSP=SEMminresCS1P.We note that our definition of D′-WFS(P) is very similar to the definition of the D-WFS semantics [17]. The difference is that D-WFS defines pure disjunctions while D′-WFS(P) defines literals. (The paper could be worked out without defining D′-WFS but using instead D-WFS.)Let us note that although theCS1 system has the nice property of confluence (and termination), its computational properties are not so efficient. In fact, computing the residual form of a program is exponential (even for normal programs, whereas it is known that the WFS ([11]) can be computed in quadratic time).In order to define a second rewriting system, two more transformation rules are introduced. The first one is Dloop which is defined as follows.Definition 10 (Dloop [9]).
For a programP1, let unf(P1)≔L∖MM(Definite(dis-nor(P1)). The transformation Dloop(dp) reduces a program P1 to P2≔{A←B+,¬B-∣B+∩unf(P1)=∅}. We assume that the given transformation takes place only if P1≠P2. We write P1→DloopAP2 to denote that P1 transforms to P2 by a dp transformation, where A≔unf(P1).The last transformation, which will be introduced, is Dsuc.Definition 11 (Dsuc [9]).
Suppose thatP is a program that includes a fact a←true and a clause A←Body such that a∈Body. Then we replace this clause by the clause A←Body∖{a}.Considering Dloop and Dsuc, the rewriting systemCS2 is introduced.Definition 12 (CS2 [9]).
LetCS2 be the rewriting system based on the transformations SUB, RED+, RED-, Dloop, and Dsuc.We can observe thatCS2 is confluent and terminating.Lemma 13 (confl. and termination ofCS2).
The systemCS2 is confluent and terminating.Proof.
(i)CS2 is terminating since all its transformation rules reduce the size of the given program. The reduction of the size of a given program is done by either the elimination of literals of the body of a clause or the elimination of clauses.
(ii) LetCS3=CS2∖{SUB}. Hence, CS3 is confluent in the class of normal logic programs [18]. (In [18], the rewriting system, which proved to be confluent, includes the so-called failure transformation rule. However, failure is redundant if the given rewriting system includes loop [4]. Loop is the version of Dloop for normal logic programs [4, 9].) Let us prove that CS3 is confluent in the class of disjunctive logic programs by contradiction. Let us suppose that CS3 is not confluent. Hence, there exists a disjunctive logic program P such that resCS3(P)=P1, resCS3(P)=P2, and P1≠P2. Hence, resCS3(dis-nor(P))=P3, resCS3(dis-norP)=P4 and P3≠P4, but this is a contradiction since CS3 is confluent in the class of normal logic programs. Now, we only need to see that CS2=CS3∪{SUB} is confluent. The only issue is to see the interaction between SUB and the transformation rules of CS3. Since SUB only removes clauses that are biggest in size than a given one that is kept by SUB at the given program, SUB does not affect the confluence of CS3. Hence, CS2 is confluent.It is known thatCS2 characterizes an extension of WFS, which captures the class of disjunctive logic programs. This extension of WFS considering CS2 is called D1-WFS and is defined as follows.Definition 14 (D1-WFS).
Given a programP, we define (8)D1-WFSP=SEMminresCS2P.The relationship between D1-WFS and WFS is stayed by the following theorem.Theorem 15 (see [9]).
LetP be a normal logic program. The following equivalence holds: (9)D1-WFSP=WFSP.Proof.
For the class of normal logic programs, the transformation rulesRED+, RED-, SUB, Dsuc, and Dloop are equivalent to N-RED+, N-RED-, N-SUB, Suc, and loop, which have been defined for normal programs [9]. (In [9], the transformation rules N-RED+, N-RED-, N-SUB were named as RED+, RED-, SUB, respectively. In this paper, we added the prefix “N-” in order to denote these transformation rules in the settings of normal logic programs.) Since the rewriting system {N-RED+,N-RED-,N-SUB,Suc,loop} characterizes WFS, CS2 also characterizes WFS.It is worth mentioning that D1-WFS generalizes a system introduced in [18] from normal to disjunctive programs.Let us consider again Example8. As we noticed before, program P reduces to P3. However, P3 still reduces (by RED-) to P4, which is as P3 but the third clause is removed. From P4 we can apply a Dloop reduction to get P5: the single clause c∨d←true. P5 is the residual form of the CS2 system.For this example, it turns out that D′-WFS is equivalent to D1-WFS, but this is not true in general. Take, for instance, the following example.Example 16.
LetP be a disjunctive logic program:
x ← ¬ a . a ← ¬ b . d ← a . c ∨ b . a ← d . b ← c .
We can see thatresCS1(P) has only two clauses: x←true and b←true. This means that the atoms x and b are considered true and the rest of atoms are considered false; hence, D′-WFS(P) = {x,b,¬d,¬c,¬a}. On the other hand, resCS2(P)=P. This means that we cannot apply any transformation rule from CS2 to P. Since all the atoms in the language of P appear in at least one head of the clauses, there are not atoms that can be considered false. Moreover, there are not facts that suggest that there are atoms that can be considered true. Hence, D1-WFS suggests that all the atoms P are undefined. In other words, D1-WFS(P) = ϕ.From Example16, we can observe that D′-WFS and D′-WFS are different in the class of disjunctive logic programs. However for normal programs both semantics are equivalent since they define WFS, but note that the residual programs with respect to CS1 and CS2 are not necessarily the same. An advantage of CS2 over CS1 is that the residual program with respect to CS2 is polynomial-time computable.


## 3. Logic Programming Semantics

This section introduces the main results of this paper. We start by stating and proving some useful properties. Some of these properties can be already proved by other authors or intuitively expected; however, since we did not find explicit references to these properties, the properties are formalized and proved.We start presenting a relationship betweendcomp and supported models.Lemma 17.
LetP be a logic program. M is a supported model of P iff M is a model of dcomp(P).Proof.
M is a model of dcomp(P) iff M is a model of comp(dis-nor(P)) (see Definition 5) iff M is a supported model of dis-nor(P) [1] iff M is a supported model of P (by definition of supported model, see Definition 3).Let us highlight that Lemma17 is introducing an extension of the well-known relationship between the Clark’s competition and supported models [15], which was introduced for the class of normal programs, to a relationship between dcomp and supported models of disjunctive logic programs.In order to avoid misunderstanding, let us now define explicitly the concept ofminimal supported model of a logic program P.Definition 18.
LetP be a program. M is a minimal supported model of P if M is a model of dcomp(P) and it is minimal (with respect to set inclusion) among the models of dcomp(P).We can observe a relationship between minimal supported model and supported models, which are minimal.Lemma 19.
LetP be a program. If M is a minimal model of P and a supported model of P, then M is a minimal supported model of P.Proof.
Our proof is by contradiction. LetM be a minimal model of P, M be a supported model of P, and M be not a minimal supported model of P. Then, there exists a proper subset M′ of M such that M′ is a supported model of P. Thus M′ is a model of P. But since M′ is a proper subset of M, M is not a minimal model of P, obtaining a contradiction.Let us observe that the converse of Lemma19 is false as the following example shows.Example 20.
LetP be the following set of clauses:a←¬a.a←b.b←b.
We can see thatdcomp(P) isa↔¬a∨bb↔b.
Moreover, one can see thatM≔{a,b} is a minimal supported model of dcomp(P), but, M is not a minimal model of P.Now let us introduce two properties regarding the transformation ruleDloop.Lemma 21.
IfP1 is a disjunctive program, P1→DloopAP2, then a∈A implies that for every clause α←Body∈P1 such that a∈α, then Body∩A≠∅.Proof.
It is a straightforward generalization for the case in normal programs [18].Lemma 22.
IfP1→DloopAP2, then Head(P2)∩A=∅.Proof.
By contradiction, supposeHead(P2)∩A≠∅; therefore, there exists a∈Head(P2)∩A. Then, there is a rule of the form a∨α←β∈P2. Hence, a∨α←β∈P1. As a∈A, then there exists b∈β∩A (by Lemma 21). Thus ∨α←β∉P2, by the construction of P2. This leads to a contradiction.Considering the results introduced by Pearce [8], we highlight the following properties in the settings of STABLE.Lemma 23.
LetT1 and T2 be two theories; then T1≡IT2 implies T1≡stableT2.Proof.
It follows immediately by Theorem3.4 in [8].Lemma 24.
IfP is a theory, I a set of atoms, and M any stable model of P, then I∩M=∅⇒P≡stableP∪¬I.Proof.
It follows immediately by Theorem3.4 in [8].The following relationship between stable models and supported models is well known in the state of the art.Lemma 25 (see [14]).
LetP be program; if M is a stable model of P, then M is a supported model of P.We show a property ofDloop regarding minimal models.Lemma 26.
LetP1 be a disjunctive program. If M is minimal model of P1 and P1→DloopAP2, then M∩A=∅.Proof.
SupposeM∩A≠∅; then b∈M and b∈A, so b is not in every minimal model of definite(dir-nor(P)); then definite(dis-nor(P))⊬b, so definite(dis-nor(P))⊬b. Therefore b∉M for all M minimal model of dis-nor(P), thereafter b∉M for all model of P, and then M is not minimal model.Osorio et al. in [19] proved that stable semantics is closed under Dloop.Theorem 27 (Dloop preserve stable, [19]).
LetP1 be a disjunctive program. If P2=Dloop(P1), then P1 and P2 are equivalent under the stable semantics.The following result was presented in [19].Lemma 28 (STABLE is closed underCS2 transformations, [19]).
LetP1 and P2 be two programs related by any transformation in CS2. Then P1 and P2 have the same STABLE models.Considering the style of GL-transformation, the following reduction is introduced.Definition 29.
LetS be a set of literals and P be a program. We define PS as follows:(10)PS=A⟵α∖α∩S∣A⟵α∈P∧∄l∈αwithlc∈S,where lc is the complement of the literal l.In the following lemma, an interesting property of theCS2 system regarding the reduction introduced by Definition 29 is proved.Lemma 30.
LetP1 be a normal program and P2=resCS2(P1). Then P2=PSEMmin(P2).Proof.
First note that ifP is obtained from P1 by a single transformation T∈CS2, then PSEMmin(P)=P1SEMmin(P), so, by a direct induction, we can verify that P2SEMmin(P2)=P1SEMmin(P2). However, P2=P2SEMmin(P2), so, by transitivity, we get the desired result.C S 2 is an interesting rewriting system in the settings of supported models as shown in the following lemma.Lemma 31.
IfP and P1 are two programs such that P1 is obtained from P by any transformation T in CS2, then M is a supported model of P1 implies M is supported model of P.Proof.
Straightforward by checking each case ofT.So far, we have highlighted relevant properties of the rewriting systemCS2, minimal models and supported models. Now we are ready for introducing our first logic programming semantics, which will be based on the aforementioned terms.Definition 32 (D3-WFS-DCOMP).
LetP be a program. We define a D3-WFS-DCOMP model as a minimal model of P that is also a supported model of resCS2(P).It is immediate to see that D3-WFS-DCOMP is more powerful than D1-WFS (see Theorem15). Note that sometimes STABLE is inconsistent, when D3-WFS-DCOMP is not.Example 33.
For instance, let us consider again the logic programP that was introduced by Example 1:d∨e←¬a.c←c.b←a.a←b.a←¬b,¬c.
We know that STABLE is inconsistent. In order to infer a D3-WFS-DCOMP model, we need to inferresCS2(P). One can see that Dloop can be applied to P. Dloop will remove the clause c←c. Hence, P→DloopAP3 such that P3≔P∖{c←c}. In P3, we can apply RED+. After applying RED+, no transformation rule of CS2 can be applied. Hence, resCS2(P) isd∨e←¬a.b←a.a←b.a←¬b.
Let us observe that{a,b} is a minimal model of P; moreover, {a,b} is a supported model of resCS2(P). Hence, {a,b} is a D3-WFS-DCOMP model.We can also observe that every model inferred by D3-WFS-DCOMP is a supported model.Lemma 34.
LetP be a program. If M is D3-WFS-DCOMP model of P, then M is a supported model of P.Proof.
LetM be a D3-WFS-DCOMP model of P, so, M is a supported model of resCS2(P). Thus, by Lemma 31 and a direct induction, M is a supported model of P.Due to its construction, we see that D3-WFS-DCOMP is similar to STABLE. However, STABLE is inconsistent more often than D3-WFS-DCOMP. This comment is formalized in the following theorem, which is one of the main results of this paper.Theorem 35.
LetP be a normal program. (1)
IfM is a D3-WFS-DCOMP model of P, then M extends the WFS semantics (i.e., M agrees in the true/false assignments with WFS).(2)
IfM is a D3-WFS-DCOMP model of P, then M is a minimal model of P as well as a minimal model of comp(P).(3)
M is a STABLE model of P implies M is a D3-WFS-DCOMP model of P.Proof.
( 1 ) It follows by construction and Theorem 15. (2) It follows by construction and Lemmas 19 and 34. (3) Let M be a stable model of P. Hence (by Lemma 28) M is a stable model of resCS2(P). Hence by [14], M is a supported model of resCS2(P). On the other hand, since M is stable model of P, it is well known that M is a minimal model of P. Hence, M is a minimal model of P as well as a supported model of resCS2(P). Finally (by definition) M is a D3-WFS-DCOMP model of P.D3-WFS-DCOMP is the first logic programming semantics that we aim to introduce in this paper. D3-WFS-DCOMP is based on minimal models and supported models; moreover, it considers the normal form (residual program) of the given logic programwith respect toCS2. However, if we consider the reduction introduced by Definition 29 and D′-WFS instead of the normal form of the given logic programwith respect toCS2, we get a new logic programming semantics. Formally, this new logic programming semantics is defined as follows.Definition 36.
LetP be a program. We define a D2-WFS-DCOMP model as a minimal model of P that is also a supported model of PD′-WFS(P).Although both D3-WFS-DCOMP and D2-WFS-DCOMP are based on minimal models and supported models, these logic programming semantics are different.Lemma 37.
The semantics D3-WFS-DCOMP is not equivalent to D2-WFS-DCOMP.Proof.
Consider again Example16. With D3-WFS-DCOMP, we obtain two models: {a,b,d} and {b,x}. However, with D2-WFS-DCOMP we only obtain the model {b,x}.We conjecture the following: for every programP, every D2-WFS-DCOMP model of P is a D3-WFS-DCOMP model of P.As part of our study of logic programming semantics for disjunctive logic programs, we also suggest studying a logic programming semantics that enforces the interpretation of∨ asinclusive disjunction. The interpretation of ∨ as inclusive disjunction has been explored by other authors. For instance, in [20], the authors also define semantics based on this notion.In order to interpret∨ as inclusive disjunction, the concept ofw-supported model is defined as follows.Definition 38.
LetP be a program, aw-supported model M of P is a model of P such that for every a∈M, there is a clause A←body such that a∈A and the body is true in M.Unlike supported models (see Definition3), which allow semantics to infer models with only one true atom in each head of each disjunctive clause,w-supported models allow semantics to infer models with more than one true atom in each head of each disjunctive clause. This subtle difference between supported andw-supported models allows us to define different behaviours of the semantics for disjunctive logic programs.Considering similar constructions to D3-WFS-DCOMP and D2-WFS-DCOMP, the logic programming semantics D3-WFS1-DCOMP is defined as follows.Definition 39.
LetP be a program. We define a D3-WFS1-DCOMP model as a minimal model of P that is also aw-supported model of PD1-WFS(P).An interesting property, which shares the three logic programming semantics introduced in this paper, is that these semantics coincide in the class of normal logic programs.Theorem 40.
LetP be any normal program; then D3-WFS-DCOMP(P) = D2-WFS-DCOMP(P) = D3-WFS1-DCOMP(P).Proof.
Since D1-WFS(P) = D′-WFS(P) (for normal programs) and by Lemma 30, then it is immediate that D3-WFS-DCOMP(P) = D2-WFS-DCOMP(P). Since supported models are the same asw-supported models (for normal programs), then D3-WFS-DCOMP(P) = D3-WFS1-DCOMP(P).Note that, however, for disjunctive programs D3-WFS-DCOMP is (in general) different from D1-WFS1-DCOMP. Take for instance, Example2 in [20].


## 4. Applications

In this section, we present an application of the logic programming semantics introduced in Section3. In particular, we sketch how to extend our semantics to consider programs with clauses allowing an empty head, explicit negation, datalog programs, and finally a lub operator.(i)
With respect to datalog programs, we first obtain the ground instantiation of the program and then we proceed as with propositional programs. This is a well-known approach and we do not discuss it any more.(ii)
With respect to programs with explicit negation, it is possible to reduce programs with explicit negation to programs without it. The idea is originally considered in [21].(iii)
With respect to programs that include clauses with empty head we proceed as follows: Say that we have the clause←α, then simply translate it as a←α, ¬a,wherea is a new atom. Clearly, α is false in every D3-WFS-DCOMP model of the program.


### 4.1. Semantics of lub-Programs

A very interesting issue consists in modeling thesetof operator of PROLOG. In a meeting, whose aim was to get a picture of the activities in logic programming and its role in the coming years, Gelfond pointed out the following:“We need to find elegant ways for accomplishing simple tasks, e.g. counting the numbers of elements in the database satisfying some property P. At the moment we have neither clear semantics nor efficient implementation ofsetof of other aggregates used for this type of problems” [22].Some time has passed since Gelfond has pointed the aforementioned quote; however, his views still hold these days.Let us consider the following example.s(S)←setof(X,p(X),S),where the intended meaning is as follows:s(S) is true when S =X:p(X).Several authors have suggested translating the above expression using negation as failure more or less as follows:s(S)←setof-s(S),setof-s(S)←try-s(S),¬bad-s(S),try-s(S)←p(X), singleton-set(X,S),try-s(S)←try-s(S1), try-s(S2), union(S1,S2,S),try-s(X)←emptyset(X),bad-s(S)←p(X), ¬member(X,S),where union, member, and singleton-set have their intended meaning. For instance,singleton-set(X,S) is true if S={X}. Given any normal program extended withsetof, if the translation is a stratified program, then the stratified model of the program captures the “intended” semantics of the original program [23]. However, when the program is not stratified, then we can consider using stable models. Several times the stable models still captures the intended meaning, but sometimes it becomes undefined.Let us consider the following simple, but yet interesting, example aboutsetof. Consider the definite program:a←trueb←a,crepresented as:rule([a])rule([b,a,c]).That is,rule([X∣Y]) represents the clause X←Y. Think that we want to write a program that computes the minimal model. Bearing in mind the fix-point semantics, we could writemm(S)←setof(X, t-p(X), S).t-p(X)←rule(X,Y), mm(S), subset(Y,S).That is,mm(S) is true (in the intended semantics) iff S is the minimal model of the program represented by the EDB (extensional database) rule.  (It is however questionable if the above program should be considered legal.) Note that mm and t-p are mutually dependent. If we use the translation ofsetof to NF given above, then STABLE has no models at all, while any of our proposed semantics, in Section 3, defines the intended model.Following the approach from [23], but adapted to the more familiar environment of PROLOG, a LUB operator is a generalization ofsetof over anycomplete lattice. The intuitive reading is that LUBL(X,p(X),S) is true if S is theleast upper boundof each X such that p(X).LetP be a logic program:h(X,S)←LUBL(C,n(X,C),S).Now translate the program above as follows:h(X,S)←f=(X,S).f≥(X,S)←n(X,S).In addition, we need to add axioms that relate the predicate symbolsf= with f≥ for each functional symbol f. Let us consider again our example. The axioms for f in this case are as follows:(1)
f=Z,S←f≥Z,S,¬f>Z,S.(2)
f>Z,S←f≥Z,S1,S1>LS.(3)
f≥Z,S←f≥Z,S1,S1>LS.(4)
f≥Z,⊥.(5)
f≥Z,C←f≥(Z,C1),f≥(Z,C2),lubL(C1,C2,C).We understand thatS1>LS means that S1≥LS and S1≠S. And lubL(C1,C2,C) interprets that C is the least upper bound of C1 and C2. The first two clauses are the same (modulo notation) as in Definition 4.2 in [24]. Clause (5) is not useful for total-order domains.Now we need to instantiate the translated program. In this paper we restrict our attention to finite ground programs. By adding simple type declarations, we can ensure to get a finite ground program. In this case, we borrow the declaration style of Relationlog; see [23]. Considering any semantics introduced by Section 3, the intended model of LUBL is inferred.


## 4.1. Semantics of lub-Programs

A very interesting issue consists in modeling thesetof operator of PROLOG. In a meeting, whose aim was to get a picture of the activities in logic programming and its role in the coming years, Gelfond pointed out the following:“We need to find elegant ways for accomplishing simple tasks, e.g. counting the numbers of elements in the database satisfying some property P. At the moment we have neither clear semantics nor efficient implementation ofsetof of other aggregates used for this type of problems” [22].Some time has passed since Gelfond has pointed the aforementioned quote; however, his views still hold these days.Let us consider the following example.s(S)←setof(X,p(X),S),where the intended meaning is as follows:s(S) is true when S =X:p(X).Several authors have suggested translating the above expression using negation as failure more or less as follows:s(S)←setof-s(S),setof-s(S)←try-s(S),¬bad-s(S),try-s(S)←p(X), singleton-set(X,S),try-s(S)←try-s(S1), try-s(S2), union(S1,S2,S),try-s(X)←emptyset(X),bad-s(S)←p(X), ¬member(X,S),where union, member, and singleton-set have their intended meaning. For instance,singleton-set(X,S) is true if S={X}. Given any normal program extended withsetof, if the translation is a stratified program, then the stratified model of the program captures the “intended” semantics of the original program [23]. However, when the program is not stratified, then we can consider using stable models. Several times the stable models still captures the intended meaning, but sometimes it becomes undefined.Let us consider the following simple, but yet interesting, example aboutsetof. Consider the definite program:a←trueb←a,crepresented as:rule([a])rule([b,a,c]).That is,rule([X∣Y]) represents the clause X←Y. Think that we want to write a program that computes the minimal model. Bearing in mind the fix-point semantics, we could writemm(S)←setof(X, t-p(X), S).t-p(X)←rule(X,Y), mm(S), subset(Y,S).That is,mm(S) is true (in the intended semantics) iff S is the minimal model of the program represented by the EDB (extensional database) rule.  (It is however questionable if the above program should be considered legal.) Note that mm and t-p are mutually dependent. If we use the translation ofsetof to NF given above, then STABLE has no models at all, while any of our proposed semantics, in Section 3, defines the intended model.Following the approach from [23], but adapted to the more familiar environment of PROLOG, a LUB operator is a generalization ofsetof over anycomplete lattice. The intuitive reading is that LUBL(X,p(X),S) is true if S is theleast upper boundof each X such that p(X).LetP be a logic program:h(X,S)←LUBL(C,n(X,C),S).Now translate the program above as follows:h(X,S)←f=(X,S).f≥(X,S)←n(X,S).In addition, we need to add axioms that relate the predicate symbolsf= with f≥ for each functional symbol f. Let us consider again our example. The axioms for f in this case are as follows:(1)
f=Z,S←f≥Z,S,¬f>Z,S.(2)
f>Z,S←f≥Z,S1,S1>LS.(3)
f≥Z,S←f≥Z,S1,S1>LS.(4)
f≥Z,⊥.(5)
f≥Z,C←f≥(Z,C1),f≥(Z,C2),lubL(C1,C2,C).We understand thatS1>LS means that S1≥LS and S1≠S. And lubL(C1,C2,C) interprets that C is the least upper bound of C1 and C2. The first two clauses are the same (modulo notation) as in Definition 4.2 in [24]. Clause (5) is not useful for total-order domains.Now we need to instantiate the translated program. In this paper we restrict our attention to finite ground programs. By adding simple type declarations, we can ensure to get a finite ground program. In this case, we borrow the declaration style of Relationlog; see [23]. Considering any semantics introduced by Section 3, the intended model of LUBL is inferred.


## 5. Conclusion and Future Work

The well-founded semantics (WFS) has been regarded as an approximation of the stable semantics STABLE. Moreover, supported model in the settings of the Clark’s complication is other well-established semantics for data management. In this paper, we explored the integration of WFS and the Clark’s complication for defining three logic programming semantics: D3-WFS-DCOMP, D2-WFS-DCOMP, D3-WFS1-DCOMP. Each of these semantics suggests different interpretations of disjunctive logic programs; however, they suggest a common interpretation in the class of normal logic programs (Theorem40).Considering the properties of D3-WFS-DCOMP, D2-WFS-DCOMP, D3-WFS1-DCOMP, these semantics can be regarded as alternative options for STABLE. The aim of our proposals was to explore a misbehavior of disjunctive (and normal) stable semantics that becomes undefined (inconsistent) very often.From our previous research, we have observed that STABLE has problems for capturing basic aggregation operators such assetof. We have sketched some applications of the introduced logic programming semantics for capturing a lub operator, a general form ofsetof. We noticed that STABLE could not define the intended meaning of a simple program that uses our lub operator.It is well-accepted that STABLE is the state of the art in the nonmonotonic reasoning community. Indeed, there is a solid platform of STABLE solvers that has supported the use of STABLE in real applications [1, 25]. Nevertheless, different extensions of STABLE have been suggested in order to deal with some misbehaviors and extensions of STABLE [3, 26–29]. We consider that the particular semantics introduced by this paper suggest a feasible option for logic based specification languages that aim at semantics close to STABLE, WFS, and the Clark’s complication.In [30], we use stable models semantics for capturing Dung’s argumentation approach [31]. Moreover, we have shown that any logic programming semantics can induce an argumentation semantics in the style of Dung’s argumentation approach [32]. Hence, in our future work, we will explore the application of the suggested semantics, in this paper, in abstract argumentation theory. For instance, in argumentation theory, there are a few workswith respect to aggregation of arguments, and we believe that the axiomatization presented in Section 4.1 could be useful for handling aggregation between arguments and/or set of arguments.



---

*Source: 4157030-2018-03-01.xml*