P-stable models of Strong kernel programs

Abstract

Currently non-monotonic reasoning (NMR) is a promising approach to model features of common sense reasoning. In order to formalize NMR the research community has applied monotonic logics. The present paper furthers the study of one of the semantics useful in this formalization called p-stable. We introduce three di®erent formats for normal programs: Negative normal programs, Restricted negative normal programs and Strong kernel programs. This forms helps to simplify the search of p-stable models of the original program. One of the main results of this paper indicates that the p-stable semantics for strong-kernel programs agrees with the stable semantics for kernel programs as de¯ned in [2]. In this way all the applications based on stable semantics of kernel programs can also be based on p-stable semantics of strong kernel programs.

-

Currently non-monotonic reasoning (NMR) is a promising approach to model features of common sense reasoning. In order to formalize NMR the research community has applied monotonic logics. The present paper furthers the study of one of the semantics useful in this formalization called p-stable.

In [ 7 ] was suggested the use of Autoepistemic Logic (AL) as an alternative formalization of NMR to avoid the problems encountered with standard modal logics. Later Gelfond and Lifschitz de¯ned the stable model semantics [ 4 ] based on an interpretation of :a. This interpretation characterizes perfect models of strati¯ed logic programs in terms of the extensions of the corresponding autoepistemic theory. More recently, in [ 1 ] is described how the stable semantics of disjunctive programs can be characterized in terms of AL via Gelfond's translation.

Additionally Pearce in [ 12 ] presented a characterization of the stable model semantics in terms of a collection of logics. He proved that a formula is \entailed by a disjunctive program in the stable model semantics if and only if it belongs to every intuitionistically complete and consistent extension of the program formed by adding only negated atoms". He also showed that in place of intuitionistic logic, any proper intermediate logic can be used. The strongest intermediate logic is Goedel's 3-valued logic G3. The construction used by Pearce is called a weak completion. Based on the work of Pearce in [ 12 ], the authors of [ 9 ] express the logic G3 in terms of Lukaciewicz L3-logic and gave a new characterization of stable models based on Lukaciewicz L3-logic. In [ 9 ] is also introduced a very similar 3-valued logic based in the Lukaciewicz L3-logic: the G03 logic. Later, in [ 10 ] a new semantics, based on weak completions, is de¯ned with the G03 logic.

In [ 8 ] the authors generalize to disjunctive programs what was done in [ 10 ]. They introduce the p-stable semantics for normal programs by using a transformation similar to the one used by Gelfond and Lifschits [ 4 ]. This new semantics for disjunctive programs agrees with semantics de¯ned in terms of weak completions for the paraconsistent logics studied in [ 10 ]. The authors also present some results that give conditions under which the concepts of stable and p-stable models agree. They show that the p-stable model semantics for normal programs is powerful enough to express any problem that can be expressed with the stable model semantics for disjunctive programs. It is important to mention that pstable semantics, which can be de¯ned in terms of paraconsistent logics, shares several properties with the stable semantics, but is closer to classical logic. For example, the following program P does not have stable models. a à :b: a à b: b à a:

However the set fa; bg could be considered the intended model for P in classical logic. Moreover, it is the p-stable model of P .

In [ 11 ] is described a schema for the implementation of p-stable semantic using two well known open source tools: Lparse and Minisat. In [ 11 ] is also presented a prototype written in Java of a tool based on that schema.

The present paper furthers the study of p-stable semantics. We introduce three di®erent formats for normal programs: Negative normal programs, Restricted negative normal programs and Strong kernel programs. This forms helps to simplify the search of p-stable models of the original program. Besides we show that the p-stable semantics for strong kernel programs agrees with the stable semantics for kernel programs as de¯ned in [ 2 ]. In this way all the applications based on stable semantics of kernel programs can also be based on p-stable semantics of strong kernel programs.

