A Model-Theoretic Counterpart of Loop Formulas

1 Introduction

The completion semantics [Clark, 1978] and the answer set semantics (also known as the stable model semantics) [Gelfond and Lifschitz, 1988] are two well-known proposals for defining the meaning of negation as failure in logic programs. 1 The former is attractive because it is simply a translation from logic programs to classical logic, but it sometimes gives unintuitive results [Przymusinski, 1989, Section 4.1]. It is well known that an answer set for a logic program is also a model of its completion, while the converse, generally, does not hold.

By adding so-called "loop formulas" to completion, Lin and Zhao [2004] defined a set of formulas whose models are exactly the answer sets. The idea comes from observing that "loops" are related to the mismatch between the models of the completion and the answer sets. Intuitively, every atom in an answer set can be "derived" from a program in a finite number of steps. The atoms in a loop that are not "supported from outside" cannot be derived in a finite number of steps, but they do not contradict the completion of the program.

1 As the answer set semantics is usually defined for propositional (grounded) logic programs only, in this paper we limit our attention to such programs, and refer to the propositional case of Clark's completion.

The Lin/Zhao theorem allows us to compute answer sets using SAT solvers, which has led to the implementation of SAT-based answer set solvers ASSAT 2 [Lin and Zhao, 2004] and CMODELS 3 [Giunchiglia et al., 2004]. These systems turn a logic program into a propositional theory and then call SAT solvers, such as CHAFF, SATO and RELSAT, to find its models, which in turn correspond to the answer sets. Thanks to recent progress with SAT solvers, in several benchmark examples they found answer sets faster than other answer set solvers such as SMODELS 4 and DLV 5 .

A program that has no loops is called "tight," and for tight programs the completion semantics and the answer set semantics are equivalent to each other. This fact was discovered earlier by Fages [1994], and then was generalized and extended by Erdem and Lifschitz [2003] to programs with nested expressions (in the sense of [Lifschitz et al., 1999]) in the bodies of rules.

Lee and Lifschitz [2003] showed that program completion, loop formulas and the Lin/Zhao theorem can be extended to disjunctive logic programs and, more generally, to arbitrary programs with nested expressions. As a consequence, the concept of a tight program and Fages' theorem are extended to disjunctive programs as well.

Yet the previous work on loop formulas has been limited to finite programs without classical negation. In this paper, we lift these limitations. First, to account for programs that allow classical negation, we propose a model-theoretic counterpart of loop formulas-the concept of an "externally supported" set. It is similar to the model-theoretic counterpart of Clark's completion-the concept of a supported set introduced in [Apt et al., 1988]. Interestingly, this reformulation of loop formulas shows that they are related to assumption sets [Sacc´a and Zaniolo, 1990] and to unfounded sets [Van Gelder et al., 1991; Leone et al., 1997] invented many years earlier. Second, we extend the concept of a loop formula to programs with nested expressions. Finally, we extend the notion of a loop and the theorem on loop formulas to infinite programs.

In the next section we introduce the concept of an externally supported set, extend the notion of a loop to infinite programs, state our main theorem, and discuss its relation to Fages' theorem about tight programs. In Section 3 we use the main theorem to define two transformations turning a logic program into an equivalent propositional theory. In Section 4, we relate externally supported sets to assumption sets and to unfounded sets, and compare our reformulation of loop formulas with the original definition by Lin and Zhao. The main theorem is generalized to arbitrary programs with nested expressions in Section 5.

2 http://assat.cs.ust.hk/ .

3 http://www.cs.utexas.edu/users/tag/cmodels/ .

4 http://www.tcs.hut.fi/Software/smodels/ .

5 http://www.dbai.tuwien.ac.at/proj/dlv/ .

2 Externally Supported Sets

2.1 Nondisjunctive Case

We begin with a review of the answer set semantics for nondisjunctive programs given in [Gelfond and Lifschitz, 1991, Section 2]. 6 The words atom and literal are understood here as in propositional logic; we call the negation sign BM in negative literals classical negation, to distinguish it from the symbol for negation as failure (not).

