We present an update operator and several of its properties. The semantics of our update operator is based on a concept called minimal generalized p-stable models which is based on a novel semantics called the p-stable semantics.
Update by de¯nition means that there is new information that must be added to the older, and some information could be changed. Intelligent agents use this, in order to bring new knowledge to their knowledge base. But there is a main problem that updates can present, and it is inconsistency. So, it is important to use an approach to avoid inconsistencies in the knowledge base. For instance, it could be that in an initial moment we can infer a from a knowledge base (KB), and later the KB is updated with the new information ¡a (where ¡ denotes negation). It is easy to see, that if we only take the union of the initial KB and ¡a we will have an inconsistency. Then it is useful to apply an update approach that avoids the inconsistency and now allows to infer ¡a since the newer knowledge has priority over the older.
Currently there are several approaches in non-monotonic reasoning dealing
with updates, such as [
Moreover, since classical logic identi¯es a class of formal logics that have been most intensively studied and most widely used, it turns out to be very useful to have some updates approaches that allow us to keep a compromise with such logic. For this reason, as part of the contribution of this paper, we propose an update semantics that allow us to keep a compromise with classical logic. Thus the result of using our semantics to update program P1 with program P2 is fa; bg.
Our semantics is based on a concept called minimal generalized p-stable
models. The de¯nition of minimal generalized p-stable models is inspired by a concept
called minimal generalized answer sets of abductive programs [
The semantics of minimal generalized p-stable models is based on the p-stable
semantics. The p-stable semantics is based on G03 which is a paraconsistent logic
that has recently been studied in some detail in [
In section 2 we summarize some basic concepts and de¯nitions used to understand this paper. In section 3 we review the minimal generalized p-stable models. In section 4 we present our update semantics and some formal properties. Finally, in section 5 we present some conclusions. 2
In this section we summarize some basic concepts and de¯nitions necessary to understand this paper. 2.1
Logic programs We use the language of propositional logic in the usual way. We consider propositional symbols : p; q; : : : ; propositional connectives : ^; _; !; :; ¡; and auxiliary symbols : `(',`)',`.'. Well formed propositional formulas are de¯ned as usual. We consider two types of negation: strong or classical negation (written as ¡) and negation-as-failure (written as :). Intuitively, :a is true whenever there is no reason to believe a, whereas ¡a requires a proof of the negated atom. An atom is a propositional symbol. A literal is either an atom a or the strong negation of an atom ¡a.
A normal clause is a clause of the form a à b1 ^ : : : ^ bn ^ :bn+1 ^ : : : ^ :bn+m where a and each of the bi are atoms for 1 · i · n + m. In a slight abuse of notation we will denote such a clause by the formula a à B+ [ :B¡ where the set fb1; : : : ; bng will be denoted by B+, and the set fbn+1; : : : ; bn+mg will be denoted by B¡. Given a normal clause a à B+ [ :B¡ we say that a is the head and B+ [ :B¡ is the body of the clause. A clause with an empty body is called a fact ; and a clause with an empty head is called a constraint. Facts and constraints are also denoted as f à and à g respectively. We de¯ne a normal logic program P , as a ¯nite set of normal clauses. The signature of a normal logic program P , denoted as LP , is the set of atoms that occur in P . Given a set of atoms M and a signature L, we de¯ne :Mf = f:a j a 2 L n M g. Since we shall restrict our discussion to propositional programs, we take for granted that programs with predicate symbols are only an abbreviation of the ground program. From now on, by program we will mean a normal logic program when ambiguity does not arise.
In our programs we will manage the strong negation ¡ as follows: each atom ¡a is replaced by a new atom symbol a0 which does not appear in the language of the program and we add the constraint à a ^ a0 to the program.
Finally, we give a de¯nition that will help us to de¯ne the p-stable semantics for programs.
De¯nition 1. [
Example 1. [
The p-stable semantics
Here, we present a ¯xed point characterization, using classical logic, of the
pstable semantics for normal programs. This kind of characterization is useful for
implementations of a semantics.2 Following a similar approach to [
De¯nition 2. [
The following examples illustrate how to obtain the p-stable models. The ¯rst example shows a program with a single p-stable model, which is also a classical model. The second example shows a program which has no stable models and whose p-stable and classical models are the same.
Example 2. Let P = fq à :qg. Let us take M = fqg then RED(P; M ) = fq à :qg. It is clear that M models P in classical logic and RED(P; M ) j= M since (:q ! q) ! q is a theorem in classical logic with the negation :, now interpreted as classical negation. Therefore M is a p-stable model of P .
http://sites.google.com/site/computingpstablesemantics/ is at Example 3. Let P = fa à :b; a à b; b à ag. We can verify that M = fa; bg models the clauses of P in classical logic. We ¯nd that RED(P; M ) = P . Now, from the ¯rst and third clause, it follows that (:b ! b) where the negation : is now interpreted as classical negation. Since (:b ! b) ! b is a theorem in classical logic, it follows that RED(P; M ) j= M . Therefore, M is a p-stable model of P .
Not all programs have p-stable models, that is why it is convenient to have the next de¯nition.
De¯nition 3. Let P be a program. We say that P is p-stable consistent if P has at least one p-stable model. We say that P is p-stable inconsistent if P does not have p-stable models.
We also remark that the authors of [
Now, we present two notions of equivalence for programs.
De¯nition 4. [
The following lemma3 indicates that given a program P and an atom x that does not occur in P , we can de¯ne a new program P 0 such that P and P 0 are equivalent and LP 0 = LP [ fxg. The two programs must have the same clauses except for one of them. One of the clauses in P 0 corresponds to one of the clauses in P after adding :x to its body. This way, P and P 0 have the same p-stable models since x does not appear as the head of any clause in P 0.
Lemma 1. Let P be a program and x be an atom, x 62 LP . Let r be any clause a à B+ [ :B¡ in P . Then M is a p-stable model of P i® M is a p-stable model of (P n frg) [ fa à B+ [ :(B¡ [ fxg)g. 3
The de¯nition of our update semantics is based on Minimal Generalized (MG) p-stable models. The intuition behind the MG p-stable models is simple. Given a logic program P and a set of atoms A, the MG p-stable models of P are the p-stable models of P [ ¢ that are obtained by adding the minimal subset ¢ µ A to P for which P [¢ has p-stable models.4 For instance, let us consider a program P = f¡a; a à :bg that does not have p-stable models and let A = fb; cg then,
of facts de¯ned by its elements. the MG p-stable model is fb; ¡ag where the minimal subset of A added to P is fbg.
Next, we present the de¯nition of abductive logic programs and their
semantics in terms of the minimal explicit generalized p-stable models. Then, we de¯ne
the MG p-stable models based on the minimal explicit generalized p-stable
models. These de¯nitions are similar to the de¯nitions of syntax and semantics of
abductive logic programs as presented in the context of the stable semantics in
[
De¯nition 5. An abductive logic program is a pair hP; Ai where P is a program and A is a set of atoms, called abducibles. hM; ¢i is an explicit generalized (EG) p-stable model of the abductive logic program hP; Ai i® ¢ µ A and M is a p-stable model of P [ ¢.
We give an ordering among EG p-stable models in order to get the minimal of them.
De¯nition 6. Let T = hP; Ai be an abductive logic program. Let hM1; ¢1i and hM2; ¢2i be two EG p-stable models of T , we de¯ne hM1; ¢1i < hM2; ¢2i if ¢1 ½ ¢2; this order is called inclusion order. hM; ¢i is a Minimal Explicit Generalized (MEG) p-stable model of T i® hM; ¢i is an EG p-stable model of T and it is minimal w.r.t. inclusion order.
For practical purposes, given a MEG p-stable model, hM; ¢i, we are only interested in its ¯rst entry, namely M , and we call it a Minimal Generalized (MG) p-stable model of an abductive logic program.
Example 4. Let hP; Ai be the abductive logic program where the set of abductive atoms is A = fx1; x2g and P = fb à :x1; a à b ^ :x2; ¡ag. There are three EG p-stable models of hP; Ai which are: hf¡a; x1g; fx1gi, hf¡a; b; x2g; fx2gi, and hf¡a; x1; x2g; fx1; x2gi. We can see that for ¢ = ; there is no EG p-stable models. Therefore, the MEG p-stable models are hf¡a; x1g; fx1gi and hf¡a; b; x2g; fx2gi, and the MG p-stable models are f¡a; x1g and f¡a; b; x2g.
The following lemma presents some results about MEG p-stable models that will be useful in a later section to show the properties of our update operator. The proof of this lemma is straightforward.
Lemma 2. Let T = hP; Ai be an abductive logic program such that P is p-stable consistent. Then, M is a p-stable model of P i® M is a MG p-stable model of T ; and if hM; ¢i is a MEG p-stable model of T then ¢ = ;. 4
In this section, we de¯ne the semantics of our update operator based on the concept of MG p-stable models, and we study some of its properties. We use ¯ to represent the update operator. In order to obtain the ¯-update p-stable models of a pair of logic programs P = (P1; P2), we de¯ne an update logic program, denoted as P¯. The update logic program is obtained by joining P10 to P2, where P10 is the resulting program from transforming P1 as follows: at the end of each clause of P1 which is not a constraint we add the negation-as-failure of an abducible (a new atom). The intuition behind the transformation applied to a program P1 consists in weakening the knowledge in P1 when giving more relevance to the knowledge contained in P2 whose rules are not modi¯ed.
De¯nition 7. Let P = (P1; P2) be a pair of logic programs over LP such that the number of clauses in P1 that are not constraints is n. Let L¤P = LP [ A where A is a set of n new abducible atoms, namely A = fai; 1 · i · n j ai is an atom, ai 62 LP and ai 6= aj if i 6= jg. We de¯ne the update logic program P¯ = P1 ¯ P2 over L¤P, as the program consisting of the following clauses: 1. all constraints in P1, 2. we add the clause a à B+ [ :(B¡ [ faig) if ri = a à B+ [ :B¡ 2 P , 1 · i · n and ai 2 A, 3. all clauses r 2 P2.
We de¯ne the abductive logic program of P as follows: T¯ = hP¯; Ai.
In this way, the intended ¯-update p-stable models of a pair of logic programs P = (P1; P2) are obtained by removing the abducible atoms from the MG p-stable models of T¯. Finally, the ¯-update p-stable models are chosen as those that contain more information, i.e. maximal in the sense of inclusion of sets, from the intended ¯-update p-stable models.
De¯nition 8. Let P = (P1; P2) be an update pair over LP and T¯ its abductive logic program. Then, M µ LP is an intended ¯-update p-stable model of P if and only if M = M 0 \ LP for some MG p-stable model M 0 of T¯. In case M is an intended ¯-update p-stable model of P and is maximal among all intended ¯update p-stable model of P w.r.t. inclusion order, then M is an ¯-update p-stable model of P.
We can illustrate our semantics with the following example.
Example 5. Let P = (P1; P2) be an update pair over LP = fa; bg where, P1 and P2 are the following logic programs, P1 = fb Ã; a à bg and P2 = f¡a Ãg. We can see that the update logic program P¯ = P1 ¯ P2 over L¤P corresponds to the program P of Example 4 where the xi are the abducible ai. The intended ¯-update p-stable models of P are f¡ag and f¡a; bg; and its only ¯-update p-stable model is f¡a; bg.
Now, we show that our update operator (¯) satis¯es several formal properties.
These properties have been deeply analyzed, in the context of stable semantics,
by several authors such as J. J. Alferes et al. in [
The following two de¯nitions are used to de¯ne the last of our properties. Given A = fA1 : : : Ang where the Ai, 1 · i · n are sets, and B = fB1 : : : Bmg where the Bj , 1 · j · m are sets, we de¯ne A ] B = fAi [ Bj j Ai 2 A and Bj 2 Bg.
De¯nition 9. Let P = (P1; P2) be a pair of logic programs over LP. We de¯ne the update semantic function of P as follows:
SEM¯(P)5 = fM j M is an ¯-update p-stable model of Pg:
Now we de¯ne the properties. Since the intuition behind the ¯rst six properties is easy, hence we only give a deeper explanation about the last property below. P1. Initialisation: If P is a logic program then ; ¯ P ´ P .
P2. Strong consistency: Let P1 and P2 be logic programs. Suppose P1 [ P2 has at least one p-stable model. Then P1 ¯ P2 ´ P1 [ P2.
P3. Idempotence: If P is a logic program then P ¯ P ´ P .
P4. Weak noninterference: If P1 and P2 are logic programs de¯ned over disjoint alphabets, and both of them have p-stable models or do not, then P1 ¯ P2 ´ P2 ¯ P1.
P5. Weak irrelevance of syntax: Let P , P1 and P2 be logic programs under LP.
If P1 ´SE P2 then P ¯ P1 ´ P ¯ P2.
P6. Augmented update: Let P1 and P2 be logic programs such that P1 µ P2.
Then P1 ¯ P2 ´ P2.
P7. Independent parts property. Let P1 = (P1; P10) and P2 = (P2; P20) such that
(LP1 \LP2 ) = ;. Then SEM¯((P1[P2); (P10[P20)) = SEM¯(P1)]SEM¯(P2):
Property P7 indicates that our update operator does not violates the general
principle that completely independent parts of a logic program should not
interfere with each other. Hence the property P7 of operator ¯ indicates that if we
update the union of a pair of logic programs (P1 [ P2) by the union of a di®erent
pair of logic programs (P10 [ P20) such that P1 and P10 are de¯ned under a di®erent
language from the language of logic programs P2 and P20 then, the result can be
also obtained from a particular union of the update of P1 by P10 and the update
of P2 by P20. This particular union of updates corresponds to our De¯nition 9.
Example 6. [
Let P1 be: openSchool à : holiday à :workday: Let P2 be:
seeStars à :
Let P10 be: ¡openSchool à holiday: workday à :holiday: Let P20 be: ¡seeStars à : Let P1 = (P1; P10), P2 = (P2; P20), and P = ((P1 [ P2); (P10 [ P20)). We can see that (LP1 \ LP2 ) = ;. According to independent parts property we have that, SEM¯((P1 [ P2); (P10 [ P20)) = SEM¯(P1) ] SEM¯(P2) since SEM¯((P1 [ P2); (P 0
1[P20)) = ffopenSchool; workday; ¡seeStarsgg = ffopenSchool; workdaygg] ff¡seeStarsgg = SEM¯(P1) ] SEM¯(P2): Theorem 1. The update operator (¯) satis¯es properties, P1, P2, P3, P4, P5, P6, and P7.
Proof. First, it is straightforward to verify that given a p-stable consistent program P , if M is p-stable model of P then there is not another p-stable model M 0 of P such that M 0 ½ M . So, by this last fact and by Lemma 2, it is also straightforward to verify that given an abductive logic program hP; Ai, where P is p-stable consistent, then if M is a MG p-stable model of hP; Ai then there is not another MG p-stable model M 0 of hP; Ai such that M 0 ½ M . (P1. Initialisation): ; ¯ P = P by construction. Hence ; ¯ P ´ P . (P2. Strong consistency): Let Q = (P1 [P2) such that Q is p-stable consistent. Let P be the update (P1; P2). We must prove that M is an ¯-update p-stable model of P i® M is a p-stable model of Q.
Let us notice that programs Q and P¯ have the same clauses except for some of them, namely in P¯ there are some clauses that have an abducible atom (a new atom) in their body and these atoms do not occur in Q. So when we apply iteratively Lemma 1, two things are certain: (1) S is a p-stable model of Q, i® S is also a p-stable model of P¯, and (2) if Q is p-stable consistent, then P¯ is p-stable consistent too. ()) By hypothesis M is an ¯-update p-stable model of P, then by De¯nition 8, there exists a MG p-stable model M 0 of the abductive logic program of P, hP¯; Ai, such that M = M 0 \ LP. Then by De¯nition 6, there exists ¢, ¢ µ A such that hM 0; ¢i is a MG p-stable model of hP¯; Ai, where M = M 0 \ LP. By hypothesis, Q is p-stable consistent then, by (2) P¯ is p-stable consistent too. Hence applying Lemma 2, it is possible to verify that ¢ = ; and M 0 = M . So hM; ;i is a MEG p-stable model of hP¯; Ai. Finally by De¯nition 5, M is a p-stable model of P¯. Thus by (1) we have that M is a p-stable model of Q. (() Let M be a p-stable model of Q. By (1), M is a p-stable model of P¯. By Lemma 2, M is a MG p-stable model of the abductive logic program of P, P ; Ai. By Lemma 2, M \ A = ;. Hence by De¯nition 8, M is an ¯-update h ¯ p-stable model of P. (P3. Idempotence): If P does not have p-stable models, then neither does P ¯ P . If P has p-stable models, then P [ P does, hence by Strong Consistency, P [ P ´ P ¯ P . Hence in each case P ¯ P ´ P . (P4. Weak noninterference): If each of P1 and P2 lacks of p-stable models then the update (in any order) lacks of p-stable models. If P1 and P2 have pstable models, then P1 [ P2 does too | because they are de¯ned over disjoint alphabets. By Strong Consistency, P1 [ P2 ´ P1 ¯ P2. Also P2 [ P1 ´ P2 ¯ P1. Hence, P1 ¯ P2 ´ P2 ¯ P1. (P5. Weak irrelevance of syntax): Let P , P1, and P2 be logic programs models. Hence, P ¯ P1 ´ P ¯ P2. under the same language L. Since P1 ´SE P2, then for every program P , P [ P1 is strongly equivalent to P [ P2. Thus, (P [ A) [ P1 and (P [ A) [ P2 have exactly the same p-stable models. Thus, P ¯ P1 and P ¯ P2 have exactly the same EG p-stable models. Therefore, P ¯P1 and P ¯P2 have exactly the same MG p-stable in each case P1 ¯ P2 ´ P2. (P6. Augmented update): If P2 does not have p-stable models, neither does P1 ¯ P2. If P2 has at least one p-stable model and P1 µ P2 then, (P1 [ P2) has at least one p-stable model too. By strong consistency P1 ¯ P2 ´ P1 [ P2. Hence (P7. Independent parts): Let P1 = (P1; P10), P2 = (P2; P20) such that (LP1 \ LP2 ) = ;, and P = ((P1 [ P2); (P10 [ P20)). Let M1 and M2 be a ¯-update p-stable model of P1 and a ¯-update p-stable model of P2 respectively. It is clear that M1 and M2 are disjoint, since (LP1 \ LP2 ) = ; ¯-update p-stable model of P i® M = M1 [ M2. it is minimal. By De¯nition 5, M 0 is a p-stable model of P ()) By De¯nition 8, if M is a ¯-update p-stable model of P, then there exists M 0, a MG p-stable model of hP¯; Bi, such that M = M 0 \ LP. Then by De¯nition 6, there exists ¢, ¢ ½ B such that hM 0; ¢i is a EG p-stable model of hP¯; Bi and ¯ [ ¢.
Moreover, since (LP1 \ LP2 ) = ;, we can verify the following: . We have to prove that M is a (1) P
¯ = P1¯ [ P2¯6, (2)¢ = ¢1 [ ¢2 such that ¢1 = ¢ \ LP1 , ¢2 = ¢ \ LP2 and ¢1 \ ¢2 = ;, (3)M 0 = M10 [ M20 such that M10 is a p-stable model of P1¯ [ ¢1 and M20 is a p-stable model of P2¯ [ ¢2. as a p-stable model of P2¯ [ ¢2.
P1¯ and B2 is the set of abducible atoms of P2¯.
Now by De¯nition 5, hM10 ; ¢1i is a MEG p-stable model of hP1¯; B1i and hM20 ; ¢2i is a MGE p-stable model of hP2¯; B2i where B1 is the set of abducible atoms of models of P1 and P2 respectively.
Finally by De¯nition 8, M1 = M10 \LP1 and M2 = M20 \LP2 are ¯-update p-stable that P (() This proof is similar to the proof of the ¯rst part above. Taking into account ¯ = P1¯ [ P2¯; and if ¢ = ¢1 [ ¢2 then there exists a p-stable model M 0 = M10 [ M20 of P ¯ [ ¢ such that M10 as a p-stable model of P1¯ [ ¢1 and M20 tu 5
Our approach for update logic program is based on the concept of Minimal generalized p-stable models, and we also present properties that our update operator satis¯es. A comparative study of our semantics and other updates semantics will be realized as future work.
This research has been supported by the Fondo Sectorial SEP-CONACyT, Ciencia B¶asica Project (Register 101581).