In [ 2 ] is introduced the de¯nition of kernel programs and it is shown that any propositional logic program P admits an equivalent|w.r.t. stable semantics| program in a format called kernel. Currently there are applications based on this kind of programs (see [ 2,5,3 ]). Moreover, kernel programs are useful since they allow us to express well known problems as the 3-coloring problem (see [ 5 ]).

This paper is structured as follows. In section 2 we introduce the general syntax of the logic programs used in this paper. We also provide the de¯nition of stable semantics, p-stable semantics, and kernel programs. In section 3 we give the de¯nition of the three di®erent formats for normal programs: negative normal programs, restricted negative normal programs, and strong kernel programs. We also show the di®erent results about the stable semantics and the p-stable semantics of programs in these formats. Finally in section 4 we present some conclusions. 2

Background

In this section we summarize some basic concepts and de¯nitions used to understand this paper. 2.1

Logic programs

A signature L is a ¯nite set of elements that we call atoms, or propositional symbols. The language of a propositional logic has an alphabet consisting of proposition symbols : p0; p1; : : : ; connectives: ^, _, Ã, :; and auxiliary symbols : (, ). Where ^, _, Ã are 2-place connectives and : is a 1-place connective. Formulas are built up as usual in logic. A literal is either an atom a, or the negation of an atom :a. The formula F ´ G is an abbreviation for (F Ã G) ^ (G Ã F ). A clause is a formula of the form H Ã B (also written as B ! H), where H and B, arbitrary formulas in principle, are known as the head and body of the clause respectively. The body of a clause could be empty, in which case the clause is known as a fact and can be denoted just by: H Ã. In the case when the head of a clause is empty, the clause is called a constraint and is denoted by: Ã B.

A disjunctive clause is a clause of the form H Ã B+ [ :B¡ where H is a disjunction of atoms h1_h2_: : :_hs, B+ is a conjunction of atoms b1^b2^: : :^bn, and :B¡ is a conjunction of negated atoms :bn+1 ^ :bn+2 ^ : : : ^ :bm. H, B+, and B¡ could be empty sets of atoms. When the set H contains exactly one element the clause is called normal. A de¯nite program is a normal program whose rules do not have negations in their bodies.

Finally, a program is a ¯nite set of clauses. If all the clauses in a program are of a certain type, we say the program is also of that type. For instance a set of disjunctive clauses is an disjunctive program, a set of normal clauses is a normal program and so on.

Finally we give two de¯nitions useful to understand the de¯nitions of stable and p-stable semantics for normal programs.

Let P be a normal program and M be a set of atoms. We de¯ne: RED(P; M ) = fH Ã B+; :(B¡ \ M ) j H Ã B+; :B¡ 2 P g.

For any program P , the positive part of P , denoted by P OS(P ) is the program consisting exclusively of those rules in P that do not have negated literals. 2.2

Stable and P-stable semantics

From now on we assume that the reader is familiar with the notion of classical minimal model [ 6 ].

Now we give the de¯nition of stable semantics for normal programs. De¯nition 1. [ 8 ] Let P be a normal program and let M µ LP . Let us put P M = P OS(RED(P; M )) then we say that M is a stable model of P if M is a minimal classical model) of P M .

Here we de¯ne the p-stable semantics for normal programs.

De¯nition 2. [ 8 ] Let P be a normal program and M be a set of atoms. We say that M is a p-stable model of P if 1. M is a classical model of P (i.e. a model in classical logic), and 2. the conjunction of the atoms in M is a logical consequence in classical logic of RED(P; M ) (denoted as RED(P; M ) j= M ).

Example 1. Let P be the normal program:

b à :a: a à :b: p à :a: p à :p:

We can verify that M1 = fa; pg and M2 = fb; pg model the rules of P . From the de¯nition of the RED transformation we ¯nd

RED(P; M1) = fb à :a; a Ã; p à :a; p à :pg

RED(P; M2) = fb Ã; a à :b; p Ã; p à :pg And it is clear that RED(P; M1) j= M1 and RED(P; M2) j= M2. Hence M1 and M2 are p-stable models for P . 2.3

Kernel programs