A nondisjunctive rule is an expression of the form

(BD AK D1 AK D2) where all D0 CX are literals. We will often write (1) in the form

where BU is D0 BE BN BM BM BM BN D0 D1 , and BY is not D0 D1B7BD BN BM BM BM BN not D0 D2 , and we will sometimes identify BU with the set CUD0 BE BN BM BM BM BN D0 D1 CV.

A nondisjunctive (logic) program is a set of rules of the form (1).

We say that a set CG of literals satisfies the body BUBN BY of rule (2) (symbolically CG CYBP BUBN BY) if D0 BE BN BM BM BM BN D0 D1 BE CG, and D0 D1B7BD BN BM BM BM BN D0 D2 BPBE CG. We say that CG satisfies a nondisjunctive program A5 (symbolically CG CYBP A5) if, for every rule (2) of that program, D0 BD BE CG whenever CG satisfies BUBN BY .

The reduct A5 CG of a nondisjunctive program A5 with respect to a set CG of literals is obtained from A5 by deleting each rule (2) such that CG BICYBP BY , and replacing each remaining rule (2) by D0 BD AW BU. A consistent set CG of literals is an answer set for A5 if CG is minimal among the sets of literals that satisfy A5 CG .

We say that a set CH of literals is supported by A5 w.r.t. a set CG of literals if there is a rule (2) in A5 such that D0 BD BE CH , and CG CYBP BUBN BY. Informally, such a rule (2) characterizes a source of support for the literal D0 BD in CH . 7

Now we make the notion of a supported set slightly stronger. We will say that a set CH of literals is externally supported by A5 w.r.t. CG if there is a rule (2) in A5 such that D0 BD BE CH , CG CYBP BUBN BY, and BU CK CH BP BN. Informally, the new, third condition ensures that the support for the literal D0 BD in CH comes from outside of CH .

6 Here we do not allow inconsistent answer sets.

7 One may notice that this definition is slightly different from the usual definition of a supported set, which says that a set CG of literals is supported by A5 if, for every literal D0 BD BE CG, there is a rule (2) in A5 such that CG CYBP BUBN BY [Apt et al., 1988]. It is clear that our definition is more general: CG is supported by A5 under the usual definition iff every singleton subset of CG is supported by A5 w.r.t. CG under the new definition.

For example, consider the following programA5 BD :

Each of the sets CUD4CV and CUD5CV is externally supported (hence also supported) by A5 BD w.r.t. CUD4BN D5CV, while CUD4BN D5CV is supported but not externally supported by A5 BD w.r.t. CUD4BN D5CV. On the other hand, let A5 BE be the following program that adds two rules to A5 BD :

Then every nonempty subset of CUD4BN D5CV is externally supported by A5 BE w.r.t. CUD4BN D5CV.

The positive dependency graph of A5 is the directed graph such that

• AF its vertices are the literals occurring in A5, and
• AF its edges go from D0 BD to D0 BE BN BM BM BM D0 D1 for each rule (1) of A5.

When A5 is finite, a nonempty set  of literals is called a loop of A5 if, for every pair D0 BD , D0 BE of literals in , there exists a path from D0 BD to D0 BE in the positive dependency graph of A5 such that all vertices in this path belong to . 8 In other words, a nonempty set  of literals is a loop of A5 iff the subgraph of the positive dependency graph of A5 induced by  is strongly connected. Note that, for every literal D0 that occurs in A5, the singleton set CUD0CV is a loop, according to this definition. 9

The positive dependency graph of A5 BE , shown in Figure 1, has four loops: CUD4CV,CUD5CV,CUD6CV,CUD4BN D5CV.

Main Theorem for Finite Nondisjunctive Programs For any finite nondisjunctive program A5 and any consistent set CG of literals, the following conditions are equivalent:

• B4CPB5 CG is an answer set for A5.
• B4CQB5 CG satisfies A5, and every set of literals that has a common element with CG is externally supported by A5 w.r.t. CG.
• B4 B5 CG satisfies A5, and every loop of A5 that is contained inCG is externally supported by A5 w.r.t. CG.

