Well-Supported Semantics for Description Logic Programs

1 Introduction

Description logic programs (or DL-programs) are introduced in [Eiter et al., 2008b] as a framework for integrating logic programming under the answer set semantics (ASP) [Gelfond and Lifschitz, 1991] with description logics (DLs) [Baader et al., 2003] for the Semantic Web. ASP is currently a dominating logic programming paradigm, while DLs like SHIF(D)

and SHOIN(D) are the semantical basis of the Web Ontology Language OWL [Horrocks et al., 2003]. A DL-program KB = (L, R) consists of a DL knowledge base L expressing ontologies and an ASP rule base R expressing constraints. L and R are separated in syntax in that they share no predicate symbols in their vocabularies. The exchange of knowledge between the two components is through an interface mechanism in rule bodies, called dl-atoms, which are interpreted as queries to L. It is due to the syntactical separation of L and R that DL-programs are classified as a loosely coupled integration, which is entirely different from the tightly coupled or full integrations such as [de Bruijn et al., 2008; Lukasiewicz, 2010; Motik and Rosati, 2010; Rosati, 2006] (see [Eiter et al., 2008a] for a survey).

In [Eiter et al., 2008b], two different semantics are proposed for DL-programs. One is called the weak answer set semantics, and the other the strong answer set semantics. Let KB = (L,R) be a DL-program and I an interpretation. Informally, I is a weak answer set of KB if I is the least model of the transformed logic program wRIL which is obtained from ground(R) (the grounding of R) by first removing all rules whose bodies are not satisfied by I, then removing all negative literals and dl-atoms from the remaining rules. [Eiter et al., 2008b] note that an obvious disadvantage of the weak answer set semantics is that it may produce counterintuitive answer sets with circular justifications by selfsupporting loops. The circular justifications are caused by some dl-atoms in rule bodies, but these dl-atoms are completely ignored (deleted) in wRIL. In order to overcome this problem, [Eiter et al., 2008b] further introduce the strong answer set semantics, which is different from the weak one in that only nonmonotonic dl-atoms are deleted in the transformation. A dl-atom A is monotonic relative to KB if for any interpretations I and J with I ⊆ J, if I satisfies A then J satisfies A. I is a strong answer set of KB if I is the least model of the transformed logic program sRIL obtained from ground(R) by first removing all rules whose bodies are not satisfied by I, then removing all negative literals and nonmonotonic dl-atoms from the remaining rules.

It turns out that the strong answer set semantics cannot overcome the problem of circular justifications. Some circular justifications are caused by nonmonotonic dl-atoms, but these dl-atoms are all deleted and thus ignored in sRIL.

For normal logic programs, the problem of circular justifications is elegantly handled by means of Fages' wellsupportedness [Fages, 1994]. Informally, an interpretation I is well-supported if there is a level mapping on I such that for every a ∈ I, there is a rule in ground(R) of the form a ← b1, · · · , bm, not c1, · · · , not cn such that I satisfies the body of the rule and for each bi, the level of bi is lower than the level of a. By enforcing the well-supportedness condition on interpretations, answer sets of normal logic programs are guaranteed to be free of circular justifications.

Fages' definition of well-supportedness does not apply to DL-programs, since it handles circular justifications caused only by positive literals (atoms) in rule bodies. The question naturally arises: can we extend Fages' well-supportedness from normal logic programs to DL-programs and define a well-supported answer set semantics for DL-programs such that its answer sets are free of circular justifications? Definitely, the extension is nontrivial and challenging because circular justifications in a DL-program are caused either by positive literals (atoms or dl-atoms) or negative literals (negative atoms or negative dl-atoms) in rule bodies.

In this paper, we extend Fages' well-supportedness to DLprograms. In particular, we introduce two forms of wellsupportedness for DL-programs. The first one defines what we call weakly well-supported models, which are free of circular justifications caused by positive literals in rule bodies. The second one defines strongly well-supported models, which are free of circular justifications caused by either positive or negative literals. The two forms of well-supportedness are proper extensions of Fages' well-supportedness in that when applied to a DL-program KB = (L, R) that represents a normal logic program (i.e., L is empty and R contains no dl-atoms), they coincide with Fages' well-supportedness. We show that the weak answer set semantics and the strong answer set semantics of [Eiter et al., 2008b] satisfy neither the weak nor the strong well-supportedness condition, even for DL-programs without negative dl-atoms. This explains why their answer sets incur circular justifications.