In [ 2 ] the authors show that any propositional logic program P admits an equivalent|w.r.t. stable semantics|program in a format called kernel. They indicate that a program in kernel format is useful to studying the existence and number of stable models. Here we present the de¯nition of kernel programs as de¯ned in [ 2 ]. We also mention some applications of this kind of programs.

A kernel program is composed of the atoms which are unde¯ned in the Wellfounded semantics, which are those that directly a®ect the existence of answer sets. The body of rules is composed of negative literals only.

De¯nition 3. [ 2 ] A logic program P is a kernel program if the following conditions hold: 1. P is WFS-irreducible, i.e., the well-founded model of P is empty, W F S(P ) = h;; ;i (see [ 13 ]); 2. every rule has its body composed of negative literals only; 3. every atom in P occurs in the body of some rule.

It is important to note that kernel programs are useful and interesting since they allow us to express well known problems as the 3-coloring problem. In [ 5 ] you can see an stable encoding of the 3-coloring problem.

In [ 2 ] is also showed how to check consistency of kernel programs in terms of colorings of the Extended Dependency Graph (EDG) program representation. The EDG program representation has a regular and simple structure. Moreover this representation gives the ¯rst purely-syntactic and complete characterization of consistent logic programs w.r.t. stable semantics.

The authors of [ 5 ] also consider programs in kernel form. In [ 5 ] is presented a distributed version of the adjSolver algorithm for computing stable models of logic programs in kernel form. The intrinsic parallelism of the branch-and-bound structure of adjSolver is exploited to control, with a centralized architecture, the delegation of promising search subspaces to distributed handling agents. AdjSolver was designed to solve the problem of computing stable models through the search for admissible 2-colorings of the EDG representing the logic program. The adjSolver search strategy is di®erent from the semantics-based coloringpropagation strategy adopted in literature for stable models computation by graph coloring.

The authors of [ 3 ] de¯ne various notions of coherence, that establish what relation there should be between the stable models of the original programs, and the stable models of the programs resulting from update/modi¯cation. They introduce signi¯cant su±cient conditions for coherence on the class of kernel programs. They also indicate that logic programs in kernel form allow one to distinguish the elements the program is composed of, namely cycles and handles, and thus to reason more easily about what happens when the program is modi¯ed. 3

Negative normal programs and Restricted negative normal programs In this section we give the de¯nition of three di®erent formats for normal programs: Negative normal programs, Restricted negative normal programs and Strong kernel programs. One of the main results indicates that the stable semantics and the p-stable semantics of a restricted negative normal program coincide. We also show how the p-stable semantics of a negative normal program or a kernel program (as de¯ned in [ 2 ]) P corresponds to the p-stable semantics of a particular program associated to P . This new program is a restricted negative normal program and it is the result of applying a transformation to the program P .

We start by introducing the de¯nitions of negative normal programs and restricted negative normal programs. This de¯nitions will be useful to de¯ne negative normal programs and restricted negative normal programs with constraints. conditions De¯nition 4. Let P be a normal program. We say that P is a negative normal (NN) program if it satis¯es the ¯rst of the two conditions listed below, and we say that P is a restricted negative normal (RNN) program if it satis¯es both 1. every rule has its body composed of negative literals only; 2. the head of any rule does not appear in the body of the same rule.

Let us observe that a RNN program is a NN program, and that NN, RNN and kernel programs have the common characteristic of having the body of every rule composed of negative literals only.

Let P be a RNN program, for any M

:b1; ^ : : : ^ :bm 2 P; fb1; : : : ; bmg \ M = ;g.

The following lemma will be useful to show that the stable semantics and the p-stable semantics of a RNN program coincide. Given a RNN program P , this lemma gives a characterization for a set M µ LP , to be a p-stable model of P . µ LP , we de¯ne SM = fa j a à Lemma 1. Let P be a RNN program. If M is p-stable model of P then M = SM . Proof. RED(P; M ) = f a à :(B¡ \ M ) j H à :B¡ 2 P g: By part 1) of the de¯nition of p-stable model (De¯nition 2), it follows that SM ½ M . Let us assume that M n SM 6= ; and take m 2 M n SM . Let us de¯ne an interpretation: I : LP ! f0; 1g such that I(a) = 1 for each a 2 LP n fmg and I(m) = 0.