Out of the three implications B4CPB5 to B4CQB5, B4CQB5 to B4 B5, B4 B5 to B4CPB5, the second is obvious, because every loop that is contained in CG has a common element with CG. Program A5 BE above has two answer sets: CUD4BN D5CV and CUD6CV. Since B4CPB5 implies B4CQB5, it follows that every set of atoms that has a common element with CUD4BN D5CV is externally supported w.r.t. CUD4BN D5CV, and every set of atoms that has a common element with CUD6CV is externally supported w.r.t. CUD6CV. On the other hand, since B4 B5 implies B4CPB5, to show that CUD4BN D5CV is an answer set we only need to check that every loop which is a subset of CUD4BN D5CV (that is, each of CUD4CV, CUD5CV, CUD4BN D5CV) is externally supported w.r.t. CUD4BN D5CV. Similarly, to show that CUD6CV is an answer set, we only need to check that CUD6CV is externally supported w.r.t. CUD6CV.

8 Note that we do allow paths of length BC.

9 Thus our definition is slightly different from the definition by Lin and Zhao (See Section 4 for detail). The example of a singleton loop shows that a loop of A5 does not necessarily correspond to a loop (or cycle) of the positive dependency graph of A5 in the sense of graph theory.

The equivalence between B4CPB5 and B4CQB5 is a generalization of a theorem from [Sacc´a and Zaniolo, 1990] as we will discuss in Section 4.1, and the equivalence between B4CPB5 and B4 B5 is a model-theoretic account of loop formulas as we will discuss in Section 3.

2.2 Extension to Programs in Canonical Form

We will extend the main theorem to finite programs with nested expressions [Lifschitz et al., 1999]. In this section, for simplicity, instead of arbitrary rules with nested expressions, we consider rules of the form

(BC AK CZ AK D1 AK D2 AK D4) where all D0 CX are literals. 10 We will call such rules canonical, and will often write (3) in the form

where BT is D0 BD BN BM BM BM BN D0 CZ , BU is D0 CZB7BD BN BM BM BM BN D0 D1 , and BY is

We will sometimes identify BT with the set CUD0 BD BN BM BM BM BN D0 CZ CV and BU with the set CUD0 CZB7BD BN BM BM BM BN D0 D1 CV.

A canonical program is a set of rules of the form (3).

The definition of satisfaction given in Section 2.1 is extended to canonical programs as follows. We say that a set CG of literals satisfies the body BUBN BY of rule (4) if D0 CZB7BD BN BM BM BM BN D0 D1 BE CG, D0 D1B7BD BN BM BM BM BN D0 D2 BPBE CG, and D0 D2B7BD BN BM BM BM BN D0 D4 BE CG. CG satisfies a program if, for every rule (4) of that program, at least one of the literals in BT belongs to CG whenever CG satisfies BUBN BY .

The reduct A5 CG of a canonical programA5 with respect to a set CG of literals is obtained from A5 by deleting each rule (4) such that CG BICYBP BY, and replacing each remaining rule (4) by BT AW BU. A consistent set CG of literals is an answer set for A5 if CG is minimal among the sets of literals that satisfy A5 CG .

Given a canonical program A5 and a set CG of literals, we will say that a set CH of literals is externally supported by A5 w.r.t. CG if there is a rule (4) in A5 such that BT CK CH BIBP BN, CG CYBP BUBN BY, BU CK CH BP BN, and CG CK B4BT D2 CH B5 BP BN. The last condition is suggested by the extension of the definition of a supported set to disjunctive programs proposed in [Baral and Gelfond, 1994] and [Inoue and Sakama, 1998].

The definition of a positive dependency graph is extended to the general case straightforwardly: for each rule (3) in A5, the edges of the graph go from each literal D0 CX (BC BO CX AK CZ) to each literal D0 CY (CZ BO CY AKD1). The definition of a loop from Section 2.1 remains the same for arbitrary finite programs.

The theorem from Section 2.1 remains true if we replace "nondisjunctive" in its statement with "canonical."

For example, let A5 BF be the program