We then define two new answer set semantics for DLprograms and characterize them in terms of the weakly and strongly well-supported models, respectively. The first semantics is based on an extended Gelfond-Lifschitz transformation and defines what we call weakly well-supported answer sets. Such answer sets are free of circular justifications for the class of DL-programs without negative dl-atoms. The second semantics does not rely on program transformations and defines strongly well-supported answer sets which are free of circular justifications for all DL-programs. We show that strongly well-supported answer sets are weakly wellsupported answer sets that are also strong answer sets.

2 DL-Programs

We follow the notation of [Eiter et al., 2008b] and assume familiarity with the basics of description logics (DLs) [Baader et al., 2003], especially with the DLs SHIF(D) and SHOIN(D) [Horrocks et al., 2003]. A DL knowledge base L consists of a finite set of axioms built over a vocabulary ΣL = (A∪R, I), where A, R and I are pairwise disjoint (denumerable) sets of atomic concepts, atomic roles and individuals, respectively. DLs are fragments of first-order logic, so the DL knowledge base L has the first-order semantics.

Let P be a finite set of predicate symbols and C a nonempty finite set of constants such that P∩ (A∪R) = ∅ and C ⊆ I. A term is either a constant from C or a variable. An atom is of the form p(t1, ..., tm), where p is a predicate symbol fromP, and ti is a term. An equality (resp. inequality) is of the form t1 = t2 (resp. t1 ̸= t2), where t1 and t2 are terms. A dl-query is of the form Q(t), where t is a list of terms, and Q is an equality/inequality symbol, a concept, a role, a concept inclusion axiom, or their negation, built from A ∪ R.

A dl-atom is of the form DL[S1op1p1, · · · , Smopmpm; Q](t), where Si is a concept or role built from A∪R, or an equality/inequality symbol; opi ∈ { ∪+ , ∪- , ∩- } is an operator; pi ∈ P is a unary predicate symbol if Si is a concept, and a binary predicate symbol otherwise; and Q(t) is a dlquery. The semantics of each operator opi shall be defined in Definition 1 below.

A dl-rule (or rule) r is of the form

where H is an atom, and the Ais and Bis are atoms or equalities/inequalities or dl-atoms. Each Ai is called a positive literal, and each not Bi called a negative literal. We use head(r) and body(r) to denote the head H and the body A1, · · · , Am, not B1, · · · , not Bn, respectively. We also use pos(r) to denote the positive literals A1, · · · , Am, and neg(r) to denote the negative literals not B1, · · · , not Bn. Therefore, a rule r can simply be written as head(r) ← body(r) or head(r) ← pos(r), neg(r).

A rule base R is a finite set of rules. R is a normal logic program if it is free of dl-atoms, equalities and inequalities.

A DL-program is a combined knowledge base KB = (L, R), where L is a DL knowledge base and R is a rule base.

A ground instance of a rule r is obtained by first replacing every variable in r with a constant fromC, then removing all valid equalities and inequalities (under the unique name assumption). A ground instance of r is consistent if it contains no equalities or inequalities. Let ground(R) denote the set of all consistent ground instances of rules in R.

The Herbrand base of R, denoted HBR, is the set of all ground atoms p(t1, ..., tm), where p ∈ P occurs in R and each ti is in C. Any subset of HBR is an interpretation. For an interpretation I, let I - = HBR \ I and ¬I - = {¬a | a ∈ I -}.

For a normal logic programR, an interpretation I satisfies an atom a ∈ HBR if a ∈ I, and I satisfies not a if a ̸∈ I. The satisfaction is extended to DL-programs as follows.

Definition 1 Let KB = (L,R) be a DL-program and I an interpretation. Define the satisfaction relation under L, denoted |=L, as follows:

1. For a ground atom a ∈ HBR, I |=L a if a ∈ I.
2. For a ground dl-atom A = DL[S1op1p1, · · · , Smopmpm;Q](c) occurring in ground(R), I |=L A if L∪⋃mi=1 Ai |= Q(c), where |= is the entailment relation

in first-order logic and

For a ground atom or dl-atom A, I |=L not A if I ̸|=L A. For a rule r in ground(R), I |=L body(r) if for each (positive or negative) literal l in body(r), I |=L l; I |=L r if I ̸|=L body(r) or I |=L head(r). An interpretation I is a model of KB if I |=L r for all r ∈ ground(R). A minimal model is a model that is minimal in terms of set inclusion.

A ground dl-atom A is monotonic relative to KB if for any I ⊆ J ⊆ HBR, I |=L A implies J |=L A. Otherwise, A is nonmonotonic. KB is positive if R is free of the negation symbol not, and that every dl-atom occurring in ground(R) is monotonic relative to KB. A positive DL-program KB has the least model.

For an interpretation I, let sRIL be the reduct obtained from ground(R) by deleting (i) every rule r with I ̸|=L body(r), and (ii) from the remaining rules all negative literals and all nonmonotonic dl-atoms. Let wRIL be obtained in the same way as sRIL except that in (ii) all negative literals and all dlatoms are deleted.

[Eiter et al., 2008b] define I to be a strong (resp. weak) answer set of KB if I is the least model of sRIL (resp. wRIL).

3 Well-Supported Semantics

For some DL-programs, applying the weak or strong answer set semantics may produce answer sets with circular justifications. For the weak answer set semantics, this problem is illustrated in [Eiter et al., 2008b] with an example DLprogram KB = (L,R), where L = ∅ and R = {p(a) ← DL[c ∪+ p; c](a)}. This DL-program has two weak answer sets: I1 = ∅ and I2 = {p(a)}. Let us use the symbol ⇐ to express "truth is supported by". Then p(a) in I2 is circularly justified by a self-supporting loop: p(a) ⇐ DL[c ∪+ p; c](a) ⇐ p(a).

The next DL-program illustrates that for the strong answer set semantics, the circular justification problem persists.

Example 1 Let KB = (L,R), where L = ∅ and R = {p(a) ← DL[c ∪+ p, b ∩- q; c ⊓ ¬b](a)}. The dl-atom in R queries L if a is in the concept c but not in the concept b, under the assumption that for any x, if p(x) is true then x is in c and if q(x) is false then x is not in b. This dl-atom is nonmonotonic, so both I1 = ∅ and I2 = {p(a)} are strong answer sets of KB. Observe that p(a) in I2 is circularly justified by a self-supporting loop: p(a) ⇐ DL[c ∪+ p, b ∩- q; c ⊓ ¬b](a) ⇐ p(a) ∧ ¬q(a).

We observe that the reason behind circular justifications is that the weak/strong answer set semantics does not satisfy the condition of well-supportedness. The notion of wellsupportedness is introduced in [Fages, 1994]. For a normal logic programR, an interpretation I is well-supported if there exists a strict well-founded partial order ≺ on I such that for any a ∈ I, there is a rule a ← body(r) in ground(R) such that I satisfies body(r) and for every positive literal b in body(r), b ≺ a. A binary relation ≤ is well-founded if there is no infinite decreasing chain a0 ≥ a1 ≥ · · ·. Clearly, a wellsupported interpretation I guarantees that every a ∈ I is free of circular justifications.

Fages' definition of well-supportedness does not apply to DL-programs. On the one hand, positive literals in a normal logic program are only atoms, but in a DL-program, positive literals in rule bodies may be dl-atoms. On the other hand, circular justifications in a normal logic program are caused only by positive literals in rule bodies, but in a DL-program, some circular justifications are caused by negative literals.

In this section, we extend Fages' well-supportedness to DL-programs and define new answer set semantics for DLprograms that satisfy the extended well-supportedness condition. We start by introducing a notion of up to satisfaction.