Now, using the fact that the program P has the property that the head of each rule does not appear in its body, it follows that I is a classical model for RED(P; M ) but it is not a model for M (Since I(m) = 0) this contradicts 2) in the de¯nition of a p-stable model (De¯nition 2) and the lemma is proved.

The following theorem indicates that the stable semantics and the p-stable semantics of a RNN program coincide.

Theorem 1. Let P be a RNN program, then the stable semantics of P coincides with the p-stable semantics of P .

Proof. If M is a p-stable model of P then M = SM according to the lemma 1, and from the de¯nition of P M (De¯nition of a stable model), P M = f then we conclude that M is a minimal model of P M and then a stable model of a à j a 2 SM g P . that P M minimal model for P M = f Let us now assume that M is a stable model of P . It follows that M is a ½ RED(P; M ), it follows that RED(P; M ) j= M .

We still need to show that M is a classical model of P . Let us consider a Therefore M models all of the rules in P as we wanted to show. rule a à :b1 ^ :b2 ^ : : : ^ :bs 2 P , such that a 62 M . Then there is at least an i for which bi 2 M (otherwise a 2 SM = M ), then the rule is modeled by M . a à j a 2 SM g. Therefore M = SM . From the fact tu tu

Let us observe that, from the de¯nition, in a NN program the head of any rule could appear in the body of the same rule.

We shall show how the p-stable semantics of a NN program P corresponds to the p-stable semantics of a particular program associated to P . This new program is a RNN program and it is the result of applying the following transformation to P : For any normal program P , the transformed program, denoted by T RN (P ) is the program that results from P after deleting from the body of each rule the atom that appears as the head of the same rule. The rules that do not present this condition remain the same.

De¯nition 5. For a rule r of the form a à :a ^ :b1 ^ : : : ^ :bn 2 P , we de¯ne the transformation T RN as follows: T RN (r) = a à :b1 ^ : : : ^ :bn. For a rule r for which head(r) 62 body(r), we de¯ne T RN (r) = r. For a normal program P we de¯ne the transformation T RN as follows: T RN (P ) = fT RN (r) j r 2 P g.

Here we show how the p-stable semantics of a NN program P corresponds to the p-stable semantics of the RNN program T RN (P ).

Theorem 2. Let P be a NN program, then the p-stable semantics of P coincides with the p-stable semantics of the RNN program T RN (P ). for one i, bi 2 Proof. Let us assume that M is a p-stable model of P and let a à :a; :b1; ::::bn be one of the rules in P with the property that the head appears in the body. Assume that a 2= M . Since M is a classical model for the rule, then at least

M , making the rule true according to M ; but then it is clear that the corresponding rule in T RN (P ) is also modeled by M . It follows that a classical model for P is also a classical model for T RN (P ). Next, by hypothesis we have that RED(P; M ) j= M . Now, it is easy to see that for each rule r 2 P , the rule RED(r; M ) is a logical consequence (in classical logic) of the rule RED(T RN (r); M ), Therefore we conclude that RED(T RN (P ); M ) j= M .

Now, if M is a p-stable model of T RN (P ), according to lemma 1, M consists of those atoms for which there exists a rule r : a à :b1 ^ : : : ^ :bn such that

Let us show ¯rst that M is a classical model of P . It is enough to examine bi 62 M for all i. the rules in P n T RN (P ):

a à :a ^ :b1 ^ : : : ^ :bn follows now. the rule is modeled by M . So M

models P .

In the case for which a 2 M , there is nothing to prove. In the case for which a 62 M , according to the lemma 1 there must exist bi 2 M for some i, and then