which has two answer sets: CUD4BN D5CV and CUD6CV. The comments about these answer sets at the end of Section 2.2 apply to programA5 BF as well.

10 Any program with nested expressions can be turned into an equivalent program whose rules have the form (3), or equivalently D0 BD BN BM BM BM BN D0 CZ BN not D0 D2B7BD BN BM BM BM BN not D0 D4 AW D0 CZB7BD BN BM BM BM BN D0 D1 BN not D0 D1B7BD BN BM BM BM BN not D0 D2 [Lifschitz et al., 1999, Proposition 6 B4CXCXCXB5 ]. In Section 5, the main theorem is extended to arbitrary rules with nested expressions.

2.3 Extension to Infinite Programs

So far we restricted our attention to finite programs only. Indeed, unless we modify the definition of a loop, the theorem in Section 2.1 does not hold for infinite programs: conditions B4CPB5 and B4CQB5 are equivalent to each other even for infinite programs, but condition B4 B5 turns out weaker than the others. For example, consider the following infinite programA5 BG :

where each D4 CX is an atom. The program has no loops (in the sense of Section 2.1) other than singletons. Besides BN, which is the only answer set for A5 BG , there is one more set that satisfies condition B4 B5: CUD4 BD BN D4 BE BN BM BM BM CV.

Looking at the example, we observe that condition B4 B5 is weaker than condition B4CQB5 in that it does not account for infinite paths in the positive dependency graph which do not correspond to loops, while condition B4CQB5 tells us that the sets that correspond to such infinite paths should also be externally supported. We propose to modify the definition of a loop as follows.

Given a (possibly infinite) program A5 and a set  of literals, we say that  is unbounded if, for every literal D0 BE , there exists an infinite path in  in the positive dependency graph of A5 that starts from D0 and does not visit the same vertex more than once. A nonempty set  of literals is called a loop of A5 if  is unbounded, or for every pair D0 BD , D0 BE of literals in , there exists a path from D0 BD to D0 BE in the positive dependency graph of A5 such that all vertices in this path belong to . When A5 is finite, no set of literals that occur in A5 is unbounded, so that this definition of a loop reduces to the earlier definition.

In program A5 BG above, every set CUD4 CX BN D4 CXB7BD BN BM BM BM CV B4CX BQ BCB5 is a loop according to this definition, since it is unbounded. But it is not externally supported by A5 BG w.r.t. CUD4 BD BN D4 BE BN BM BM BM CV.

The theorem from Section 2.1 remains true if we replace "finite nondisjunctive" with "canonical":

2.4 Tight Programs

The notion of a loop helps us simplify the definition of a "tight" program [Erdem and Lifschitz, 2003]. Let A5 be any canonical program. We will say that a loop of A5 is trivial if the loop consists of a single literal such that the positive dependency graph of A5 does not contain an edge from the literal to itself. For example, in programA5 BG above, every singleton loop is trivial, while every loop CUD4 CX BN D4 CXB7BD BN BM BM BM CV B4CX BQ BCB5 is not. We say that A5 is absolutely tight if every loop of A5 is trivial. Let A5 CG be the set of rules of A5 whose heads and bodies are satisfied by CG. ProgramA5 is tight on a set CG of literals if the subgraph of the positive dependency graph of A5 CG induced by CG has no loops other than trivial ones. These definitions are more general than the corresponding definitions in [Lee and Lifschitz, 2003] in that they are applicable to infinite programs and to programs with classical negation as well. We get the following corollaries to the main theorem, which generalizes Propositions 2 and 4 from [Lee and Lifschitz, 2003].

Corollary 1 For any absolutely tight canonical program A5 and any consistent set CG of literals, CG is an answer set for A5 iff CG satisfies A5 and CG is supported by A5.

Corollary 2 For any canonical program A5 and any consistent set CG of literals such that A5 is tight on CG, CG is an answer set for A5 iff CG satisfies A5 and CG is supported by A5.

3 Translating Logic Programs into Propositional Logic

