On the Equivalence between Answer Sets and Models of Completion for Nested Logic Programs

1 Introduction

We consider logic programs with nested expressions in the bodies of rules , called nested logic programs in this paper. Nested expressions are formulas built from literals (atoms with or without classic negation), connectives such as nega­ tion as failure not, disjunction";", and conjunction",". This is a proper subset of the class of programs considered in [Lif­ schitz et al., 1999], where the head of a rule can also be an arbitrary formula. Lloyd and Topor [Lloyd and Topor, 1984] defined nested logic programs without negation as failure, and argued for the higher expressive power of the extended language, while Lifschitz et al. further showed the role of negation as failure in nested logic programs.

Our goal in this paper is to provide a characterization of answer sets for nested logic programs in terms of tightness on the one hand, and to use an answer set generator, such as Smodels or DLV to compute answer sets for nested logic programs on the other. The studies on characterizations of answer sets have proved useful in relating the completion se­ mantics [Clark, 1978] with the answer set semantics [Gel­ fond and Lifschitz, 1988]. Fages [Fages, 1994] defined a syntactic condition on logic programs, called positive-order­ consistent, which guarantees the equivalence of the two se­ mantics. Positive-order-consistent requires a program to have no positive loops. For example, the program {a ~ a} is not positive-order-consistent. Babovich et al. [Babovich et al., 2000] on the other hand formalized the notion, tight on a set, which says that an extended logic program II is tight on X if

Mingyi Zhang

Guizhou Academy of Sciences P.R. China

there exists a level mapping >. from X to ordinals, such that for any rule

Erdem and Lifschitz [Erdem and Lifschitz, to appear] ex­ tended the work to nested logic programs, and weakened the condition so that the positive literals are required to be or­ dered by >. only for applicable rules w.r.t. X.

As shown in [Babovich et al., 2000; Erdem and Lifschitz, to appear], that a program is tight on S is a sufficient con­ dition for the equivalence of S being an answer set and S satisfying the completion of the program. However, there are simple programs that are not tight even on their answer sets. For example, suppose we want to express that two or more propositions are equivalent, and they are true if certain condi­ tions are satisfied. For instance, consider

Clearly, II is not tight on its unique answer set {a , b}. Any level mapping >. that maps the domain {a, b} to non-negative integers will have to satisfy >.(a) > >.(b), as well as >.(b) > >.(a), which is impossible.

Even for logic programs without negation as failure, tight­ ness may fail to apply, e.g., with II= {a~ . a~ a.}, II is not tight on its unique answer set {a}.

In this paper, we define the notion of weak tightness, which is a sufficient as well as a necessary condition for a model of completion to be an answer set. Consequently, an answer set is characterized by three independent properties: weak tight­ ness, supportedness, and closedness. This characterization of answer sets can be generalized to nested programs via a lin­ ear time transformation to extended programs. This yields a new characterization of answer sets for nested programs. Al­ though the transformation uses a linear number of extra vari­ ables, we will see that these extra variables are non-split, in the sense that in a Davis-Putnam procedure [Davis and Put­ nam, 1960], they need not create choice points during search for answer sets, and thus they need not enlarge the search space.

Our results have some practical implications. First, they widen the application range of systems like Cmodels

[Babovich, 2002], a system implemented for the computa­ tion of answer sets for tight logic programs. Secondly, the transformation from nested programs to extended programs allows answer sets for nested programs to be computed by an answer set generator for extended programs, or indirectly via the models of their completed programs.

The next section introduces logic programs with nested ex­ pressions. In Section 3 we define weak tightness and show that answer sets are characterized by this condition along with models of completion. In Section 4 we present a polynomial time transformation from nested programs to extended pro­ grams. Section 5 remarks on related work.

2 Nested Logic Programs

We consider a propositional language L. A literal is an atom, or an atom with the sign -, in front, called the classi­ cal negation. Elementary formulas are literals and constants T ("true") and ..l ("false"). Formulas are built from elemen­ tary formulas using the unary connective not and the binary connectives, (conjunction) and; (disjunction). A nested logic program (or, just program if not otherwise specified) is a set of rules of the form

