9512.net
甜梦文库
当前位置:首页 >> >>

Uniform Equivalence of Logic Programs under the Stable Model Semantics


In: Proc. 19th International Conference on Logic Programming (ICLP 2003), LNCS, c ? 2003 Springer.

Uniform Equivalence of Logic Programs under the Stable Model Semantics
Thomas Eiter and Michael Fink
Institut f¨ r Informationssysteme, Abt. Wissensbasierte Systeme, u Technische Universit¨ t Wien a Favoritenstra?e 9-11, A-1040 Vienna, Austria eiter,michael @kr.tuwien.ac.at

Abstract. In recent research on nonmonotonic logic programming, repeatedly strong equivalence of logic programs ? and ? has been considered, which holds if the programs ? ? and ? ? have the same stable models for any other program ?. This property strengthens equivalence of ? and ? with respect to stable models (which is the particular case for ? ), and has an application in program optimization. In this paper, we consider the more liberal notion of uniform equivalence, in which ? ranges only over the sets of facts rather than all sets of rules. This notion, which is well-known, is particularly useful for assessing whether programs ? and ? are equivalent as components in a logic program which is modularly structured. We provide semantical characterizations of uniform equivalence for disjunctive logic programs and some restricted classes, and analyze the computational cost of uniform equivalence in the propositional (ground) case. Our results, which naturally extend to answer set semantics, complement the results on strong equivalence of logic programs and pave the way for optimizations in answer set solvers as a tool for input-based problem solving.

Keywords: uniform equivalence, strong equivalence, stable models, answer set semantics, computational complexity, program optimization.

1 Introduction
In the last years, logic programming with non-monotonic negation, and in particular stable semantics, as a problem solving tool has received increasing attention, which led to application in several ?elds. To a great deal, this is due to the availability of several advanced implementations of the stable semantics such as smodels [18], DLV [11], or ASSAT [15]. In turn, the desire of more ef?cient stable models solvers has raised the need for sophisticated optimization methods by which logic programs can be simpli?ed and processed more ef?ciently. In this direction, properties of logic programs under the stable semantics have been investigated which may aid in optimization. A particular useful such property is strong equivalence [12, 23]: Two logic programs ? and ? are strongly equivalent, if by adding any set of rules to both ? and ? , the resulting programs ? and ? are equivalent under the stable semantics, i.e., have the same set of stable models. Thus, if a program contains a subprogram

?

?

? ?

? ?

?

?

?

?

This work was partially supported by the Austrian Science Fund (FWF) Project Z29-N04, and the European Commission projects FET-2001-37004 WASP and IST-2001-33570 INFOMIX.

particular if the resulting program is simpler to evaluate than the original one. However, strong equivalence is a very restrictive concept. As for optimization, it is not very sensitive to a modular structure of logic programs which naturally emerges by splitting them into layered components that receive input from lower layers by facts and in turn output facts to a higher layer [13, 5], nor to the usage of the same logic program to compute solutions over varying inputs given as sets of facts. In this paper, we study the more liberal notion of uniform equivalence [22, 16], which is better suited in this respect: Two logic programs ? and ? are uniformly equivalent, if by adding any set of facts to both ? and ? , the resulting programs and ? have the same set of stable models. Thus, a component within a ? program may be (of?ine) replaced by a uniformly equivalent set of rules ? , provided the global component structure of the program is not affected (a simple syntactic check). That strong equivalence and uniform equivalence are different concepts is illustrated by the following simple example.

? which is strongly equivalent to a program ??, then we may replace ? by ??, in

?

?

?

?

? ?

?

Example 1. Let and not strongly equivalent, since is not a stable model of are uniformly equivalent.

?

?

?

?

??? . Then and are has the stable model , which . However, it can be seen that and

???

?

?

?

?

Moreover, this holds even for programs without disjunction. Example 2. Let easily veri?ed that equivalent: For model of

?

? ??? and ? ??? . Then, it is ? and ? are uniformly equivalent. However, they are not strongly ? and ? , we have that ? is a stable but not of ? .

While strong equivalence of logic programs under stable semantics has been considered in a number of papers [3, 4, 14, 12, 19, 23, 24], to our knowledge uniform equivalence of has not been considered. Sagiv [22] has studied the property in the context of de?nite Horn datalog programs, where he showed decidability of uniform equivalence testing, which contrasts with the undecidability of equivalence testing for datalog programs. Maher [16] considered the property for de?nite general Horn programs, and reported undecidability. Moreover, both [22, 16] showed that uniform equivalence coincides for the respective programs with Herbrand logical equivalence. In this paper we focus on propositional logic programs (to which general programs reduce). Our main contributions are brie?y summarized as follows.
? We provide characterizations of uniform equivalence of logic programs. In particular, we use the concept of strong-equivalence models (SE-models) [23, 24] and thus give characterizations which appeal to classical models and the Gelfond-Lifschitz reduct [9, 10]. Our characterizations of uniform equivalence will elucidate the differences between strong and uniform equivalence in the examples above such that they immediately become apparent. ? For the ?nitary case, we provide a simple and appealing characterization of a logic program with respect to uniform equivalence in terms of its uniform equivalence models (UE models), which is a special class of SE-models. The associated notion of consequence can be fruitfully used to determine redundancies under uniform equivalence.

2