Definition 2 Let KB = (L, R) be a DL-program, and E and I be two sets of atoms in HBR with E ⊆ I. For any ground literal l, we define "E up to I satisfies l under L," denoted (E, I) |=L l, as follows:

1. For a ground atom a ∈ HBR, (E, I) |=L a if a ∈ E; (E, I) |=L not a if a ̸∈ I.
2. For a ground dl-atom A, (E, I) |=L A if for every F with E ⊆ F ⊆ I, F |=L A; (E, I) |=L not A if for no F with E ⊆ F ⊆ I, F |=L A.

As the phrase "up to" suggests, for any ground (positive or negative) literal l, (E, I) |=L l means that for all interpretations F between E and I, F |=L l. This implies that the truth of l depends on E and ¬I - and is independent of atoms in I \ E, since for any a ∈ I \ E and any interpretation F with E ⊆ F ⊆ I, whether or not a is in F, F |=L l.

This up to satisfaction has the property of monotonicity.

Proposition 1 Let A be a ground atom or ground dl-atom. For any E1 ⊆ E2 ⊆ I, if (E1, I) |=L A then (E2, I) |=L A, and if (E1, I) |=L not A then (E2, I) |=L not A.

3.1 Well-Supportedness for DL-Programs

In normal logic programs, circular justifications are caused only by some positive literals in rule bodies. Therefore, in Fages' definition of well-supportedness, it is required that for any a in an interpretation I, there should be a rule a ← body(r) such that I satisfies body(r) and for every positive literal b in body(r), b ≺ a.

Following Fages' definition, we introduce a form of wellsupportedness for DL-programs, which overcomes circular justifications caused only by positive literals in rule bodies. The idea is as follows: for each a ∈ I we require that there exist a rule a ← body(r) and a proper subset E of I such that for each positive literal l in body(r), (E, I) |=L l, where E contains only atoms whose truth in I is not circularly dependent on a. Recall that when (E, I) |=L l, the truth of l depends only on E and ¬I -, independently of I \ E. Therefore, the truth of a ∈ I depends only on E and ¬I - and thus a will have no circular justification caused by positive literals in rule bodies. Formally, we have

Definition 3 Let KB = (L,R) be a DL-program. An interpretation I is weakly well-supported if there exists a strict well-founded partial order ≺ on I such that for any a ∈ I, there is a rule a ← body(r) in ground(R) and a subset E ⊂ I such that (1) I |=L body(r) and for every b ∈ E, b ≺ a, and (2) for every positive literal l in body(r), (E, I) |=L l.

The condition "for every b ∈ E, b ≺ a" means that the truth of all atoms in E is not circularly dependent on a. The following result shows that Definition 3 is a proper extension to Fages' well-supportedness.

Theorem 1 Let KB = (L, R) be a DL-program, where L = ∅ and R is a normal logic program. An interpretation I is weakly well-supported iff I is well-supported under Fages' definition.

The following example illustrates that neither the weak nor the strong answer set semantics satisfies this extended wellsupportedness condition, which explains why their answer sets incur circular justifications.

Example 2 Consider KB = (L,R) in Example 1. I1 = ∅ and I2 = {p(a)} are both strong and weak answer sets of KB. Obviously, I1 = ∅ is weakly well-supported. Consider I2 = {p(a)}. For p(a) ∈ I2, we have a single rule r in ground(R) with the head p(a) and a single proper subset E = ∅ of I2. body(r) has a single positive literal l = DL[c ∪+ p, b ∩- q; c ⊓ ¬b](a). I2 |=L body(r), but (E, I2) ̸|=L l. Thus, I2 is not weakly well-supported.

Weakly well-supported interpretations are free of circular justifications caused by positive literals in rule bodies. However, in DL-programs circular justifications may also be caused by some negative literals in rule bodies, as illustrated in the next example.

Example 3 Let KB = (L,R), where L = ∅ and R = {p(a) ← not DL[c ∪+ p, c ∩- p; ¬c](a)}. I1 = ∅ and I2 = {p(a)} are both strong and weak answer sets of KB. They are also weakly well-supported. For p(a) ∈ I2, however, we have a circular justification, p(a) ⇐ not DL[c ∪+ p, c ∩- p; ¬c](a) ⇐ p(a), which is caused by the negative literal in the rule body.