where H is a literal or ..l, and G is a formula. H is called the head of the rule and G the body. If G = T, we will drop it from the body; rules with the body Tare called facts .

Here are some special cases. A formula of the form not ¢, where ¢ is a literal, is called a default negation. When G is a conjunction of literals and default negations, the rule is called an extended rule. In an extended rule, the literals that do not appear in the scope of not are called positive literals. The programs that consist of only extended rules are called ex­ tended programs; and extended logic programs without clas­ sic negation are called normal programs.

An extended rule may be denoted by H +- B+ , B-, where B+ is the set of positive literals and B- the set of default negations.

We denote by lit(<I>) the set of literals occurring in if>, where if> is any syntactic entity, such as a formula or a pro­ gram. Let X be a set of literals. Xw denotes the subset of X, restricted to the literals in V, i.e., X1 v = X n V. A set of elementary formulas X is consistent if ..l ~ X and it contains no complementary literals land-,[,

That a consistent set of literals X satisfies a formula F, denoted X f= F, is defined recursively as follows:

• for elementary formula F, X f= F ifF E X or F = T
• X f= not F if X IF F
• X f= (F, G) if X f= F and X f= G
• X f= (F; G) if X f= For X f= G

A consistent set X of literals is closed under a program II if, for every rule H +-Gin II, HE X whenever X f= G. X is supported by II if, for any l E X there is a rule l +- G such that X f= G.

We now define answer sets for a program. For a program II without negation as failure, a consistent set of literals X is an answer set for II if and only if X is minimal among the consistent sets of literals closed under II.

A consistent set of literals X is an answer set of program II if and only if X is minimal among the consistent sets of literals closed under II x, where the reduct II x is obtained from II by replacing every maximal occurrence of a formula not F by ..l if X f= F and T otherwise.

We define the completion semantics for finite nested pro­ grams without the classic negation. Let II be such a program. The completion of II, denoted C omp(II), is the following set of propositional formulas: for each atom¢ which is either an atom in L , or ..l,

• if¢ does not appear as the head of any rule in II, then ¢ := ..l E Comp(II);
• otherwise,¢= Body1 V .. . V Bodyn E Comp(II) (with each default negation not ~ replaced by negative literal ·~), if there are exactly n rules ¢ +- Bodyi E II with ¢ as the head.

Finally, given a nested program II without negation as fail­ ure, to construct the unique minimal set among the consistent sets of literals closed under II, we define the familiar Tn op­ erator as

It is clear that Tn is monotonic over the domain of sets of literals. The least fixpoint can then be computed by

The following proposition is needed later in this paper.

Proposition 2.1 Let II be a program without negation as fail­ ure. Then, X is an answer set for II iff X is consistent and X= Tnt oo.

3 Weakly Tight Logic Programs

Let II be an extended program, X a set of literals, and h a literal in X. We define the set of applicable rules of II, with respect to h and X, as follows;

A level mapping >.is a partial function from literals to nat­ ural numbers such that the set N of natural numbers mapped from literals forms a partial order (N, >). 1

Definition 3.1 Let X be a set of literals and II an extended program. II is said to be weakly tight on X if there ex­ ists a level mapping >. with the domain X such that for any nonempty II(h, X) where h E X, there is a rule h +­ Body+, Body- in II(h, X) such that for each b E Body+, >.(h) > >.(b).

Example 3.2 Let program II = {a +- b. b +- a. b +­ c, not d. c +- . }. Then, S = {a, b, c} is the only answer set for II. Though II is not tight on S, II is weakly tight on S. For example, a level mapping>. satisfying the weak tightness condition can be: >.(a)= 3, >.(b)= 2, >.(c)= 1.

1 By a partial order, we mean a relation that is transitive and ir­ reflexive.

Lemma 3.3 Let II be an extended program, and San answer set for II. Then II is weakly tight on S.

Proof Since Sis an answer set for II, S = Tns too. It can be seen that the following mapping >. exists: for each literal q such that q E Trrs t n but q !f. Tns t n- 1, let >.(q) = n. Clearly, >. satisfies the condition for weak tightness. 0

Theorem 3.4 For any extended program II and any consis­ tent set of literals S, S is an answer set for II iff II is weakly tight on S, and S is closed under and supported by II.

Proof ( =>) Let S be an answer set for II. Then T rr s t oo = S. It's obvious that S is closed under and supported by II. From Lemma 3.3 we know that II is also weakly tight on S.

( <=) Assume II is weakly tight on S, and S is closed under and supported by II. We show that S is an answer set for II. Let M = Tns t oo. The condition that S is closed implies M ~ S. We are done if M = S. Otherwise we have M c S. Let q E S\M. Since S is supported by II, there is a rule r : q +-- Body+, Body- in II such that q +-- Body+ E II 5 and Body+ ~ S. Thus, the same ruler is in II(q, S), which is nonempty. As II is weakly tight on S, there is a mapping >.and a rule q +-- Body'+, Body'- in II(q, S) such that q +­ Body'+ E II 5 and >.(q) > >.(b) for each b E Body+. Since M is also closed, there is b E Body+ such that b E S\M. Then, from the definition of>., there is a literal p E S\M such that >.(p) is minimal, hence p E T ns t 1. This contradicts the assumption that M is the least fix point of the operator T ns. 0

Note that neither supportedness nor closedness can be re­ moved from the theorem for it still to hold. E.g. the program II = {a +-- b} is tight as well as weakly tight on {a, b}, which is not supported by II. For closedness, we note that any program is tight as well as weakly tight on the empty set.

Corollary 3.5 Let II be a finite normal program and Sa set of atoms satisfying Comp(II). Then, II is weakly tight on S iff S is an answer set for II.

To compare two conditions that guarantee a model of com­ pletion to be an answer set, we have the following definition.

Definition 3.6 Let Condl(X, Y) and Cond2(X, Y) be con­ ditions where X ranges over the set of all extended programs andY over the set of all sets of literals. Condl(X, Y) is said to be weaker than Cond2(X, Y) if

• for all X andY, Cond2(X, Y) implies Condl(X, Y), and
• there exist some X andY such that Condl(X, Y) does not imply Cond2(X, Y).

Proposition 3.7 For any extended program II and set of lit­ erals X, if II is tight on X then it is weakly tight on X. But the converse is not true.

In Section 5, we will see that weak tightness is also weaker than other conditions used to characterize answer sets in the literature. Then, the question arises as whether the weak tightness condition is the weakest. Technically, the answer is no, since the weak tightness condition can be made weaker in trivial ways, e.g., one can make it weaker by not requiring a level mapping to be applied to a rule with a body literal that does not appear in the head of any rule.

4 Transformation

When a program II is translated to another program II', new propositional symbols may be used. Thus, the language for II' is enlarged. Below, we define a notion of equivalence be­ tween a program and its translation. Throughout this section, a program means a finite nested program.

Definition 4.1 Let II be a program in language L. Suppose the language L' for II' is a superset of L. II' is equivalent to II, denoted II ~ II', if and only if both of the following statements hold.

• For any answer setS for II, there is exactly one answer setS' for II' such that srL = s.
• For any answer setS' for II', Sk is an answer set for II.

Lemma 4.2 The relation ~ is reflexive and transitive.

Our transformation makes use of some transformations in [Lifschitz et al., 1999] that preserve strong equivalence. Two programs II1 and II2 are said to be strongly equivalent if for any program P, II1 UP and II2 UP have the same set of answer sets. Strong equivalence entails our notion of equiva­ lence.

Proposition 4.3 If two programs II1 and II2 are strongly equivalent, then they are equivalent to each other, i.e., II1 C II2 and II2 ~ II1.

4.1 Transformation

In the following, we say that a formula is basic if it is built from ";", ",", literals, constants, and not L and not not L where L is a literal or constant. A program is said to be basic if it consists of rules whose body formulas are basic. A rule

is said to be fiat if every Gi is a conjunction of literals and default negations. A program is fiat if every rule in it is flat.

Let II be a nested program. Our transformation consists of three steps, briefly described below.

• II is transformed to a basic program II' by some simpli­ fication rules.
• II' is transformed to a flat program II" by transformation rules that name some subexpressions by new atoms.
• II" is then transformed to II'" by splitting each flat rule with disjunctive body into several extended rules with the same head.

We now give the details. Below, F => R denotes a rewrite rule.

Step 1. Simplification

1. not (F; G) => not F, not G
2. not (F, G) => not F; not G
3. not not not F =>not F

1. F, T =? F (and its symmetric case, T, F =? F; the same for all rewrite rules below)
2. F; T =? T

6. F, .l =? .l

1. F; .l =? F
2. p, ·p :::} .l
3. not p; not ·P =? T