Now, it only remains to prove that RED(P; M ) j= M . But again, M consists of those atoms for which there is a rule, a à :b1 ^ : : : ^ :bn and bi 62 M for all i; then RED(P; M ) contains the rules a Ã, for all a 2 M . The desired conclusion tu

We also introduce another format for normal program called Strong Kernel program. This last format considers the three conditions of a kernel program (as de¯ned in [ 2 ]) and also the condition of RNN programs about that the head of any rule does not appear in the body of the same rule.

De¯nition 6. Let P be a normal program. We say that P is a strong kernel (SK) program if the following conditions hold: 1. P is WFS-irreducible, i.e., the well-founded model of P is empty, W F S(P ) = h;; ;i (see [ 13 ]); 2. every rule has its body composed of negative literals only; 3. every atom in P occurs in the body of some rule. 4. the head of any rule does not appear in the body of the same rule.

Let us observe that SK programs are also RNN programs. Then a corollary of theorem 1 indicates that the stable semantics of a SK program coincides with the p-stable semantics of the same program.

Corollary 1. Let P be a SK program, then the stable semantics of P coincides with the p-stable semantics of P .

Let us observe ¯rst, that a kernel program (as de¯ned in [ 2 ]) is a NN program, and also that if we apply the transformation T RN to a kernel program, then we obtain a SK program. So, a corollary of theorem 2 indicates that the p-stable semantics of a kernel program P corresponds to the p-stable semantics of the SK program T RN (P ).

Corollary 2. Let P be a kernel program, then the p-stable semantics of P coincides with the p-stable semantics of the SK program T RN (P ).

As a consequence of corollary 2, all the applications based on stable semantics of kernel programs can also be based on p-stable semantics of strong kernel programs: to check consistency of kernel programs in terms of colorings of the Extended Dependency Graph program representation, as described in [ 2 ]; a distributed version of the adjSolver algorithm for computing p-stable models of logic programs in strong-kernel form, as described in [ 5 ]; and to distinguish the elements that a program is composed of, namely cycles and handles, and thus to reason more easily about what happens when the program is modi¯ed, as described in [ 3 ]. We mentioned this applications at the end of section 2 of this paper.

We remark that kernel and, in particular strong kernel programs are useful and interesting since they allow us to express well known problems as the 3-coloring problem. Next, we illustrate the p-stable kernel encoding of the 3coloring problem over the graph hV; Ei = hf1; 2g; f(1; 2)gi. Let us note that in this program, when expressed in the p-table semantics, is necessary to implement three rules for each constraint necessary in the stable semantics. In the encoding below, those three rules are written below the corresponding constraint in the stable semantics, which has been commented out. The formal and detailed description of how to write such constraints in the p-stable semantics, is presented in [ 8 ]. %Assignment of colors to vertices col(1; blue) à :col(1; red); :col(1; green): col(2; blue) à :col(2; red); :col(2; green): col(1; red) à :col(1; blue); :col(1; green): col(2; red) à :col(2; blue); :col(2; green): col(1; green) à :col(1; blue); :col(1; red): col(2; green) à :col(2; blue); :col(2; red): % arc(1,2) cannot join 2 nodes of the same color % à :col(1,red); :col(2,red); :col(1, blue); :col(2, blue): x à :y; :col(1; red); :col(2; red); :col(1; blue); :col(2; blue): y à :z; :col(1; red); :col(2; red); :col(1; blue); :col(2; blue): z à :x; :col(1; red); :col(2; red); :col(1; blue); :col(2; blue): % à :col(1,red); :col(2,red); :col(1,greeen); :col(2,green): x à :y; :col(1; red); :col(2; red); :col(1; green); :col(2; green): y à :z; :col(1; red); :col(2; red); :col(1; green); :col(2; green): z à :x; :col(1; red); :col(2; red); :col(1; green); :col(2; green): % à :col(1,green); :col(2,green); :col(1,blue); :col(2,blue): x à :y; :col(1; green); :col(2; green); :col(1; blue); :col(2; blue): y à :z; :col(1; green); :col(2; green); :col(1; blue); :col(2; blue): z à :x; :col(1; green); :col(2; green); :col(1; blue); :col(2; blue):