In application to finite programs without classical negation, conditions B4CQB5 and B4 B5 of the main theorem suggest ways to turn a program into an equivalent propositional theory. This translation is closely related to the Lin/Zhao theorem on loop formulas, as we will see in Section 4.

On the other hand, condition B4 B5 of the main theorem suggests the propositional theory CC B4A5B5, which consists of

Consider a finite program A5 whose rules have the form (4) where all D0 CX are atoms. For any set CH of atoms, the external support formula for CH is the disjunction of the conjunctions BU CM BY CM CM D4BEBTD2CH BMD4 (5) for all rules (4) of A5 such that BT CK CH BIBP BN, and BU CK CH BP BN. We will denote the external support formula by ES A5BNCH . Condition B4CQB5 of the main theorem suggests the propositional theory CC CQ B4A5B5 which consists of B4CXB5 the implications 11 BU CM BY AR BT (6) for all rules (4) in A5, and B4CXCXB5 the implications CF D4BECH D4 AR ES A5BNCH for all sets CH of atoms that occur in A5.

• B4CXB5 the implications (6) for all rules (4) in A5, and
• B4CXCXB5 the implications

for all loops  of A5.

D4 AR ES A5BN

Formula (7) is called the conjunctive loop formula of .

Corollary 3 For any finite program A5 without classical negation and any set CG of atoms, CG is an answer set for A5 iff CG is a model of CC CQ B4A5B5 iff CG is a model of CC B4A5B5.

Note that the number of loops is exponential in the worst case. But we cannot do much about this: Lifschitz and Razborov [2004] showed that any equivalent translation from logic programs to propositional formulas involves a significant increase in size assuming a conjecture from the theory of computational complexity which is widely believed to be true.

4 Unfounded Sets and Disjunctive Loop Formulas

Since conditions B4CQB5 and B4 B5 in the statement of the main theorem are equivalent to each other, any intermediate condition between the two also characterizes answer sets. In this section, we study two such conditions related to some earlier work.

11 We identify 'not' with 'BM', 'BN' with 'CM', and 'BN' with 'CN'.

4.1 Relation to Unfounded Sets

The first condition is

• B4CSB5 CG satisfies A5, and every nonempty subset of CG is externally supported by A5 w.r.t. CG.

Since B4CQB5 implies B4CSB5, B4CSB5 implies B4 B5, and B4CPB5,B4CQB5,B4 B5 are equivalent to each other, it is clear that all these conditions are equivalent to each other.

In fact, the equivalence between conditions B4CPB5 and B4CSB5 was established before for the special case when the rules of the program have the form (3) with D4 BP D2. It is related to the notion of an unfounded set originally introduced in [Van Gelder et al., 1991] to characterize negative conclusions under the well-founded semantics. Sacc´a and Zaniolo [1990] showed that answer sets for a nondisjunctive program can be characterized in terms of unfounded sets. 12 Leone et al. [1997] extended the notion of an unfounded set and the theorem by Sacc´a and Zaniolo to disjunctive programs.

Their definition can be further extended to programs with rules of the form (4) as follows. A set CH of literals is unfounded by a programA5 w.r.t. a set CG of literals if, for each rule (4) inA5 such that BTCKCH BIBP BN, at least one of the following conditions holds: CG BICYBP BUBN BY, BUCKCH BIBP BN, orCGCKB4BTD2CH B5 BIBP BN.

It is easy to see that CH is not unfounded w.r.t. CG iff CH is externally supported w.r.t. CG in the sense of Section 2.2.

A set CG of literals is called unfounded-free if it does not have any nonempty subset that is unfounded w.r.t. CG. The equivalence between conditions B4CPB5 and B4CSB5 stated above can be reformulated as follows: CG is an answer set for A5 iff CG satisfies A5 and CG is unfounded-free. This is a generalization of Corollary 2 from [Sacc´a and Zaniolo, 1990] and Theorem 4.6 from [Leone et al., 1997] to programs with rules of the form (3).

For finite programs A5 without classical negation, condition B4CSB5 suggests the following translation CC CS into propositional logic, which consists of