? We consider restricted subclasses, in particular positive programs, head-cycle free programs [1], and Horn programs, and consider the relationship between uniform and strong equivalence on them. ? We analyze the computational complexity of deciding uniform equivalence of two ? given programs and . We show that the problem is ? -complete in the general propositional case, and thus harder than deciding strong equivalence of and , which is in ??? [19, 24]. However, the complexity of testing uniform equivalence decreases on important fragments; in particular, it is ???-complete for positive and head-cycle free programs, while it is polynomial for Horn programs. In the nonground case, the complexity increases by an exponential for function-free programs. ? Finally, we address extensions to extended and to nested logic programs.

?

?

?

?

?

Our results complement the results on strong equivalence of logic programs, and pave the way for optimization of logic programs under stable negation by exploiting uniform equivalence. For space reasons, some proofs are omitted here (see [6] for an extended version).

2 Preliminaries
We deal with disjunctive logic programs, which allow the use of default negation ??? · ? ? ? ? ? , where ? ? in rules. A rule is a triple ? ? ? ? , ·? ? ?? ? and ?·? ? , ?·? ? , where ? ,? , are atoms from a ?rst-order language. Throughout, we use the traditional representation of a rule as an expression of the form

?

?

?

?? ?

?

?

??

? ? ?

We call ? ? the head of , and ? ? ??? ? ?·? ? the body of . If ? ? , then is a constraint. As usual, is a fact if ? ? , which is also represented by ? ? if it is nonempty, and by (falsity) otherwise. A rule is normal (or non-disjunctive), if ?; de?nite, if ?; and positive, if . A rule is Horn if it is normal and positive. A disjunctive logic program ? ?? ? is a (possibly in?nite) set of rules. A program is a normal logic program ???? ? (resp., de?nite, positive, or Horn), if all rules in are normal (resp., de?nite, positive, or Horn). Furthermore, a program is head-cycle free ?HCF? [1], if its dependency graph (which is de?ned as usual) has no directed cycle that contains two atoms belonging to the head of the same rule. In the rest of this paper, we focus on propositional programs over a set of atoms – programs with variables reduce to their ground (propositional) versions as usual. We recall the stable model semantics for ?? s [10, 21], which generalizes the stable model semantics for ??? s [9]. An interpretation , viewed as subset of , models the head of a rule , denoted ? ?, iff ? for some ? ? ?. It models · ? ? is true in , i.e., ? , and ( ) each ? ?, i.e., ? ? iff ( ) each ? ? ? ? is false in , i.e., ? . Furthermore, models rule , iff ? ? ? whenever ? ?, and , for a program , iff , for all ? . The reduct of a rule relative to a set of atoms , denoted ? , is the positive rule ? · ? ? if ? ? ? , and is void otherwise. such that ? ? ? ? ? and · ? ? ?

?? ? ??

?

?

?

?

? ? ? ?? ? ?

?·?

?

???

?·?

??? ? . ??? ?·?

?

?

? ? ?

?

?

?

? ? ? ??

? ? ? ?? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?? ? ? ? ?
3

?? ? ? ? ? ?

?? ?

? ?? ? The Gelfond-Lifschitz reduct ? , of a program , is ? ? and . An interpretation is a stable model of a program iff is a minimal model (under inclusion ) of ? . By ? ?? ? we denote the set of all stable models of . Equivalences. Several notions for equivalence of logic programs have been considered, cf. [12, 16, 22]. Under stable semantics, two ?? s and are regarded as equivalent, denoted , iff ? ?? ? ? ?? ?. The more restrictive forms of strong equivalence [12] and uniform equivalence [22, 16] are as follows.

?

?

? ?

? ? ? ? ? ? ? ? ?

? ?

?

? ?

?

?

De?nition 1. Let and be two ?? s, Then × , iff for any rule set , the and are strongly equivalent, denoted () programs and are equivalent, i.e., . ? , iff for any set of non( ) and are uniformly equivalent, denoted and are equivalent, i.e., . disjunctive facts , the programs

? ?

? ? ? ? ? ? ? ?

?

?

?

? ? ? ? ? ? ?

?

?

?

One of the main results of [12] is a semantical characterization of strong equivalence in terms of the non-classical logic HT. For characterizing strong equivalence in logic programming terms, Turner introduced the following notion of SE-models [23, 24]: De?nition 2. Let be a ?? , and let pair ? ? is an SE-model of , if set of all SE-models of .

?

?

?

? and

be sets of atoms such that . The . By ? ? ? we denote the

?

?

?? s ? and ?, ? × ? iff ? ?? ? ? ???. Example 3. Reconsider ? ??? and ? ??? . ? is in ? ?? ? but not in ? ???. Recall that ? ? ?. However, ? × ?, as ?
Proposition 1 ([23, 24]). For every

Strong equivalence can be characterized as follows.

3 Characterizations of Uniform Equivalence
After the preliminary de?nitions, we now turn to the issue of characterizing uniform equivalence between logic programs in model-theoretic terms. As restated above, strong equivalence can be captured by the notion of SE-model (equivalently, HT-model [12]) for a logic program. The weaker notion of uniform equivalence can be characterized in terms of SE-models as well, by imposing further conditions. We start with a seminal lemma, which allows us to derive simple characterizations of uniform equivalence. ? , iff for every Lemma 1. Two ?? s and are uniformly equivalent, i.e.

SE-model ? ?, such that ? ? is an SE-model of exactly one of the programs and , it holds that ( ) , and ( ) there exists an SE-model ? ?, , of the other program. ? . If neither models , nor , then Proof. For the only-if direction, suppose