where Rule 3 has higher priority to be applied than Rules 1 and 2. D

The simplification rules given here are essentially their cor­ responding equivalences given in [Lifschitz et at., 1999]. The only difference is that, for the purpose of termination, we cannot directly adopt an equivalence for symmetry, such as F, G ¢:? G, F, as a rewrite rule. We therefore have to repre­ sent the symmetric cases by rules.

The simplification rules are similar to the ones found in propositional logic, except perhaps Rule 3, which simplifies negation as failure only when it is nested at least three lev­ els deep. Among these rules, only 1-3 are essential for the purpose of producing a basic program. The rest are used to simplify basic formulas further.

That a rule has a higher priority to be applied than another rule means that when both rules are applicable, the former should be applied and the latter should not. The only intention here for Rule 3 over Rules 1 and 2 is to prevent transforming an expression of the form

where n > 2, by distributing each not over F (which would result in higher complexity).

Step 2. Naming subexpressions

• (a) F, (G; H) =? F, ¢ and add the rule¢+- G; H where¢ is a new atom. 2

(b) (G;H),F =? ¢,F

and add the rule¢+- G; H where¢ is a new atom.

• (c) not not p =? not¢ and add the rule ¢ +- not p where ¢ is a new atom. D

Step 3. Splitting

A fiat rule of form H +- G1 ; .. . ; Gn is replaced by rules