To eliminate all circular justifications, we introduce another form of well-supportedness.

Definition 4 Let KB = (L, R) be a DL-program. An interpretation I is strongly well-supported if there exists a strict well-founded partial order ≺ on I such that for any a ∈ I, there is a rule a ← body(r) in ground(R) and a subset E ⊂ I such that (E, I) |=L body(r) and for every b ∈ E, b ≺ a.

The conditions "(E, I) |=L body(r)" and "for every b ∈ E, b ≺ a" suggest that the truth of a is determined by body(r) whose truth is determined by E and ¬I -, where for no b ∈ E, its truth is circularly dependent on a. This eliminates circular justifications on a, caused either by positive literals or negative literals in rule bodies.

Proposition 2 If an interpretation I is strongly wellsupported, then I is weakly well-supported.

The converse does not hold. For instance, in Example 3, I2 = {p(a)} is weakly well-supported. For p(a) ∈ I2, we have a single rule r in ground(R) with the head p(a) and a single proper subset E = ∅ of I2. Although I2 |=L body(r), (E, I2) ̸|=L body(r). Thus I2 is not strongly well-supported.

However, when a DL-program contains no negative dlatoms in rule bodies, the two forms of well-supportedness coincide.

Theorem 2 For a DL-program KB = (L, R), where R contains no negative dl-atoms, an interpretation I is strongly well-supported iff I is weakly well-supported.

Since normal logic programs can be viewed as special DLprograms without dl-atoms, the following corollary is immediate from Theorems 1 and 2.

Corollary 1 Let KB = (L,R) be a DL-program, where L = ∅ and R is a normal logic program. An interpretation I is strongly well-supported iff I is well-supported under Fages' definition.

3.2 Well-Supported Semantics for DL-Programs

We define answer sets for DL-programs that are either weakly well-supported or strongly well-supported models. First, we introduce an immediate consequence operator TKB in terms of the up to satisfaction (E, I) |=L l.

Definition 5 Let KB = (L, R) be a DL-program and E and I be two sets of ground atoms with E ⊆ I ⊆ HBR. Define

A key property is that when the second argument I is a model of KB, TKB is monotone w.r.t. its first argument E.

Theorem 3 Let KB = (L,R) be a DL-program and I a model of KB. For any E1 ⊆ E2 ⊆ I, TKB(E1, I) ⊆ TKB(E2, I) ⊆ I.

Therefore, for any model I of KB, the monotone sequence 〈T iKB (∅, I)〉∞i=0 , where T 0KB (∅, I) = ∅ and T i+1 KB (∅, I) = TKB(T iKB (∅, I), I), converges to a fixpoint, denoted T α KB (∅, I). This fixpoint has the following important property.

Theorem 4 Let KB = (L,R) be a DL-program and I a model of KB. If I = T α KB (∅, I), then I is a minimal model of KB.

Next, we define two new answer set semantics for DLprograms in terms of TKB. The first one is based on an extended Gelfond-Lifschitz transformation. Recall that for a normal logic programR and an interpretation I, the standard Gelfond-Lifschitz transformation of Rw.r.t. I is

Since RI has no negative literals in rule bodies, it has the least model. The standard ASP semantics defines I to be an answer set of R if I is the least model of RI [Gelfond and Lifschitz, 1991].

We extend the standard Gelfond-Lifschitz transformation to DL-programs simply by replacing the satisfaction relation for normal logic programs with the satisfaction relation |=L for DL-programs, as formulated below.

Definition 6 Given a DL-program KB = (L,R) and an interpretation I, the Gelfond-Lifschitz transformation of R w.r.t. I under L is

We then apply this extended Gelfond-Lifschitz transformation to define answer sets for DL-programs.

Definition 7 Let KB = (L, R) be a DL-program, I a model of KB, and KBI = (L,RI ). I is an answer set of KB if I coincides with the fixpoint T α KBI (∅, I).