?

?

?

?

?
?

? ?
? is

? ?

?

not an SE-model of any of the programs and . Without loss of generality, assume and . Then, since in this case and no strict subset of models , ? ? ?? ?, while ? ? ?? ?. This contradicts our ? . Hence, item ( ) must hold. assumption

?

?

? ?

?

?

?

?

?

? ? ?

?

?

4

To show ( ), assume ?rst that ? ? is an SE-model of but not of . In view of ( ), it is clear that must hold. Suppose now that for every set , , it holds that ? ? is not an SE-model of . Then, since no subset of models , ? ? is the only SE-model of of form ?? ?. Thus, ? ? ?? ? in this case, while ? ? ?? ? ( implies ? ? , so ? ? is an ? . Thus, it follows that for some ). However, this contradicts SE-model of such that ,? ? is an SE-model of . The argument in the case where ? ? is an SE-model of but not of is analogous. This proves item ( ). For the if direction, assume that ( ) and ( ) hold for every SE-model ? ? which is an SE-model of exactly one of and . Suppose that there exist sets of atoms and , such that w.l.o.g., ? ? ?? ? ? ? ?? ?. Since ? ? ?? ?, we , and, moreover, . Consequently, ? ? is an SE-model of have that ? . Since ? ? ?? ?, either ? ? , or there exists such that ? ? ? . Let us ?rst assume ? ? , then, since ? ? and , it follows that . This implies and hence, ? ? is not an SE-model ? is an SE-model of exactly one program, , but ? ? violates ( ) of . Thus, ? since ; this is a contradiction. ? ? ? must hold, and that there must exist such It follows that ? ? ? ? is an SE? . So we can conclude and that ? that ? must hold. So if ? ? ? model of but not of . To see the latter, note that were an SE-model of , then it would also be an SE-model of , contradicting the assumption that ? ? ?? ?. Again we get an SE-model, ? ? ?, of exactly one of the programs, in this case. Hence, according to ( ), there exists an SE-model ? ? , it follows that ? ? ? of , . However, because of ? is also an SE-model of , contradicting our assumption that ? ? ?? ?. This proves that, given ( ) and ( ) for every SE-model ? ? such that ? ? is an SE-model of exactly one of and , no sets of atoms and exists such that ? holds. is a stable model of exactly one of and . That is, ? ?

?

?

?

?

?

?

? ?

?

?

?

?

?

?

?

? ?

? ? ?

?

?

?

?

?

? ? ? ? ?

?

?

?

?

?

?

? ? ? ?

?

?

? ? ? ? ? ? ? ? ?

?

?

?

?

?

?

?

?

?

From Lemma 1 we immediately obtain the following characterization of uniform equivalence between logic programs. Theorem 1. Two () ( )
? ? ?

?? s, ? and ? are uniformly equivalent, ?

and ??? ??? . By Theorem 1, we can easily verify that and are uniformly equivalent: Their SEmodels differ only in ? ?, which is an SE-model of but not of . Thus, items ( ) and ( ) clearly hold for all other SE-models. Moreover, ? ? is an SE-model of , and thus item ( ) also holds for ? ?.

? Example 4. Reconsider the programs ? ?

?

is an SE-model of iff it is an SE-model of , and where , is an SE-model of (respectively ) iff there exists a set , such that , and ? ? is an SE-model of (respectively ).
?,

?

?

?

?

?

?, iff ?

?

?

?

? ?

?

?

Note that and are strongly equivalent after adding the constraint , which enforces exclusive disjunction. Uniform equivalence does not require such an addition. 5

?

?

? ?? ? for any programs ?

Example 5. Let

?

? and ? as in the previous example. Since ? ?? ? ? ? ??? and ? , the pair ? ? is no longer an SE-model of (because ). Hence, ? × ? . ? and ? are uniformly equivalent, i.e., ? ? ? ? ? ? ?
?

For ?nite programs, we can derive from Theorem 1 the following characterization of uniform equivalence. Theorem 2. Two ?nite ?? s following conditions hold:

?, iff the

() ? ? is an SE-model of iff it is an SE-model of for every , and ( ) for every SE-model ? ? ? ? ? ? ? ? ? such that , there exists an SE-model ? ? ? ? ? ? ? ? ? ?=? ? ?? such that .

?

? ? ?

?

Proof. Since ( ) holds by virtue of Theorem 1, we only need to show ( ). Assume ? ?, where , is in ? ? ? ? ? ?. ? ? ? ? ? ? ? ?, then the statement holds. Otherwise, by virtue of TheIf ? orem 1, there exists ? ? ?, , such that ? ? ? is in ? ? ? ? ? ?. ? By repeating this argument, we obtain a chain of SE-models ? ? ? ? ?, ? ? ?, . . . , ? ?, . . . such that ? ? ? ? ? ? ? ? ? and ·? , ?. Furthermore, we may choose for all ? such that ? coincides with on all atoms which do not occur in (and hence all , ?, do so). Since and are ?nite, it follows that ? and hence ·? must hold for some ? ? ? ? ? ? ? ? ? must hold. This proves the result. ? ?

? ?

?

?

?

?

? ?

? ?

?

?

? ? ? ? ? ?

?

?

?

?

? ? ? ? ? ?