The set of all transformation rules in Steps 1, 2 and 3 de­ fine a binary relation over programs. We will use II >-; II' to denote a single transformation step that transforms program II to program II' by an application of a transformation rule in Step i where i E [1..3]. By a rewrite sequence, we mean a se­ quence of zero or more rewrite steps which takes the general form

2 Apparently, in this case all the occurrences of ( G; H) in the given program can be replaced by ¢> simultaneously.

A program II is called an w;-normalform if II cannot be re­ duced further by transformation rules in Step i where i E [1..3] . In addition, we denote by

a rewrite sequence generated only by the transformation rules in Step i.

Example 4.4 Suppose II contains a single rule

II is an w1-normal form. We can have II >- 2 II' where II' = {a+- ~' not d. ~+-not not b; c.}, and II' >- 2 II" where II" = {a +- ~' not d. ~ +- not ry; c. 'fJ +- not b.}. Finally, II" >- 3 II"' where II"' = {a +- ~' not d. ~ +­ notry. ~+-c. ry+-notb.}.

Lemma 4.5 There is no infinite sequence

where II0 is a nested program when i = 1, II0 is an w1 - normal form when i = 2, and II0 is an w2 -normalform when i = 3,

Lemma 4.6 Let n be the size of the program II0 mentioned below.

1. For any nested program II0, and any rewrite sequence Ilo >-1 ... >-1 IIm where IIm is an w1-normalform, IIm is a basic program, and m is bounded by O(n).
2. For any w1 -normal form II0 , and any rewrite sequence Ilo >-2 ... >-2 IIm where IIm is an w2-normalform, IIm is a flat program, and m is bounded by O(n) .
3. For any w2 -normal form II0, and any rewrite sequence ITo >-3 ... >-3 IIm where IIm is an w3-normalform, IIm is an extended program, and m is bounded by O(n) .

We can show that every transformation in Step 2 preserves equivalence.

For any program II, Lemmas 4.5 and 4.6 together guaran­ tee the existence of a finite rewrite sequence

where II' is an w1-normal form, II" is an w2-normal form, and II"' is an extended program. Let us call such a II"' the transformation ofii, denoted by Tr(II). 3

We are ready to show the main theorem of this section.

Theorem 4.8 For any program II, II ~ Tr(II).

Proof Assume II >-i II' >-2 II" >-3 II 111 = Tr(II). From [Lifschitz et al., 1999], II and II' are strongly equiv­ alent, so are II" and II 111 · It follows that II ~ II' and II" ~ II"'. Lemma 4. 7 shows that every individual rewrite step in II' >-2 II" preserves equivalence. By transitivity (Lemma 4.2) we get II' ~ II", and therefore II ~ Tr(II). D

3 Although transformation rules can be applied nondeterrninisti­ cally, it is easy to show that the rewrite relation >-i for any i E (1..3] is confluent [Dershowitz and Jouannaud, 1990] so that the final ex­ tended program is unique, up to atom renaming.

Corollary 4.9 For any programs II and P,

1. II UP~ Tr(II) UP
2. II U P ~ Tr(II) U Tr(P), if the sets of new atoms, lit(Tr(II)) - lit(II) and lit(Tr(P)) - lit(P), are dis­ joint.

The claim in 1 above is considered by some authors as a form of strong equivalence within the same language.

It follows from Lemma 4.6 that

Theorem 4.10 For any program II, there is a linear time re­ duction of II to an extended program II' so that the answer sets for II can be identified in linear time from those for II'.

We remark that the extra atoms introduced in our transfor­ mation are non-split. They are just "connecting atoms" serv­ ing the purpose of propagating values from subexpressions. Their values can be determined solely by constraint propaga­ tion from the values of the original atoms.

Non-split variables can be accommodated easily in systems like Smodels by applying the procedure Heuristic only to the set of original variables, so that non-split variables will not be picked up for guessing a value. In this way, non-split vari­ ables do not create choice points during the search for answer sets.

4.2 Weakly tight nested logic programs

We give a characterization of answer sets for nested pro­ grams, in terms of their transformations, and show the coun­ terpart of Theorem 3.4 for nested programs.

Definition 4.11 Let II be a nested program and Tr(II) its transformation. Let X ~ lit(II) and V satisfy

Then, II is said to be weakly tight on X if and only ifTr(II) is weakly tight on X U V.

Theorem 4.12 Let II be a nested program, and X a consis­ tent set of literals. X is an answer set for II iff II is weakly tight on X, and X is closed under and supported by II.

Corollary 4.13 Let II be a finite nested program without the classic negation and Sa set of atoms satisfying Comp(II). Then, II is weakly tight on S iff S is an answer set for II.

5 Related Work

Well-Supported Model

Definition 5.1 [Fages, 1991] Let II be a normal program. A set of atoms S is well-supported iff there exists a level map­ ping >. with S as the domain such that for any atom a E S there exists a rule a +- Body+, Body- E II, which is appli­ cable w.r.t. S, andforeachp E Body+, >.(a)> >.(p).

Ben-Eliyahu and Dechter's characterization [Ben-Eliyahu and Dechter, 1994] of answer sets for head cycle-free disjunc­ tive programs reduces to that of Fages for normal programs.

Theorem 5.2 [Fages, 1991] For any normal program II, the well-supported models ofii are exactly the answer sets for II.

The level mapping in Fages' definition depends on the sup­ portedness: one needs to find a rule that supports an atom, and then determines if a level mapping applies to the same rule. The two conditions in our case are independent.

Example5.3 Letii ={a+- b; b +- c}, andS = {a,b,c}. Note that S is a model of II. II is weakly tight (as well as tight) on S, since we can assign a level mapping as: >.(a) = 2, >.(b) = 1, and>.( c) = 0. ButS is not well-supported by II.

To summarize the relationships among tightness, weak tightness and well-supportedness for normal programs, we have, for any normal program II and set of atoms S,

• If S is well-supported, then II is weakly tight on S; but the converse is not true.
• If II is tight on S, then II is weakly tight on S; but the converse is not true.
• That II is tight on S is not a sufficient condition for S to be well-supported; that S is well-supported is not a sufficient condition for II to be tight on S.

Therefore, the weak tightness is the weakest among all three, bridging the gap between tightness and well-supportedness.

Strong Compatibility of Logic Programs

In [Zhang, 1992], Zhang showed a cbaracterization of default extensions. Here, we re-formulate it for logic programs. For an extended logic program II, let us define

A subprogram II' ~ II is said to be compatible (w.r.t. II) if Con(II') U Just(II') is consistent and ..l rf. Con(II').

The characterization of default extensions as given in [Zhang, 1992], when applied to logic programs, can be stated as follows.

Theorem 5.4 Let II be an extended logic program. II has an answer set iff there is a subprogram II' ~ II such that

P 1. II' is compatible,

P2. A(II') = II', and

A subprogram II' ~ TI is said to be strongly compatible if it is compatible and A(TI') = TI'. We can show the following relationship.

Proposition 5.5 Let TI be an extended program. For any II'~ n,

1. if II' is strongly compatible, then II is weakly tight on Con(II');
2. II is weakly tight on Con(II'), and Con(II') is closed under and supported by II, if! II' is strongly compatible and satisfies P3 as well.