There are six p-stable models: fcol(1; red); col(2; green)g; fcol(2; green); col(1; blue)g; fcol(1; green); col(2; red)g; fcol(1; blue); col(2; red)g; fcol(1; green); col(2; blue)g; and fcol(1; red); col(2; blue)g. Each of them indicates a coloring for the given graph. 4

Conclusion

This paper furthers the study of p-stable semantics. We introduced three different formats for normal programs: NN programs, RNN programs and SK programs. We showed that the stable semantics and the p-stable semantics of a RNN program coincide; and that the p-stable semantics of a NN program corresponds to the p-stable semantics of a particular RNN program associated to the original program.

Since the SK format considers the three conditions of a kernel program [ 2 ] and also the condition of RNN programs about that the head of any rule does not appear in the body of the same rule then, is showed that the stable semantics of a SK program coincides with the p-stable semantics of the same program and that the p-stable semantics of a kernel program corresponds to the p-stable semantics of a particular SK program.

We also indicated that all the applications based on stable semantics of kernel programs can also be based on p-stable semantics of strong kernel programs.

We remarked that kernel and, in particular strong kernel programs are useful and interesting since they allow us to express well known problems as the 3coloring problem.

References

1. C. Baral . Knowledge Representation, reasoning and declarative problem solving with Answer Sets . Cambridge University Press, Cambridge, 2003 .

2. S. Constantini and A. Provetti . Normal forms for answer set programming . Journal of Theory and Practice of Logic Programming , 5 : 747 { 760 , 2005 .

3. S. Costantini , B. Intrigila , and A. Provetti . Coherence of updates in answer set programming . In Proc. of the IJCAI-2003 Workshop on Nonmonotonic Reasoning, Action and Change, NRAC03 , pages 66 { 72 , 2003 .

4. M. Gelfond and V. Lifschitz . The Stable Model Semantics for Logic Programming . In R. Kowalski and K. Bowen, editors, 5th Conference on Logic Programming , pages 1070 { 1080 . MIT Press, 1988 .

5. G. Grossi , M. Marchi , E. Pontelli, and A. Provetti . Experiments with answer set computation over parallel and distributed architectures . In Proceedings of 4th International Workshop on Answer Set Programming (ASP2007) ., September 2007 . To appear an extended version in a special issue of the Journal of Logic and Computation .

6. J. W. Lloyd . Foundations of Logic Programming . Springer, Berlin, second edition, 1987 .

7. R. C. Moore . Autoepistemic logic . In P. Smets, E. H. Mamdani , D. Dubois , and H. Prade, editors, Non-Standard Logics for Automated Reasoning . Academic Press, 1988 .

8. M. Osorio , J. Arrazola , and J. L. Carballido . Logical weak completions of paraconsistent logics . To apper in the Journal of Logic and Computation , 2008 .

9. M. Osorio , V. Borja , and J. Arrazola . Three valued logic of LÃukasiewicz for modeling semantics of logic programs . In Proceedings of IBERAMIA, number 3315 in Lecture Notes in Computer Science , pages 343 { 352 . Springer, 2004 .

10. M. Osorio , J. A. Navarro , J. Arrazola , and V. Borja . Logics with common weak completions . Journal of Logic and Computation , 16 ( 6 ): 867 { 890 , 2006 .

11. S. Pascucci and A. Lopez. Implementing p -stable with simpli¯cation capabilities . Submmited to Inteligencia Arti¯cial, Revista Iberoamericana de I.A. , Spain , 2008 .

12. D. Pearce . Stable Inference as Intuitionistic Validity . Logic Programming , 38 : 79 { 91 , 1999 .

13. A. van Gelder , K. Ross , and J. S. Schlipf . The well-founded semantics for general logic programs . Journal of the ACM , 38 ( 3 ): 620 { 650 , 1991 .