Note that the previous theorem remains valid even if only one of and is ?nite. In the light of this result, we can capture uniform equivalence of ?nite programs by the notion of UE-model de?ned as follows.
? ? ? ? ? is a uniform De?nition 3 (UE-model). Let be a ?? . Then, any ? ? equivalence ?UE? model of , if for every ? ? ? ? ? ? ? it holds that implies ? . By ? ? ? we denote the set of all UE-models of .

?

?

?

?

?

?

?

?

That is, the UE-models comprise all SE-models of a ?? which correspond to classical models of (for ), plus all its maximal ’non-classical’ SE-models, ? ? ? ? ? ? ? ? ? ? ? ? ? ? , where i.e., ? ? ? ?? ? ?. ? ? ?? ? By means of UE-models, we then can characterize uniform equivalence of ?nite logic programs by the following simple condition.

?

?

?

?

Theorem 3. Two ?nite only if ? ? ? ? ?

? and ( ) ? ? ? ? ?? ? ? ???.

Proof. By Theorem 2 we have to show that Conditions ( ) ? ? , ?

? ? ? ? ? ? ? ? ? hold iff For the if direction assume ? ?? ? ? ???. Then ( ) holds by de?nition of ? be an SE-model of ? , such that . There are two UE-models. Now let ?

?

??.

?? s ? and ? are uniformly equivalent, i.e., ?

?

?, if and

?

?

6