• B4CXB5 the implications (6) for all rules (4) in A5, and
• B4CXCXB5 the implications (7) for all nonempty sets of atoms that occur in A5.

Note that CC CS B4A5B5 is a superset of CC B4A5B5. In B4CXCXB5,  is not empty. If it were, then the implication would be unsatisfiable.

Corollary 4 For any finite program without classical negation, a set of atoms is an answer set for A5 iff it is a model of CC CS B4A5B5.

4.2 Relation to Disjunctive Loop Formulas

Here is another condition intermediate between B4CQB5 and B4 B5:

• B4CTB5 CG satisfies A5, and, for every loop  AI CG, every set of literals that has a common element with  is externally supported by A5 w.r.t. CG.

Given a finite program A5 whose rules have the form (4) where all D0 CX are atoms, the propositional theory CC CT B4A5B5 consists of

12 Their theorem refers to "assumption sets" rather than "unfounded sets." But as the authors noted, the two notions coincide as far as the theorem is concerned.

• B4CXB5 the implications (6) for all rules (4) in A5, and
• B4CXCXB5 the implications

for all loops  of A5.

Formula (8) is called the disjunctive loop formula of .

Corollary 5 For any finite program A5 without classical negation, a set of atoms is an answer set for A5 iff it is a model of CC CT B4A5B5.

In fact, if A5 is nondisjunctive, (8) is essentially the loop formula defined by Lin and Zhao [2004]. In the rest of this section, we give a more precise description of the relationship between this special case of Corollary 5 and the Lin/Zhao theorem.

Note first that when A5 is nondisjunctive, CC CT B4A5B5 consists of

• B4CXB5 the implications

for all rules (2) in A5, and

• B4CXCXB5 the implications

for all loops  of A5.

We now review the Lin/Zhao theorem. The completion of the same programA5, CompB4A5B5, consists of the equivalences

for all atoms D0 BD that occur in A5.

By LFB4A5B5 we denote the set of the disjunctive loop formulas (10) for all non-trivial loops .

Implications (11) can be further broken into implications (9). In implications (12), every singleton set CUD0 BD CV is a loop. If the loop is non-trivial, then LFB4A5B5 contains the corresponding implication (10), which is stronger than (12). Consequently, in the presence of LFB4A5B5, implications (12) for all non-trivial loops CUD0 BD CV can be dropped. On the other hand, if CUD0 BD CV is trivial, then D0 BD BPBE BU, so that (12) coincides with (10) (where  BP CUD0 BD CV). To sum up, CompB4A5B5CJLFB4A5B5 can be equivalently rewritten as the set consisting of formulas (9), formulas (10) for trivial loops, and formulas (10) for non-trivial loops (they form LFB4A5B5). This set is exactly CC CT B4A5B5.

Theorem 1 [Lin and Zhao, 2004, Theorem 1] For any finite nondisjunctive program A5 without classical negation, a set of atoms is an answer set for A5 iff it is a model of CompB4A5B5 CJ LFB4A5B5. To see why CompB4A5B5 CJ LFB4A5B5 is equivalent to CC CT B4A5B5, observe first that CompB4A5B5 can be rewritten as the set of implications "right-to-left" AI CN D0 BD AWBUBNBY BE A5 BU CM BY AJ AR D0 BD BN (11) and "left-to-right" D0 BD AR CN D0 BD AWBUBNBY BE A5 BU CM BYBM (12)

5 Loop Formulas for Programs with Nested Expressions

Lifschitz et al.[1999] extended the answer set semantics to programs with nested expressions. "Formulas" defined in that paper allow negation as failure (D2D3D8), conjunction (BN) and disjunction (BN) to be nested arbitrarily. A program with nested expressions is a set of rules of which both heads and bodies are formulas. The following program A5 BH , for instance, is a program with nested expressions which is not in canonical form because the first rule has a disjunction in its body.