Example 4 Consider KB = (L, R) of Example 1. For I1 = ∅, the Gelfond-Lifschitz transformation of R w.r.t. I under L is RI1 = ∅, so the fixpoint T α KBI1 (∅, I1) is empty. Therefore, I1 is an answer set of KB. For I2 = {p(a)}, the extended Gelfond-Lifschitz transformation RI2 = R and the fixpoint T α KBI2 (∅, I2) = ∅. Since I2 ̸= T α KBI2 (∅, I2), I2 is not an answer set of KB.

Such answer sets can be characterized by weakly wellsupported models.

Theorem 5 Let KB = (L,R) be a DL-program and I a model of KB. I is an answer set of KB under Definition 7 iff I is a weakly well-supported model of KB.

Due to this result, we call answer sets under Definition 7 weakly well-supported answer sets.

Theorem 6 For any DL-program KB, weakly wellsupported answer sets of KB are strong answer sets of KB.

As Example 4 shows, strong answer sets may not be weakly well-supported answer sets.

As illustrated in Example 3, weakly well-supported models may have circular justifications caused by negative dl-atoms in rule bodies. Such circular justifications persist in weakly well-supported answer sets. Observe that in the extended Gelfond-Lifschitz transformation RI , all negative literals in rule bodies are dropped so that circular justifications caused by negative dl-atoms are completely missed. To overcome this problem, we present another definition of answer sets without using the extended Gelfond-Lifschitz transformation.

Definition 8 Let KB = (L, R) be a DL-program. A model I of KB is an answer set of KB if I coincides with the fixpoint T α KB (∅, I).

Example 5 Consider KB = (L,R) in Example 3, where R = {p(a) ← not DL[c ∪+ p, c ∩- p; ¬c](a)}. I1 = ∅ and I2 = {p(a)} are models of KB. T α KB (∅, I1) = ∅, so I1 is an answer set. For I2, T 0KB (∅, I2) = ∅ and T 1KB (∅, I2) = TKB(∅, I2) = ∅, so T α KB (∅, I2) = ∅. Therefore, I2 is not an answer set of KB.

Answer sets under Definition 8 can be characterized by strongly well-supported models.

Theorem 7 Let KB = (L,R) be a DL-program and I a model of KB. I is an answer set of KB under Definition 8 iff I is a strongly well-supported model of KB.

Due to this property, we call such answer sets strongly wellsupported answer sets. The following corollary is immediate from Theorem 4.

Corollary 2 For any DL-program KB, strongly wellsupported answer sets of KB are minimal models of KB.

As shown in Example 3, weakly well-supported (resp. strong or weak) answer sets are not necessarily minimal models. The following result follows from Proposition 2.

Corollary 3 For any DL-program KB, strongly wellsupported answer sets of KB are also weakly well-supported answer sets of KB.

The next result follows from Theorem 2.

Corollary 4 Let KB = (L, R) be a DL-program, where R contains no rules with negative dl-atoms. A model I of KB is a strongly well-supported answer set iff I is a weakly wellsupported answer set.

As a result, for any DL-program KB = (L,R), its strongly well-supported answer sets are also weakly wellsupported answer sets that are also strong answer sets that are also weak answer sets. When L = ∅ and R is a normal logic program, all of the four answer set semantics coincide with the standard ASP semantics.

4 RelatedWork

To deal with the circular justification problem with the weak answer set semantics, [Eiter et al., 2008b] introduce the strong answer set semantics. However, examples show that this problem persists in the strong answer set semantics. In [Eiter et al., 2005], the authors also propose another answer set semantics for DL-programs by means of FLP-reduct [Faber et al., 2004]. Given a DL-program KB = (L,R) and an interpretation I, the FLP-reduct of R w.r.t. I, denoted fRI , is the set of all rules r ∈ ground(R) such that I |=L body(r). Then, I is defined to be an answer set of KB if I is a minimal model of fRI .