possibilities: If ? ? is maximal, then ? ? ? ? ? ? as well and thus ( ) holds ( ); otherwise, ? ? is not maximal, which means that there exists some ? ? ? ? ? ? ? ? such that , and since ? ? ? ? ? ? Condition ? ). ( ) holds again ( ? . Then by Condition ( ) ? ? ? and ? ? ? For the only-if direction let coincide on models ? ?. Assume w.l.o.g. that ? ?, , is in ? ? ?, but not in ? ? ?. By ( ) there exists ? ?, , which is an SE-model of both and . Since contradicts ? ? ? ? ? ?, let , i.e., ? ? is an SE-model of as well, but it is not in ? ? ?. Hence, there exists ? ? ? ? ? ? ?, ? and by ( ) there exists ? ? ?, ? , which is an SE-model of . This again contradicts ? ? ? ? ? ?. Hence, ? ? ? ? ? ?. ? ?

?

?

? ?

?

?

?

? ?

?

?

? ?

?

?

?

?

?

?

? ? ?

?

? ?

?

?

?

This result shows that UE-models capture the notion of uniform equivalence, in the same manner as SE-models capture strong equivalence. That is, the essence of a program with respect to uniform equivalence is expressed by a semantic condition on alone.

?

?

Example 6. Each SE-model of the program satis?es the condition of an ??? ??? UE-model, and thus ? ? ? ? ? ?. The program has the additional SE-model ? ?, and all of its SE-models except this one are ? ? ? ? ? ? ? ? ? UE-models of . Thus, ? ? ? ? ?, ? ? . Note that the strong equivalence between and fails because ? ? is not an SE-model of . This SE-model is enforced by the intersection property ( ? ? ? and ? ? ? in ? ? ? implies ? ? ? ? ? ? ? ?) which the Horn program enjoys, which however is not satis?ed by the disjunctive program (= ). The maximality condition of UE-models eliminates this intersection property.

?

?

?

?

?

?

?

?

?

?

?

?

?

?

?

??? , which has classical models , Example 7. Reconsider . Its UE-models are of form ? ? where ? ? ? . Note that the atoms and have symmetric roles in ? ? ?. Consequently, the program obtained by exchanging the roles of and , ??? has the same UE models. Hence, and are uniformly equivalent.





?



?

?

?

?





Like Theorem 2, also Theorem 3 remains valid if only one of and is ?nite. However, the following example shows that it fails if both and are in?nite.

? . Furthermore, , while has the incomplete ?. Both and have the same maximal incomplete SE-models (namely none), and hence they have the same UE-models. ? , since e.g. has a stable model while has obviously not. Note However, that this is caught by our Theorem 1, item ( ): for ? ? ?, which is an SE-model of but not of , we cannot ?nd an SE-model ? ? of between ? ? ? and ? ?.

? and ? over ? ? and ? ??? Both ? and ? have the single classical model ? has no “incomplete” SE-model ? ? such that ? ?, where for SE-models ? ?
Example 8. Consider the programs

?

?

?

?

?

, de?ned by
?

·?

?

?

?

?

?

?

?

?

?

?

?

?

?

? ??

7

Based on UE-models, we de?ne an associated notion of consequence under uniform equivalence. Recall that ? ? models a rule iff and . De?nition 4 (UE-consequence). A rule, , is an UE-consequence of a program denoted ? for all ? ? ? ? ? ?. ? , if ?

?

Clearly, iff is a classical tautology. The next ? for all ? , and result shows that a program remains invariant under addition of UE-consequences. Proposition 2. For any ?nite program

?

?

?

? ?

?

?

?

?

?

? ?

?

?,

? and rule ?, if ? ? ?

?

? then ? ? ?

?

?

?. ?

? ? Proof. For the if-direction, we apply Prop. 2 repeatedly and obtain ? ? ? ? ? ?. For the only-if direction, we have ? ?? ? ? ??? if ? ? ? by Theorem 3, and thus ? and ? have the same UE-consequences. Since ? ? ? (resp. ? ? ?), for all ? ? ? ?? ? (resp. ? ? ? ???, it follows ? ? ? and ? ? ?. We note that with respect to uniform equivalence, every program ? has a canonical normal form, ? ? , given by its UE-consequences, i.e., ? ? ? ? ?? Clearly, ? ? ? holds for every program ? , and ? ? has exponential size. Applying optimization methods which build on UE-consequence, ? resp. ? ? may be transformed
? ? ? ?

From this proposition, we obtain an alternative characterization of uniform equivalence in terms of UE-consequence. As usual, we write ? for any set of rules if ? for all ? . ? iff Theorem 4. Let and be any ?nite ?? s. Then ? and ? .

?

?

? ? ? ?

? ?

? ? ? ? Proposition 3. For any ?nite program ? and rule ?, ( ) ? ? ? implies ? for each set of facts ; ( ) ? ?, for each set of facts , implies ? ?. ( )? ? implies ?

into smaller uniform equivalent programs; we leave this for further study. As for the relationship of UE-consequence to classical consequence and cautious consequence under stable semantics, we note the following hierarchy. Let denote consequence from the stable models, i.e., for every ? ? ?? ?. iff

?

?

, ; and

?

?

This hierarchy is strict, i.e., none of the implications holds in the converse direction. ??? ??? (For ( ), note that but ? , since the UE-model ? ? violates .) We next present a semantic characterization in terms of UE-models, under which UE-and classical consequence and thus all four notions of consequence coincide.
?i.e.,

? be a ?nite Theorem 5. Let ? be any ?nite ?? . Then the following conditions are equivalent: ( ) ? ? ? iff ? ?, for every rule ?. ? ? ?? ?, it holds that ?. ( ) For every ?
Lemma 3. Let
?

Lemma 2. Let be a ?nite ?? . Suppose that ? ? ? ? ? ? implies is a model of ?. Then, implies ? , for every rule .

?

?

? ? ? ? ? ?? . Then, ? ? ? implies ? ?, for every rule ?. ? ?

8

Proof. ( ) ? ( ) Follows immediately from Lemmas 2 and 3. ( ) ? ( ) Suppose , for every rule , but there exists some UE? iff model ? ? of such that . Hence for some rule ? . Let ? be the rule which results from by shifting the negative literals to the head, i.e., ? ? ?, · ? ? ? · ? ?, and ? ? ? ? ? . On the ? ?? ? ? . Then, ? . Moreover, ? . Hence, and thus other hand, ? implies ? ?? ? ? ? . This is a contradiction. It follows implies that ? ? , and hence that for each UE-model ? ? of . ? ?

? ??

?

?

? ?

?? ? ? ? ?

?

? ? ?

?

? ? ?

? ?

?

?

?

?

?

? ?

?

?

An immediate corollary to this result is that for ?nite positive programs, the notion of UE-consequence collapses with classical consequence, and hence uniform equivalence of ?nite positive programs amounts to classical equivalence. We shall obtain these results as corollaries of more general results in the next section, though.

4 Restricted Classes of Programs
After discussing uniform equivalence of general propositional programs, let us now consider two prominent subclasses of programs, namely positive and head-cycle free programs. 4.1 Positive programs While for programs with negation, strong equivalence and uniform equivalence are different, the notions coincide for positive programs, as shown next. ? iff × . Proposition 4. Let and be positive ?? s. Then

? ? ? Proof. The if-direction is immediate as ? × ? implies ? ? ?. For the only-if-direction, we show that if ? and ? are not strongly equivalent then ? and ? are not uniformly equivalent. To start with, observe that ? ? holds for any positive program ? and any set of literals . W.l.o.g., let ? ? be an SE-model of ? but not of ?. By de?nition of SE-model ? , i.e. ? . On the other hand, since ? ? is not SE-model of ?, we have either ( ) ? , i.e., ?, or ( ) ?. ( ) Consider the programs ? ? and ? ? . Clearly, ? and , ? ? ? . Hence, is an answer set of ? . On the other for each ? hand, ? and thus ? . Hence, cannot be an answer set of ? . ? and ? ? . Clearly, ? and ( ) Consider the programs ? for each ? , ? ? ? . Hence, is an answer set of ? . On the other hand, ? and thus ? . Hence, cannot be an answer set of ? . In any case we must conclude that ? and ? are not uniformly equivalent.
? ?

?

?

?

As known and easy to see from the main results of [12, 23, 24], on the class of positive programs classical equivalence and strong equivalence coincide. By combining this and the previous result, we obtain ? if and only if Theorem 6. Let and be positive ?? s. Then and

? ? ? ? ? ? , i.e., ? and ? have the same set of classical models.
9

? ?

Note that Sagiv [22] showed that uniform equivalence of datalog programs ? and ? ? is equivalent to equivalence of ? ? and ? over Herbrand models; this implies the above result for de?nite Horn programs. Maher [16] showed a generalization of Sagiv’s result for de?nite Horn logic programs with function symbols.

Example 9. Consider the positive programs . Their classical models are , , and . Hence, uniformly equivalent, and even strongly equivalent (due to Prop. 4).





?









and ? ? and ? are

4.2 Head-cycle free programs The class of head-cycle free programs generalizes the class of ??? s by permitting a restricted form of disjunction. Still, it is capable of expressing nondeterminism such as a guess for the value of an atom , which does not occur in the head of any other rule. As shown by Ben-Eliyahu and Dechter, each head-cycle free program can be rewritten to an ??? , obtained by shifting atoms from the head to the body, which has the same stable models. More formally, let us de?ne the following notation: De?nition 5. For any rule , let any

· ???

?? ? , let ?

? ??? ?

? ???

? ? ? ? ??? ??? ? .

?

?? ? ??? ? if ? ??? ?

and

? ?

?

? ??? · ??? ? ? otherwise. For ? ?
(cf.

It is well-known that for any head-cycle free program , it holds that [1]). This result can be strengthened to uniform equivalence. ? . Theorem 7. For any head-cycle free program , it holds that Proof. For any set of facts , it holds that ? is head-cycle free. Thus, ? ?

?

?

?

?

?

?

?

?

and that this program ? . Hence, . ? ?

?

?

We emphasize that a similar result for strong equivalence fails, as shown by the canonical counterexample in Example 1. Moreover, the program is not strongly equivalent to any ??? . Thus, we can not conclude without further consideration that a simple disjunctive “guessing clause” like the one in (such that and do not occur in other rule heads) can be replaced in a more complex program by the ??? and ??? ; addition of a further constraint unstrati?ed clauses is required. However, we can conclude this under uniform equivalence taking standard program splitting results into account [13, 5]. We close this section with the following result, which provides a characterization of arbitrary programs which are strongly equivalent to their shift variant. × if and only if for every disjunctive Theorem 8. Let be any ?? . Then,

?

?

rule ( )

Example 10. Reconsider . Then ??? ??? has the SE-model ? ?, which satis?es the conditions ( ) and ( ) for . Note that also the extended program ? is not strongly ? is also an SE-model of ? . equivalent to its shifted program ? . Indeed, ? ? , since ? Furthermore, is also not uniformly equivalent to ? is moreover a UE-model of ? , but has the single SE-model (and thus UE-model) ? ?.

? ? ? it holds that ? ? ??? and
?

?

has no SE-model ? ? such that ( ) ? · ? ?, i.e., violates the reduced rule

?

?

?

?

? ?? ? .

? and

? ?

?

?

?

?

?

?

10

5 Complexity
In this section, we address the computational complexity of uniform equivalence. While our main interest is with the problem of deciding uniform equivalence between two given programs, we also consider the related problems of UE-model checking and UEconsequence. denote the size of For UE-model checking, we have the following result. Let an object .

?

?

Theorem 9. Given a pair of sets ? ? and a program , deciding whether ? ?? ? ? ? is ( ) ???-complete in general, and ( ) feasible in polynomial time with respect to · · , if is head-cycle free. Hardness in case ( ) holds even for positive programs.

?

?

?

?

Corollary 1. UE-model checking for Horn programs is polynomial. We now consider the problem of our main interest, namely deciding uniform equivalence. By the previous theorem, the following upper bound on the complexity of this problem is obtained. Lemma 4. Given two

?? is the class of problems such that the complementary ? ??? Recall that ? problem is nondeterministically decidable in polynomial time with the help of an ?? ? ???? ). oracle (i.e., in ?

? ?

?? s ? and ?, deciding whether ?

?

? is in the class ??? .

Proof. To show that two ?? s and are not uniformly equivalent, we can by Theo? such that ? ? is an UE-model of exactly on of the rem 3 guess an SE-model ? programs and . By Theorem 9, the guess for ? ? can be veri?ed in polynomial ? ? . time with the help of an ?? oracle. This proves ? -membership of ? ?

?

?

?

?

?

?

?

This upper bound has a complementary lower bound proved in the following result. Theorem 10. Given two

?? s ? and ?, deciding ?

?

? Proof. (Sketch) Membership in ? has already been established in Lemma 4. To show ? -hardness, we provide a polynomial reduction of evaluating a quanti?ed Boolean ? ? formula (QBF) from a fragment which is known ? -complete to deciding uniform equivalence of two ?? s and . ? ? Consider a ? ? of form ? , where each is a conjunct of at most three literals over the boolean variables in , ? and ? . Deciding whether a given such is true is well-known to ? ? be ? -complete; thus deciding whether is false is ? -complete. W.l.o.g., we assume that each contains some literal over . Now let and be the following programs:

?

?

? is ??? -complete.

?

?

?

?

?

?

?

?

?

?

?

?

¨

? ?? ? ?? ? ??

? ??

? ? ?

?
11

? ?

and

where ? results from by replacing literals and by ? and ? , respectively. Informally, the disjunctive clauses with and ? in the head resp. and ? serve (resp., ). The atom ? serves for for selecting a truth assignment to the variable handling a spoiled assignment to some , which occurs if both and ? are true, and enforces the maximal interpretation as the unique model of , by the rules with ? in the body. Similarly, ? recognizes a spoiled assignment to some variable or that some disjunct of the QBF is true, and enforces for all atoms , ? and ? the unique value true. However, for the selection of a truth assignment is conditional to the truth ? of any atom or ? , while for it is mandatory by the additional rule ? ? . This difference leads to a suite of candidate SE-models ? ? of which do not satisfy ? are , where corresponds to a truth assignment to and all atoms not in false, such that ? ? violates uniform equivalence of and via ( ) just if there is no way to make all false by some assignment to . These candidate models for spoiling uniform equivalence are eliminated iff formula evaluates to false. Since and are obviously constructible in polynomial time, our result follows. ? ?

? ?

?? ? ?? ? ?? ??

? ?? ?? ?? ?? ?? ?? ? ? ? ??

? ? ? ? ?

? ? ? ? ? ?

?? ?? ? ?? ?? ? ? ?

? ?? ? ?? ?? ??? ??

? ? ? ?

? ? ? ?
?
,

,

?

? ?

? ?

?

?

?

?

? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?

The previous result shows that deciding uniform equivalence of ?? s and is more complex than deciding strong equivalence, which is in ??? [19, 24]. Thus, the more liberal notion of uniform equivalence comes at higher computational cost in general. However, for important classes of programs, it has the same complexity Theorem 11. Let and be ?? s without simultaneous negation and head-cycles ? each program is either positive or head-cycle free?. Then, deciding is ???- complete, where ???-hardness holds if is either positive or a ??? , and is Horn. ? for given de?nite Horn proNote that Sagiv showed [22] that deciding
?i.e.,

?

?

?

?

?

?

?

grams and is polynomial. This clearly generalizes to arbitrary Horn programs. We further remark that for ??? s deciding strong equivalence is also ???-hard. Finally, we complement the results on uniform equivalence and UE-model checking with brie?y addressing the complexity of UE-consequence. ? Theorem 12. Given a ?? and a rule , deciding ? is ( ) ? -complete in general, ( ) ???-complete if is either positive or head-cycle free, and ( ) polynomial if is Horn.

?

?

?

?

?

?

?

?

?

?

?

? Proof. (Sketch) The complementary problem, ? , is in ? for general and in ?? for head-cycle free , since a guess for a UE-model ? ? of which violates can, by Theorem 9 be veri?ed with a call to a ??-oracle resp. in polynomial time. In

?

?

?

?

?

?

?

12

case of a positive , by Theorem 5, , which is in ??? for general ? iff and polynomial for Horn . The hardness results can be obtained by adapting the constructions in hardness proofs of previous results. ? ?

?

?

?

?

? ?

?

We conclude this section with some remarks on the complexity of programs with variables. For such programs, in case of a given ?nite Herbrand universe the complexity of equivalence checking increases by an exponential. Intuitively, this is explained by the exponential size of the ground instance of a program over the universe. Note that Lin reported [14], without a full proof, that checking strong equivalence for programs in this setting is in ???, and thus has the same complexity as in the propositional case; however, this is not correct. Unsurprisingly, uniform equivalence of logic programs over an arbitrary Herbrand universe is undecidable according to Maher [16].

6 Extensions
Our results easily carry over to extended logic programs, i.e., programs where classical (also called strong) negation is allowed as well. If the inconsistent answer set is disregarded, i.e., an inconsistent program has no models, then, as usual, the extension can be by a positive atom semantically captured by representing strongly negated atoms ? and adding constraints ? , for every atom , to any program. Furthermore, since the proofs of our main results are generic in the use of reducts, they can be easily generalized to nested logic programs considered in [12, 23, 24, 19], ? i.e., we get the same characterizations and the same complexity ( ? ). However, if in the extended setting the inconsistent answer set is taken into account, then the given de?nitions have to be slightly modi?ed such that the characterizations of uniform equivalence capture the extended case properly. The same holds true for the characterization of strong equivalence by SE-models as illustrated by the following example. Note that the rede?nition of ? and × is straightforward. ? denote the set of all literals using strong negation over . Let ? Example 11. Consider the extended logic programs and ??? ??? . They both have no SE-model; × ? hence, by the criterion of Prop. 1, would hold, which implies and . However, has the inconsistent answer set ? , while has no answer set. Thus formally, and are not even equivalent if ? is admitted as answer set. Since [23, 12, 24] made no distinction between no answer set and inconsistent answer set, we start adapting the de?nition of SE-models. De?nition 6. A pair ? ?, ? , is an SEE-model of an extended ?? , if each of and is either consistent or equals ? and . From previous characterizations we get more general characterizations in terms of SEE-models for extended programs.

?

?

? ? ?

?

?

?

?

?

?

?

?

?

?

?

?

?

?

?

?

Theorem 13. Two extended

?? s ? and ? are

– strongly equivalent iff they have the same SEE-models, and – uniformly equivalent iff () ? ? is an SEE-model of iff it is an SEE-model of , and

?

?

13

( )

?

?,

that

?

, is an SEE-model of (resp. ) iff there exists a set , and ? ? is an SEE-model of (resp. ).

?

?

?

?

?

? , such

For positive programs, uniform and strong equivalence coincide also in the extended case.

We ?nally note that Pearce and Valverde have given, inspired by our work, a generalization of our results on UE-models to equilibrium logic [20].

? and ? be positive, extended ?? s. Then ? × ? iff ? ? ?. As a consequence of previous complexity results, checking ? ? ? (resp. ? × ?) ? for extended logic programs, ? and ?, is ?? -hard (resp. ???-hard). However, not all properties do carry over. As Example 11 reveals, in general a headcycle free extended ?? ? is no longer equivalent, and hence not uniformly equivalent, to its shift ? . However, under the condition below ? ? ? holds as well. Call any ?? contradiction-free, if ? ? is not an answer set of it. Proposition 5. Let ? be a head-cycle free and contradiction-free extended ?? . Then ? ? ? iff for each ? ? , the program ? is contradiction-free if the program ? ? ? ??? ? is contradiction-free. As shown in [6], “ ? ? ” can be equivalently replaced by “ ? ? such that ?? ? ,” where ? ?? ? ? ? ? ??? ? ??? ? ? ? . ?
Theorem 14. Let
? ? ?

7 Conclusion
Uniform equivalence of logic programs, which has been considered earlier for datalog and general Horn logic programs [22, 16], under stable semantics is an interesting concept which can be exploited for program optimization. We have presented characterizations of uniform equivalence in terms of Turner’s SE-models [23, 24] (equivalently, HT models [12]), and we have analyzed the computational cost for testing uniform equivalence and related problems. While we have presented a number of results, there are several issues which remain to be considered. We have found a simple and appealing characterization of uniform equivalence in terms of UE-models for ?nitary programs, which single out from the SEmodels certain maximal models. However, in case of in?nite programs, such maximal models need not exist. It thus would be interesting to see whether also in this case uniform equivalence can be captured by a set of SE-models, or whether a completely novel notion of model (like SE-model for strong equivalence) is needed. Researching this issue is part of our ongoing work. Another direction of research is to investigate the usage of uniform equivalence for program replacement and program rewriting in optimization. To this end, in follow-up works [7, 8] we analyzed compliances with current optimization techniques and gave characterizations of programs possessing equivalent programs belonging to syntactic subclasses of disjunctive logic programs under both, uniform and strong equivalence. Furthermore we gave encodings of our characterizations in answer-set programming and investigated the computational complexity of program simpli?cation and determining semantical equivalence. 14

Acknowledgments. We thank the anonymous referees for their valuable comments.

References
1. R. Ben-Eliyahu and R. Dechter. Propositional semantics for disjunctive logic programs. Annals of Mathematics and Arti?cial Intelligence, 12:53–87, 1994. 2. R. Ben-Eliyahu and L. Palopoli. Reasoning with minimal models: Ef?cient algorithms and applications. In Proc. KR’94, pp. 39–50, 1994. 3. P. Cabalar. A three-valued characterization for strong equivalence of logic programs. In Proc. AAAI ’02, pp. 106–111, 2002. 4. D. J. de Jongh and L. Hendriks. Characterizations of strongly equivalent logic programs in intermediate logics. Theory and Practice of Logic Programming, 3(3):259–270, 2003. 5. T. Eiter, G. Gottlob, and H. Mannila. Disjunctive datalog. ACM TODS, 22(3):364–417, 1997. 6. T. Eiter and M. Fink. Uniform equivalence of logic programs under the stable model semantics. Tech. Rep. INFSYS RR-1843-03-08, Inst. f¨ r Informationssysteme, TU Wien, 2003. u 7. T. Eiter, M. Fink, H. Tompits, and S. Woltran. Simplifying logic programs under uniform and strong equivalence. Manuscript, submitted, July 2003. 8. T. Eiter, M. Fink, H. Tompits, and S. Woltran. Eliminating disjunction from propositional logic programs under stable model preservation. Manuscript, submitted, August 2003. 9. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Logic Programming: Proc. Fifth Int’l Conference and Symposium, pp. 1070–1080, 1988. 10. M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Computing, 9:365–385, 1991. 11. N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, C. Koch, C. Mateis, S. Perri, and F. Scarcello. The DLV system for knowledge representation and reasoning. Tech. Rep. INFSYS RR-1843-02-14, Inst. f¨ r Informationssysteme, TU Wien, 2002. u 12. V. Lifschitz, D. Pearce, and A. Valverde. Strongly equivalent logic programs. ACM Trans. on Computational Logic, 2(4):526–541, 2001. 13. V. Lifschitz and H. Turner. Splitting a logic program. In Proc. ICLP-94, pp. 23–38, 1994. 14. F. Lin. Reducing strong equivalence of logic programs to entailment in classical propositional logic. In Proc. KR-2002, pp. 170–176, 2002. 15. F. Lin and Y. Zhao. ASSAT: Computing answer sets of a logic program by SAT solvers. In Proc. AAAI-2002, pp. 112–117, 2002. 16. M. J. Maher. Equivalences of logic programs. In Minker [17], pp. 627–658. 17. J. Minker, editor. Foundations of Deductive Databases and Logic Programming. Morgan Kaufmann, 1988. 18. I. Niemel¨ , P. Simons, and T. Syrj¨ nen. Smodels: A system for answer set programming. In a a Proc. 8th Int’l Workshop on Non-Monotonic Reasoning ?NMR’2000?, 2000. 19. D. Pearce, H. Tompits, and S. Woltran. Encodings for equilibrium logic and logic programs with nested expressions. In Proc. EPIA 2001, LNCS 2258, pp. 306–320, 2001. 20. D. Pearce and A. Valverde. Some types of equivalence for logic programs and equilibrium logic. In Proc. Joint Conf. Declarative Programming (APPIA-GULP-PRODE), 2003. 21. T. Przymusinski. Stable semantics for disjunctive programs. New Generation Computing, 9:401–424, 1991. 22. Y. Sagiv. Optimizing datalog programs. In Minker [17], pp. 659–698. 23. H. Turner. Strong equivalence for logic programs and default theories (made easy). In Proc. LPNMR-01, LNCS 2173, pp. 81–92, 2001. 24. H. Turner. Strong equivalence made easy: nested expressions and weight constraints. Theory and Practice of Logic Programming, 3(4-5):609–622, 2003.

15


赞助商链接

更多相关文章:
更多相关标签:

All rights reserved Powered by 甜梦文库 9512.net

copyright ©right 2010-2021。
甜梦文库内容来自网络,如有侵犯请联系客服。zhit325@126.com|网站地图