Since no proper subset of { Pl, P2, P3} corresponds to the satisfaction of completion, to see whether a model of comple­ tion is also an answer set one needs all three conditions. The key lies in condition P2 which embodies both supportedness and an order of derivation. Thus, Zhang's characterization does not provide a nontrivial condition for a model of com­ pletion to be an answer set.

Note that P2 alone does not imply weak tightness. For example, with II = {a +-- a; a +-- not a}, we have A(II) = II. But II is not weakly tight on C on(II) = {a}, due to the fact that a +-- a is the only applicable rule w.r.t. {a}.

ASS AT

In the system ASSAT [Lin and Zhou, 2002], the comple­ tion of a normal program is executed by a SAT solver, pos­ sibly repeatedly. When a model M of the completion from program II is generated, if M f; II M then M is not an answer set for II. ASSAT relies on M- IIM to compute loop for­ mulas which say tha~ the atoms in M - II M that are involved in a (maximal) loop should be false if they cannot be derived otherwise. However, M- IIM does not provide a complete picture of the loops involved. There could be loops whose in­ terpretation in M is faked due to the loops on M - II M. For example, let II = { c +-- c. c +-- not b. b +-- not a. a +-- a}, and let the computed model of completion be M = {a, c}. In this case, M - II M = {a}. Though the loop on a is captured correctly, the loop on c is captured incorrectly. It remains to be seen whether stronger loop formulas can be computed, based on the idea of level mapping.

Transformations of Nested Programs

The transformation given in [Lifschitz et al., 1999] deals with arbitrary nested programs where rules may have arbi­ trary formulas in the heads. The transformation preserves strong equivalence but is not polynomial.

Independently in [Pearce et al., 2002], arbitrary nested pro­ grams are translated to disjunctive programs where extra vari­ ables are used to avoid an exponential blow-up, an idea simi­ lar to the one adopted in this paper. Our transformation how­ ever departs from that of [Lifschitz et al., 1999] in a mini­ mal way. By partitioning the transformation into three stages (cf. Theorem 4.8), we are able to identify exactly where ex­ tra variables are required. This is only when dealing with a disjunction or an expression like not not L where L is a literal. In [Pearce et al., 2002], other forms of subformu­ las, such as the whole body of a rule and a conjunction, can also be labeled by extra variables. Our transformation is thus simpler and more compact. While our transformation takes linear time, the one in [Pearce et al., 2002] is only claimed to be polynomial time. Finally, the extra variables introduced in our case are non-split. It is not clear whether this is pos­ sible for the class of all nested programs where the heads of rules are arbitrary formulas. It is interesting to see whether our approach, combined with some of the ideas in [Pearce et a!., 2002], can be extended in order to be able to handle all nested programs.