We summarize the foundations and applications of the new semantics called p-stable and we show that it holds the important property of extending the WFS semantics.
The research community has long recognized the study of non-monotonic
reasoning (NMR) as a promising approach to model features of commonsense
reasoning. On the other hand, monotonic logics have been successfully applied as
a basic building block in the formalization of non-monotonic reasoning. In this
direction, Veloso et al. [
The stable semantics, which has been successfully used in the modeling
of non-monotonic reasoning, was introduced by Gelfond and Lifschitz [
In [
In [
We emphasize that the p-stable semantics presented here, is a two-valued
semantics that can be characterized by the three-valued logic G03. This semantics
should not be confused with the partial stable semantics de¯ned by Przymusinski
[
This work has two main contributions, the ¯rst one corresponds to a
summary about the foundations of the new semantics called p-stable which includes
its applications and its relationship with paraconsistent logics. The second one
corresponds to showing that the p-stable semantics holds the important
property of extending the well founded semantics (WFS) de¯ned in [
The structure of the paper is as follows: Section 2 tells about the foundations of the G03-stable semantics and some of its applications. Section 3 starts with basic background and de¯nitions of the G03-logic, the p-stable semantics, the X-stable semantics for any logic X and programs with variables. In section 4, we review how the well founded semantics (WFS) can be induced by a powerful method called a Con°uent LP-Systems CS [9]. Section 5 shows that the p-stable semantics extends the WFS semantics. Then, we present our conclusions. 2
Motivation of the G03-stable semantics This section is dedicated to review the p-stable semantics. We review its origins and foundations, its major known results, and some of its extensions. Although the contribution of this paper is not based on all the results presented in this section, we consider that it is worth to know more about the state of the art of this new semantics. 2.1
Origins and logical foundations of the G03-stable semantics
Recently, in [
One interesting feature of the G03-logic presented in [
The authors of [
Weak completions have been used by D. Pearce [
In a parallel way, the p-stable semantics of disjunctive programs can be
de¯ned in terms of weak completions of paraconsistent logics, in particular G03
[
We can say then, that two major classes of logics are successfully used to model NMR: constructive intermediate logics and paraconsistent logics. A well known semantics for modeling NMR is the stable semantics, which can be de¯ned in terms of Intermediate logics. This semantics provides a fairly general framework for representing incomplete information and for reasoning with it. The p-stable semantics, which can be de¯ned in terms of paraconsistent logics, shares several properties with the stable semantics, but is closer to classical logic. 2.2
[
One of the main results presented in [
The G03-stable semantics shares properties with the stable semantics, but is
closer to the semantics de¯ned by classical logic. Consider the normal program
P1 : fa à :bg.
The well known stable semantics by Gelfond et al. [
Now, let us consider the following program P2: fa à :b; a à b; b à ag.
P2 does not have stable models, but the set fa; bg is a model of P in classical logic. Indeed, this set is also the only G03-stable model of P2.
The main purpose of argumentation theory (Dung [
These results help to understand the close relationship between two successful approaches to non-monotonic reasoning: argumentation theory and logic programming with negation as failure. 2.3
In order to ¯nish this brief motivation, we consider the expressivity of p-stable semantics. We mention three di®erent approaches for knowledge representation based on this semantics: updates, preferences and argumentation (see previous section).
In case intelligent agents get new knowledge and this knowledge must be
used to update the knowledge base, it is important to avoid inconsistencies. An
update semantics for update sequences of programs based on G03-stable semantics
is proposed in [
The concept of preferences is considered a vital component of reasoning with
real-world knowledge. In [
Finally, we mention that the theory of the p-stable semantics is closely related to topics that have been active areas of research: The theory of paraconsistent logics, the theory of ground non-monotonic modal logics, and the theory of weak completions created by D. Pearce to characterize the stable semantics of disjunctive programs in terms of constructive intermediate logics.
Thus, the G03-stable semantics is one of several semantics de¯ned by a family of paraconsistent logics, all of which de¯ne the p-stable semantics when restricted to disjunctive programs. 3
Since the present work continues the study of the p-stable semantics, we review the background necessary to understand the de¯nition of the p-stable semantics. In this way, this section summarizes the G03 logic, however some di®erent results of the p-stable semantics are related to other logics; we present here some basic background about these logics. We also present some important de¯nitions useful to understand this work. 3.1
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: ^, _, Ã, : auxiliary symbols: (, ), where ^, _, Ã are 2-place connectives and : is a 1-place connective. Formulas are built up as usual in logic. If F is a formula we will refer to its signature LF as the set of atoms that occur in F . The formula F ´ G is an abbreviation for (F Ã G) ^ (G Ã F ). The formula A Ã B is just another way of writing B ! A. A literal is either an atom a, or the negation of an atom :a.
When a formula is constructed as a conjunction (or disjunction) of a set of literals `, F = V ` (or F = W `), we denote by Lit(F ) such set of literals. 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 noted just by: H Ã. In the case when the head of a clause is empty, the clause is called a constraint and is noted by: Ã B.
A normal clause is a clause of the form a à V(B+ [ :B¡) where a is an atom, and B+, B¡ are, possibly empty, sets of atoms. A disjunctive clause is a clause of the form W H à V(B+ [ :B¡) where H is a set of atoms, and B+, B¡ are, possibly empty, sets of atoms.
The symbol :, before one of such sets, denotes the conjunction of the negations of the atoms belonging to the set. Sometimes a disjunctive clause may be written as H Ã B+; :B¡ following typical conventions for logic programs, similarly for normal clauses. 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 that the program is also of that type. For instance a set of disjunctive clauses is a disjunctive program, a set of normal clauses is a normal program and so on.
For arbitrary programs, and proper subclasses, we will use HEAD (P ) to denote the set of all atoms occurring in the heads of the clauses of P .
Let P rogL be the set of all normal programs with atoms from the signature L. A partial interpretation based on a signature L is a disjoint pair of sets hI1; I2i such that I1 [ I2 µ L. A partial interpretation is total if I1 [ I2 = L.
Given two interpretations I = hI1; I2i, J = hJ1; J2i, we set I ·k J if, by de¯nition Ii µ Ji, i = 1; 2. Clearly ·k is a partial order. We may also see an interpretation hI1; I2i as a set of literals I1 [:I2. When we look at interpretations as sets of literals then ·k corresponds to µ.
A general semantics SEM is a function on P rogL which associates with every program a partial interpretation. Given a signature L and two semantics SEM1 and SEM2, we de¯ne SEM1 ·k SEM2 if for every program P 2 P rogL, SEM1(P ) ·k SEM2(P ). When SEM1 ·k SEM2, we say that SEM2 is an extension of SEM1.
Next, we proceed to give de¯nitions of the relevant logics and semantics. 3.2
3 The G03 logic is a 3-valued logic with truth values in the domain D = f0; 1; 2g where 2 is the designated value. The evaluation functions of the logic connectives are then de¯ned as follows: x ^ y = min(x; y); x _ y = max(x; y); the : and ! connectives are de¯ned according to the truth tables given in Table 1.
We de¯ne a tautology as any formula that takes only the designated value
2, regardless of what the truth values the atoms in the formula may take. We
will use the notation j=G03 A, to express the fact that A is a tautology in G03.
We must notice the subtle di®erence between the logic G03 and the best known
logic G3 due to GÄodel; the latter is de¯ned exactly by the same functions as
the former, except that the negation corresponding to the truth value 1 is 0.
As a consequence, whereas G03 accepts the principle of the excluded middle, G3
does not. An axiomatization for G03 is presented in [
One of the main results presented in [
We observe that the formula (:A ^ A) ! B is not a theorem in either of the two logics. This fact indeed makes these two logics paraconsistent. The G03 logic is strictly stronger than Cw, and both of them are strictly weaker than classical logic. In particular the formula B ! [(:B ^ A) ! C], where A,B and C are arbitrary formulas, which is a tautology in classical logic, is not always a tautology in G03, as is seen in the particular case when A, B, C take the truth values of 2,1 and 0 respectively. As a useful result we also mention that the formula (:A ! A) ! A is a tautology in the G03 logic for any formula A. Intuitionistic logic, that we abbreviate as I, is de¯ned as positive logic plus the following two axioms: (A ! B) ! [(A ! :B) ! :A] and :A ! (A ! B). These two axioms allow to do proofs by contradiction but in some limited way; other constructions such as the law of the excluded middle: (A _ :A), are not valid in intuitionistic logic; however the formula (:A ^ A) ! B is valid in this logic. All of these properties are shared with the logic G3 mentioned before; in fact, G3 is stronger than I in the sense that any theorem in I is also a theorem in G3.
Notice the opposite situation occurring between intuitionistic and G3 logics,
and the paraconsistent logics Cw and G03 regarding the last two formulas above;
as it was mentioned before, the ¯rst one is valid in Cw and G03, but the second
one is not. See van Dalen [
As a known fact, we observe that the ¯rst two axioms of positive logic guarantee the deduction theorem, namely: for ¡; A; B, where ¡ is a set of formulas, and A; B are formulas: ¡; A ` B if and only if ¡ ` A ! B. 3.3
p-stable semantics
From now on we assume that the reader is familiar with the notion of classical
minimal model, Lloyd [
Here we de¯ne the p-stable semantics for disjunctive programs.
De¯nition 1. [
For convenience and to be consistent with the de¯nition of a semantics SEM as a function on P rogL which associates with every program a partial interpretation, from now on, we denote a p-stable model M of a disjunctive program P as a pair hM; LP n M i. We know, that this is not a standard way to represent the p-stable semantics, however this will be useful to present the contribution of this paper.
The following examples illustrate how to obtain the p-stable models of di®erent programs. Our ¯rst example shows a disjunctive program with two p-stable models.
Example 1. Let P be the disjunctive program:fa _ b à :c; a à c; b à :c; c à :bg: Let M1 = fbg and M2 = fa; cg. Both sets model (in classical logic) the rules of P . From the de¯nition of the RED transformation we ¯nd that RED(P; M1) = fa _ b Ã; a à c; b Ã; c à :bg and RED(P; M2) = fa _ b à :c; a à c; b à :c; c Ãg: It is clear that RED(P; M1) j= M1 and RED(P; M2) j= M2. Hence hM1; fa; cgi and hM2; fbgi are p-stable models for P .
The next example shows a program with a single p-stable model, which is also a classical model.
Example 2. Let P be the normal program: q à :q: Let us take M = fqg then RED(P; M ) is the following program: q à :q: 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 for P .
Our third example shows a program which has several classical models but has no p-stable models.
Example 3. Let P be the normal program: fa à :b; b à :c; c à :ag. It is clear that the sets M1 = fa; bg; M2 = fa; cg; M3 = fb; cg; M4 = fa; b; cg are all models of P in classical logic. However, they are not p-stable models of P . If we apply de¯nition 2 to M4, we have RED(P; M4) = P and M4 models P in classical logic, however RED(P; M4) 6j= M4. If we apply de¯nition 2 to M1, we obtain RED(P; M1) as the following program: fa à :b; b Ã; c à :ag and it is clear that M1 models in classical logic each of the rules of P . However, the second condition in de¯nition 2 is not satis¯ed, since RED(P; M1) 6j= a: By symmetry the same result is obtained for M2 and M3. Hence, the program does not have p-stable models.
Finally, we present a program which has no stable models and whose p-stable and classical models are the same.
Example 4. Let P be the normal program: fa à :b; a à b; b à ag. We can verify that M = fa; bg models the rules of P in classical logic. From the de¯nition of the RED transformation, we ¯nd that RED(P; M ) = P . Now, from the ¯rst and third rule, 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 P j= M . Therefore, M is a p-stable model of P . 3.4
Now we review a characterization of the p-stable semantics for disjunctive programs in terms of the G03 logic. First we present some useful de¯nitions.
Given a program P and a set of atoms M µ LP , we call the construct P [ :M c a weak completion of the program P (with respect to the set of atoms M ), where the superscript c, denotes set theoretical complement operator with respect to LP .
De¯nition 3. Let P be any theory, X be any logic and M be a set of atoms. M is a X-stable model of P if the next two conditions hold: `X P [ :M c ! M and M is a classical model of P .
The expression appearing in the ¯rst condition of this de¯nition is interpreted as the formula where the antecedent is the conjunction of all rules in P and all literals in :M c, and the consequent is the conjunction of all the atoms in M . We will keep using this interpretation in what follows.
Of particular interest to us is the G03-stable semantics, which is the result of
using the logic G03 in the previous de¯nition. For more details see [
Theorem 1 gives a characterization of the p-stable semantics for disjunctive
programs in terms of the G03 logic. This result was ¯rst proven for normal
programs in [
Theorem 1. [
As can be seen, p-stable models are de¯ned for propositional logic programs only.
However this de¯nition can be extended to predicate programs, which allows the
use of predicate symbols in the language, but without function symbols to ensure
the ground instance of the program to be ¯nite. So a term can only be either
a variable or a constant symbol. The ground instance of a predicate program
P , Ground (P ), is de¯ned in Lifschitz [
The following section review the WFS semantics in order to show that the pstable semantics holds the important property of extending the WFS semantics. Since the de¯nition of WFS for normal programs is unique and has been accepted by the research community, as opposed to the case of disjunctive programs, from now on we deal exclusively with normal propositional logic programs. 4
WFS and
WFS+ semantics In this section we review how the well founded semantics (WFS) can be induced by a powerful method called a Con°uent LP-System CS [9]. This method does not only characterize well-known semantics for logic programs but can be used to de¯ne new semantics. Roughly speaking, a semantics for a class of logic programs determines the set of derivable literals for each program P . The method of determining such a semantics is to rewrite the program P according to certain rewriting rules until we arrive at a normalform of the original program from which we can immediately read o® the derivable literals. Suitable sets for rewriting rules correspond to di®erent normalforms and thus to di®erent semantics.
The theory of Con°uent LP-Systems CS [9] combines methods from rewriting systems with logic programming technology to de¯ne a powerful framework for investigating the semantics of logic programs. The starting point of this theory is to determine a set of rewriting rules that is con°uent and that computes the semantics in a canonical way. These rules transform programs into simpler programs. Con°uence and termination guarantee that every program has associated with it a normalform. This normalform then induces a semantics and a simple and e±cient method to answer queries with respect to this semantics.
It is important to note that Con°uent LP-Systems CS correspond to a general theory, i.e., the concept is not attached to any particular semantics. [9] shows how most of the classical semantics such as Fitting's 3-valued version of Clark's completion, the wellfounded semantics WFS and Schlipf's extension WFS+ can be de¯ned as a Con°uent LP-System in a natural way.
The following de¯nition plays an important role to de¯ne the semantics of a normal program based on the notion of a rewriting system [9].
De¯nition 4. [9] For any normal program P we de¯ne SEMmin(P ) = hP true; P falsei where P true := fp j p à 2 P g, P false := fp j p 2 LP n HEAD(P )g.
Now we de¯ne a rewriting system, normalform, and some properties of rewriting systems.
De¯nition 5. [9] An abstract rewriting system is a pair hS; !i where ! is a binary relation on a given set S. Let !¤ be the re°exive, and transitive closure of !. When x !¤ y we say that x reduces to y. An irreducible element is said to be in normalform. We say that a rewriting system is noetherian: If there is no in¯nite chain x1 ! x2 ! : : : ! xi ! xi+1 ! : : :, where for all i the elements xi and xi+1 are di®erent, con°uent: If whenever u !¤ x and u !¤ y then there is a z such that x !¤ z and y !¤ z.
In a noetherian and con°uent rewritten system, every element x reduces to a unique normalform that we denote by norm(x) [9].
The main concept on which the notion of a Con°uent LP-Systems CS is based, is the concept of a transformation rule.
De¯nition 6. [9] A transformation rule is a binary relation on P rogL. Let a program P 2 P rogL be given. We de¯ne the following transformation rules. RED+: This transformation can be applied to P , if there is an atom a which does not occurs in HEAD(P ). RED+ transforms P into the program where all occurrences of :a are removed.
RED¡: This transformation can be applied to P , if there is a rule a à 2 P . RED¡ transforms P into the program where all clauses that contain :a in their bodies are deleted.
SUB (Subsumption): This transformation can be applied to P , if P contains two clauses a à body1, a à body2 where body1 µ body2. SUB transforms P into the program where the clause a à body2 has been removed.
Success: Suppose that P includes a fact a à and a clause q à body such that a 2 body. Then we replace the clause q à body by q à body n f g a .
Failure: Suppose that P contains a clause q à body such that a 2 body and a 62 HEAD(P ). Then we erase the given clause.
LC (Logical consequence): Suppose P j= a for an atom a. Then we can add the rule a à to P .
Loop: We say that P2 results from P1 by Loop w.r.t. A if, by de¯nition, there is a set A of atoms such that 1. for each rule a à body 2 P1, if a 2 A, then body \ A = ;, 2. P2 := fa à body 2 P1 j body \ A = ;g, 3. P1 6= P2.
Although these transformation rules are not really functions on P rogL (e.g. RED¡ is only determined if an occurrence of a certain rule is distinguished), they induce a set of operators on P rogL [9]. An operator, denoted as op, is a function over the set of programs that transforms a program P into a program P op as follows. If C1, C2 are clauses, g is a literal and f is an atom, then op can be of type
Red+, then P op is the reduction of P with respect to C1 and g. We write hRED+; C1; gi [9].
We could de¯ne in a similar way the operators for the other transformations. Example 6. [9] If P is fc à :dg and op1 is hRED+; :d Ã; c à :di then P op1 is fc Ãg. If op2 is hRED+; c à :d; :ci then P op2 = P .
Next, we give the de¯nition of Con°uent LP-System CS.
De¯nition 7. [9] A Con°uent LP-System CS over the signature L is a pair hfopi j i = 1; : : : ; ng; !i that satis¯es the following conditions: 1. fopi j i = 1; : : : ; ng is a ¯nite set of transformation rules on P rogL. By abuse of language we often view them as (computable) operators as we explained before. 2. hP rogL; !i, where ! is the union of all the transformation rules in CS, is a noetherian and con°uent rewriting system. 3. If P ! P1 then SEMmin(P ) ·k SEMmin(P1).
We denote the uniquely determined normalform of a program P with respect to the Con°uent LP-System CS by normCS (P ) [9].
Every Con°uent LP-System CS induces a semantics SEMCS as follows [9]: SEMCS (P ) := SEMmin(normCS (P )).
Now, we present a Con°uent LP-System CS1 used to compute the WFS
semantics in quadratic time and introduced in [
The Con°uent LP-System CS1 induces the WFS semantics.
Theorem 2. [9] The WFS semantics is the semantics induced by the Con°uent LP-System CS1.
The W F S+ semantics is an extension of WFS introduced in [8]. We present
a Con°uent LP-System CS2 used to compute the W F S+ semantics given in [
The Con°uent LP-System CS2 induces the W F S+ semantics.
Theorem 3. The WFS+ semantics is the semantics induced by the con°uent LP-system CS2.
Example 7. Let us obtain the WFS+ semantics of a normal program. Let us P = f P = f consider the program P : f
a à b; a à :b; b à ag. Applying LC we add the rule a à to P and we obtain f
a Ã; a à b; a à :b; b à ag. Since the last program includes the fact a à and the rule b à a, we can apply Success and obtain: fa Ã; a à b; a à :b; b Ãg. Applying Success again we obtain: a Ã; a à :b; b Ãg. Finally, we can delete a à :b applying RED¡: a Ã; b Ãg. Then the normCS2 (P ) = f a Ã; b Ãg. Thus the WFS+ semantics of P is SEMCS2 (P ) = SEMmin(normCS2 (P )) = hfa; bg; ;i. 5
hM; LP n M i.
Here, we show that the p-stable semantics extends the WFS+ and specially the
WFS semantics. These results are based on the fact that the p-stable semantics
for disjunctive and in particular for normal programs is invariant under each of
the transformations that de¯ne the Con°uent LP-Systems CS1 and CS2 [
The following theorem indicates that the p-stable semantics is consistent with the WFS+ semantics.
Theorem 4. Let P be a normal program. Let hT; F i be the model of P in the WFS+ semantics. If hM; LP n M i is a p-stable model of P then hT; F i ·k of each of the programs P; P1; : : : ; Pn.
SEMmin(P ) ·k SEMmin(P1) ·k : : : ·k SEMmin(Pn) = W F S+(P ). Proof. Let P ! P1 ! : : : ! Pn be the chain of reductions in the Con°uent LP-System CS2 that leads to the normalform Pn = normCS2 (P ). Then we have
Since the p-stable semantics is invariant under any of the transformations that de¯ne the Con°uent LP-System CS2, then hM; LP n M i is a p-stable model LP n M . Thus we have hT; F i ·k hM; LP n M i.
For any fact a à 2 P , it follows that a 2 M according to remark 1, hence T µ M . By the same remark 1, M ½ HEAD(Pn), therefore LP n HEAD(Pn) ½ tu
Since the p-stable semantics is an extension of WFS+ and WFS+ is an extension of WFS, a corollary of theorem 4 indicates that the p-stable semantics is also an extension of WFS semantics.
Corollary 1. Let P be a normal program. Let hT; F i be the model of P in the WFS semantics. If hM; LP n M i is a p-stable model of P then hT; F i ·k Proof. All transformations that de¯ne the WFS semantics are contained in those that de¯ne the WFS+ semantics. Let P ! P1 ! : : : ! Ps be a chain of reductions that leads to the normalform Ps = normCS1 (P ). This chain can be extended to P ! P1 ! : : : ! Ps : : : ! Pn so that Pn = normCS2 (P ), where n ¸ s.
Then the result follows from Theorem 4.
Then we have SEMmin(Ps) ·k SEMmin(Pn), i.e., SEMCS1 (P ) · SEMCS2 (P ). tu 6
We showed that the p-stable semantics extends the well known WFS semantics. This result is based on the fact that WFS can be induced in a natural way by a con°uent LP-system, which is based on certain transformations rules; and on the fact that the p-stable semantics for normal programs is invariant under each of these transformations. 1. A. Avron.
Natural 3-valued logic characterization and proof theory. J. Symb. Logic, 56(1):276{294, 1991.
Arti¯cial Intelligence, 171(10-15):619{641, 2007. 2. T. J. M. Bench-Capon and P. E. Dunne. Argumentation in arti¯cial intelligence. 538, 2001. The Logical Way to the Inconsistent, Proceedings of the Second World Congress on Paraconsistency (WCP 2000), number 228 in Lecture Notes in Pure and Applied Mathematics, pages 1{94. Marcel Dekker, Inc., 2002. 7. N. da Costa. On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic, 15(4):497{510, 1974. grams. In KR, pages 591{602, 1992.
Logic, 108(1{3):153{188, 2001. 8. J. Dix. A framework for representing and characterizing semantics of logic pro9. J. Dix, M. Osorio, and C. Zepeda. A General Theory of Con°uent Rewriting Systems for Logic Programming and its applications. Annals of Pure and Applied