For the semantics of such programs, along with the definition of satisfaction, we refer the reader to Section 2 of [Erdo˘gan and Lifschitz, 2004]. Recall that an occurrence of a formula BY in a formula BZ is singular if the symbol before this occurrence is BM; otherwise, the occurrence is regular [Lifschitz et al., 1999]. For any formula BZ, by poslitB4BZB5 we denote the set of all literals having a regular occurrence in BZ that is not in the scope of negation as failure. For instance, poslitB4D4BN not D5BN B4not not D6BN BMD7B5B5 BP CUD4BN BMD7CV.

For a set CH of literals, by BY CH BR we denote the formula obtained from a formula BY by replacing all regular occurrences of literals fromCH that are not in the scope of negation as failure with BR; by A5 CH BR we denote the program obtained from a programA5 by the same substitution. In application to canonical programs, this operation is closely related to the concept of external support: Proposition 1 Let A5 be a canonical program, and CG a set of literals satisfying A5. For any set CH of literals, CH is externally supported by A5 w.r.t. CG iff CG does not satisfy A5 CH BR . For example, for program A5 BE in Section 2.1 we checked that CUD4BN D5CV is externally supported w.r.t. CUD4BN D5CV. On the other hand, the program B4A5 BE B5 CUD4BND5CV BR is BRAWBR BRAW not D6 D6 AW not D4BN

and we can check that CUD4BN D5CV does not satisfy the program, in accordance with Proposition 1.

Proposition 1 shows that the main theorem in Section 2.3 can be stated without mentioning external support: in conditions B4CQB5 and B4 B5, we can replace "CH is externally supported by A5 w.r.t. CG" with "CG does not satisfy A5 CH BR ." This fact can be used to generalize the main theorem to arbitrary programs.

First we need to generalize the definition of a positive dependency graph to programs with nested expressions. The positive dependency graph of a program A5 with nested expressions is the directed graph BZ such that

• AF its vertices are the literals occurring in A5, and
• AF its edges go from each literal in poslitB4HeadB5 to each literal in poslitB4BodyB5 for each rule Head AW Body of A5.

If A5 is canonical, this definition reduces to the earlier definition. The positive dependency graph of A5 BH is the same as the positive dependency graph of A5 BE as shown in Figure 1.

Once we define a positive dependency graph, the definition of a loop given in Section 2.3 remains the same for programs with nested expressions.

Main Theorem For any program A5 with nested expressions and any consistent set CG of literals, the following conditions are equivalent:

• B4CPB5 CG is an answer set for A5.
• B4CQB5 CG satisfies A5, and, for every set CH of literals that has a common element with CG, CG does not satisfy A5 CH BR .
• B4 B5 CG satisfies A5, and, for every loop  of A5 that is contained in CG, CG does not satisfy A5  BR .

The translations CC CQ through CC CT can be extended to finite programs A5 with nested expressions that do not contain classical negation. For instance, the extended theory CC CQ B4A5B5 consists of B4CXB5 the implications Body AR Head for all rules Head AW Body in A5, and B4CXCXB5 the implications CF D4BECH D4 AR BMA5 CH BR for all sets CH of atoms that occur in A5.

6 Conclusion

The following are the main contributions of this paper:

• AF We reformulated the definition of a loop formula so that loop formulas became a generalization of completion.
• AF We generalized the definition of a loop formula and the Lin/Zhao theorem to programs with nested expressions, not necessarily finite.
• AF We presented a model-theoretic account of loop formulas-the concept of an externally supported setand showed that loop formulas are related to assumption sets and to unfounded sets.

It is interesting to note that the computational methods used in DLV and in SAT-based answer set solvers are related to each other, in view of our main theorem: DLV uses condition B4CSB5 [Leone et al., 1997, Theorem 4.6] for finding answer sets for disjunctive programs, and ASSAT and CMODELS use condition B4CTB5 for nondisjunctive programs.

Acknowledgements

I am grateful to Vladimir Lifschitz and Fangzhen Lin for many useful discussions. Vladimir helped me develop the idea and improve the presentation significantly. I am also grateful to anonymous referees for their comments. Wolfgang Faber suggested that there may be a relationship between loop formulas and unfounded sets. Nicola Leone gave pointers to earlier work on unfounded sets and on assumption sets. This work was partially supported by NSF under Grant IIS-0412907.