FLP-reduct based answer sets of KB are minimal models of KB. This shows an advantage over the weak/strong answer set semantics. However, it turns out that the problem of circular justifications occurring in weak/strong answer sets persists in FLP-reduct based answer sets. As an illustration, consider a DL-program KB = (L,R), where L = ∅ and R consists of two rules: p(a) ← q(a) and q(a) ← DL[c ∪+ p, b ∩- q; c ⊔ ¬b](a). KB has only one model I = {p(a), q(a)}. The FLP-reduct fRI of R w.r.t. I is the same as R. Therefore, I is an answer set of KB under the FLP-reduct based semantics. We see that p(a) ∈ I is circularly justified by a self-supporting loop: p(a) ⇐ q(a) ⇐ DL[c ∪+ p, b ∩- q; c ⊔ ¬b](a) ⇐ p(a) ∨ ¬q(a). Note that p(a) ⇐ q(a) ⇐ · · · ⇐ p(a)∨¬q(a) implies p(a) ⇐ q(a) ⇐ · · · ⇐ p(a), since the truth of q(a) cannot be supported by ¬q(a). It is easy to check that I is neither strongly nor weakly well-supported.

The notion of FLP-reduct is first introduced in [Faber et al., 2004], where it is used to define an answer set semantics for logic programs with aggregates (or abstract constraints). Our definition of the up to satisfaction relation (E, I) |=L l (Definition 2) is inspired by the notion of conditional satisfaction introduced by [Son et al., 2007], which is also used to define an answer set semantics for logic programs with abstract constraints. Although logic programs with abstract constraints and DL-programs are significantly different, their semantical issues are closely related. This is first observed by [Eiter et al., 2008b].

To address the problem of circular justifications, recently [Wang et al., 2010] extend the notion of loop formulas [Lin and Zhao, 2004] to DL-programs and propose a canonical answer set semantics by means of loop formulas. This approach first constructs the completion COMP(KB) of a DLprogram KB, then constructs the set LF(KB) of all loop formulas from KB, and finally defines a canonical answer set to be a model of COMP(KB) ∪ LF(KB). It turns out that this loop formula based semantics also incurs circular justifications. Consider a DL-program KB = (L, R), where L = {¬e(b), f(a)} and R consists of two rules: p(b) ← p(a) and p(a) ← DL[e ∪+ p, f ∩- p; f](b). I = {p(a), p(b)} is a canonical answer set of KB, but p(b) ∈ I is circularly justified by a self-supporting loop: p(b) ⇐ p(a) ⇐ DL[e ∪+ p, f ∩- p; f](b) ⇐ ¬p(a) ∨ p(b). It is easy to check that I is neither strongly nor weakly well-supported.

5 Summary

[Fages, 1994] introduces the notion of well-supportedness as a key requirement for the semantics of normal logic programs and characterizes the standard ASP semantics in terms of the well-supportedness condition. In this paper, we extend Fages' work to DL-programs. We introduce two forms of well-supportedness for DL-programs. The first one defines weakly well-supported models that are free of circular justifications caused by positive literals in rule bodies. The second one defines strongly well-supported models that are free of circular justifications caused by either positive or negative literals. We then define two new answer set semantics for DL-programs and characterize them in terms of weakly and strongly well-supported models, respectively. While the weakly well-supported answer set semantics is free of circular justifications for the class of DL-programs without negative dl-atoms, the strongly well-supported semantics is free of circular justifications for all DL-programs. Our simple examples demonstrate that the existing answer set semantics for DL-programs, such as the weak answer set semantics, the strong answer set semantics, and the FLP-based answer set semantics, satisfy neither the strong nor the weak wellsupportedness condition, even for DL-programs without negative dl-atoms. This explains why their answer sets incur circular justifications.

As interesting future work, we are extending the wellsupportedness to disjunctive DL-programs, where the head of a rule is a disjunction of atoms. We are also deeply exploiting the semantical connections between DL-programs and logic programs with abstract constraints. Moreover, practically implementing the proposed well-supported semantics for DLprograms presents a challenging task.

Acknowledgments

We would like to thank all anonymous reviewers for their helpful comments. This work is supported in part by NSFC grants 60970045 and 60833001.