Introduction

Currently, is a promising approach to model features of commonsense reasoning. In order to formalize NMR the research community has applied monotonic logics. In [7], Gelfond and Lifschitz defined the stable model semantics by means of an easy transformation. The stable semantics has been successfully used in the modeling of non-monotonic reasoning (NMR). Additionally, Pearce presented a characterization of the stable model semantics in terms of a collection of logics in [20]. 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 construction used by Pearce is called a weak completion.

In [14], a new semantics for normal programs based on weak completions is defined with a three valued logic called G 3 logic. The authors call it the Pstable semantics. In [12], the authors define the p-stable semantics for disjunctive programs by means of a transformation similar to the one used by Gelfond and Lifschitz in their definition of the stable semantics. The authors also prove that the p-stable semantics for disjunctive programs can be characterized by means of a concept called weak completions and the G 3 logic, with the same two conditions used by Pearce to characterize the stable semantics of disjunctive programs, that is to say, for normal programs it coincides with the semantics defined in [14]. In fact, a family of paraconsistent logics studied in [12] can be used in this characterization of the p-stable semantics.

In [13], the authors offer an axiomatization of the G 3 logic along with a soundness and completeness theorem, i.e., every theorem is a tautology and vice-versa. We also remark that the authors of [12] present some results that give conditions under which the concepts of stable and p-stable models agree. They present a translation of a disjunctive program D into a normal program N , such that the p-stable model semantics of N corresponds to the stable semantics of D when restricted to the common language of the theories. Besides, they show that if the size of the program D is n then the size of the program N is bounded by An 2 for a constant A. The relevance of this last result is that it shows 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.

One major recent result of the p-stable semantics is in the context of argumentation theory [6], which explores ways to carry out into the theory of computation the mechanisms humans use in argumentation. The three major semantics of argumentation theory (grounded, stable, and preferred) can be characterized in terms of three logic programming semantics: the well founded semantics [22], the stable semantics [7] and the p-stable semantics, respectively in terms of a unique normal logic program P , that is constructed only in terms of the argumentation framework AF [3]. Argumentation theory does not depend on a particular semantics. Then, if we want to obtain the stable semantics of AF , we compute the stable semantics of logic programming over P AF . If, on the other hand, we want to obtain the preferred semantics of AF , we compute the p-stable semantics over P AF . Moreover, if we want to obtain the grounded semantics of AF , we compute the well founded semantics over P AF .

There are also initial work about other two approaches for knowledge representation based on the p-stable semantics: updates, and preferences. In case intelligent agents get new knowledge and this knowledge must be added or updated to their knowledge base, it is important to avoid inconsistencies. An update semantics for update sequences of programs based on p-stable semantics is proposed in [15]. The concept of preferences is considered a vital component of reasoning with real-world knowledge. In [16], the authors introduce preference rules which allow us to specify preferences as an ordering among the possible solutions of a problem. Their approach allow us to express preferences for arbitrary programs. They also define a semantics for those programs. The formalism used to develop their work is p-stable semantics.

It is important to mention that the p-stable semantics, which can be defined in terms of paraconsistent logics, shares several properties with the stable semantics, but is closer to classical logic. For example, the following program P = {a ← ¬b, a ← b, b ← a} does not have stable models. However, the set {a, b} could be considered the intended model for P in classical logic. In fact, it is the only p-stable model of P .

In [18], a schema for the implementation of the p-stable semantic using two well known open source tools: Lparse and Minisat is described. In [18], a prototype1 written in Java of a tool based on that schema is also presented. In this paper we present an implementation of the p-stable semantics implementation with aim to improve the implementation presented in [18], considerable effort has been made in the optimization the code and in the design of the algorithms used, which are theoretically more efficient than those used in [18]. As this implementation started recently, we have not yet made definitive tests to warrantee that the solver is error-free, nor we can give conclusive comparative tests between our implementation and that on [18].

In the section 2 the basic concepts about the p-stable semantics are introduced, specially the transformations. In the section 3 are presented the algorithms used to apply the transformations. In the section 4 and 5 is explained how to construct the graph of dependencies of the program and how this graph is used to reduce the search space when looking for the p-stable models.

Background

In this section, we define some basic concepts in terms of logic programming semantics, including the definitions of the transformations, which are used to simplify a program.

Syntax

A signature L is a finite set of elements that we call atoms. A literal is either an atom a, called positive literal, or the negation of an atom ¬a, called negative literal. Given a set of atoms {a 1 , ..., a n }, we write ¬{a 1 , ..., a n } to denote the set of atoms {¬a 1 , ..., ¬a n }. A normal clause or normal rule, r, is a clause of the form a ← b 1 , . . . , b n , ¬b n+1 , . . . , ¬b n+m .

where a and each of the b i are atoms for 1 ≤ i ≤ n + m, and the commas mean logical conjunction. In a slight abuse of notation we will denote such a clause by the formula a ← B + (r) ∪ ¬B − (r) where the set {b 1 , . . . , b n } will be denoted by B + (r), the set {b n+1 , . . . , b n+m } will be denoted by B − (r), and B + (r) ∪ B − (r) denoted by B(r). We use H(r) to denote a, called the head of r. We define a normal program P , as a finite set of normal clauses. If for a normal clause r, B(r) = ∅, H(r) is known as a fact . We write L P , to denote the set of atoms that appear in the clauses of P .

Semantics

From now on, we assume that the reader is familiar with the single notion of minimal model [8]. In order to illustrate this basic notion, let P be the normal program {a ← ¬b., b ← ¬a., a ← ¬c., c ← ¬a.}. As we can see, P has five models: {a}, {b, c}, {a, c}, {a, b}, {a, b, c}; however, P has just two minimal models: {b, c}, {a}. We will denote by M M (P ) the set of all the minimal models of a given logic program P . Usually M M is called minimal model semantics. Now we give the definition of p-stable model semantics for normal programs.

Definition 1. [19] Let P be a normal program and M be a set of atoms. We define the reduction of P with respect to M as RED(P, We say that two normal programs P and P are equivalent if and only if they have the same set of p-stable models, this relation is denoted by P ≡ P . An important theorem relating the p-stable and minimal models is the following. Theorem 1. [14] Let P be a normal program. If M ∈ P S(P ) then M ∈ MM(P ).

M ) = {a ← B + ∪¬(B − ∩ M )|a ← B + ∪ ¬B − ∈ P }.

Transformations preserving equivalence

The main purpose of the transformations presented in this section is to simplify the input normal program, reducing its size. What allows the use of those transformations under the p-stable semantics are the propositions proved in [17,4] about equivalence of normal programs under these transformations. Let P be a normal program, the definition of the transformations SUB, TAUT, RED − , RED + , SUCC, LOOP, NAF and EQUIV when applied to P is as follows Proposition 1. [17,4] Let P be a normal program, and let P be the resulting program from the application to P of any of the transformations SUB, TAUT, EQUIV, SUCC, RED + , RED − , NAF or LOOP. Then P ≡ P .

1. SUB(P ) = P \ {r } ⇐⇒ r ∈ P , ∃r ∈ P : r = r , B − (r ) ⊆ B − (r ), B + (r ) ⊆ B + (r ), H(r) = H(r ). 2. TAUT(P ) = P \ {r } ⇐⇒ r ∈ P , H(r ) ∈ B + (r ). 3. EQUIV(P ) = (P \ {r }) ∪ {r} ⇐⇒ r ∈ P, H(r ) ∈ B − (r ), B − (r) = B − (r ) \ {H(r )}, B + (r) = B + (r ), H(r) = H(r ). 4. SUCC(P ) = (P \ {r }) ∪ {r} ⇐⇒ r ∈ P, B − (r) = B − (r ), H(r) = H(r ),

Computing the p-stable models

Now we present the implementation of a p-stable model solver. To find the p-stable models of a program P we can first apply the transformations to P , however the application of the transformations is not absolutely necessary nor sufficient to find the p-stable models of P . In this section we start presenting the implementation of the application of the transformations, and then we give three approaches to find the p-stable models of P , one that follows from the theorem 1, and the others from the theorem 2 which is also presented in this section.

Implementing the transformations

Given a program P as input to the p-stable solver, we associate to each atom a ∈ L P three sets that are used for the application of the transformations, those sets are initialized as follows, With the information in those sets it is efficient the application of some transformations, because it is avoided the use of a search algorithm, for example, it will not be necessary to search through all the program P when we require all the rules whose head is a particular atom a. Each atom a ∈ L P also has associated a variable state(a), which can hold one of the following values (we refer to this variable as the state of a): if state(a) = state f act then a is a fact, if state(a) = state no f act then a can not be a fact, if state undef ined then we can not tell yet if a is or can not be a fact. The application of the transformations TAUT and EQUIV is easily implemented, and in this paper we do not write the algorithms that apply those transformations. The transformations SUCC, RED + , RED − , NAF and a particular case of SUB are applied iteratively by the algorithm transf ormations iterated(...). This particular version of SUB consists in deleting the rules whose head is a fact. For the general case of SUB it is necessary to check for set inclusion between the bodies of all pairs of rules with the same head, some of our experimental implementations showed that it was very inefficient and in most cases only a few rules were deleted. The LOOP transform was implemented using the Dowling-Gallier algorithm [5] (which finds the unique minimal model of a positive program in linear time) it is presented in the LOOP (...) algorithm. Also a watched variables scheme [9] might be used, this technique is effective in some cases when the deletion of atoms from rules needs to be continuously undone, but at this stage we do not need undo any changes.

For the algorithm transf ormations iterated(...) we need two lists (see the algorithm at the end of the paper), they are Lp and Lf , which have to be initialized before calling to transf ormations iterated(...). Lp is initialized with the atoms that are facts, then for all a ∈ Lp it is assigned state(a) = state f act. Lf initialized with the atoms a such that there is no rule with head a, then for all a ∈ Lf it is assigned state(a) = state no f act. In transf ormations iterated(...) the auxiliary algorithms remove rule(r) and remove atom f rom rule(a, r, B) are used. remove rule(r) removes the rule r and if all the rules with head H(r) have been removed, set state(H(r)) = state no f act and add a to Lf . remove atom f rom rule(a, r, B) removes the atom a from B, where B = B + (r) or B = B − (r), if after removing a from B, |B| = 0, then set state(H(r)) = state f act and add a to Lp

In the next example we illustrate how the algorithm transf ormations iterated(...) behaves with the program P as input Before starting the transf ormations iterated(...) algorithm, the EQUIV and TAUT transformations are applied obtaining Π 1 (this is an optional step), also Lp and Lf have to be initialized. Then we call transf ormations iterated(Π 1 ). In the first iteration d is removed from Lf , we apply NAF and RED + until d do not appear in the program, obtaining Π 2 . In the second iteration remove b from Lp then apply SUB by removing all the rules whose head is b, then SUCC and RED − are applied until b do not appear in the program, obtaining Π 3 . In the third iteration remove c from Lf , and apply NAF and RED + until c do not appear in the program obtaining Π 4 . In the fourth iteration remove a from Lf , and apply NAF and RED + until a do not appear in the program obtaining Π 5 . At this point Lp and Lf are empty making the algorithm stop.

During the execution of transf ormations iterated(P ) have been removed all the rules whose head is a fact, including the rules r for which B(r) = ∅, which are precisely the rules that indicate that H(r) is a fact, it does not represent any problem because we can recover the atoms that are facts just by gathering the atoms whose state is state f act. As the transformations applied preserve equivalence, P ≡ Π 5 ∪ {b ←}, we added the rule b ← to Π 5 because state(b) = state f act. The state of all the atoms that were added to Lp was set to state f act (in this case {b}), and the state of the atoms that were added to Lf was set to state no f act ({d, a, c}), it means that b must be in all the p-stable models of P and {d, a, c} can not be in any.

It is not hard to see that after the application of this algorithm we can no longer apply SUCC, RED − , RED + or NAF.

The graph of dependencies

In most cases the application of the transformations is not enough to find a p-stable model of a normal program, and other techniques are required. One of those techniques is to partition the program into sets of rules called modules. Those modules are created based on its graph of dependencies. Before explaining this technique in detail we give the next definition Definition 3. A strongly connected component C of a graph G is a subset of nodes of G. C is a maximal set of nodes(maximal respect to inclusion) such that there is a directed cycle in G that contains all the nodes in C.

When we have the rule a h ← a 1 , a 2 , ..., a m , not a m+1 , not a m+2 , ..., not a n ., a h is dependent of all the a i s, i = 1...n, in a graph this dependencies can be represented with the directed edges (a i , a h ), i = 1, ..., n. The graph of dependencies of a program P represents all the dependencies between the atoms in L P , given by all the rules of P .

The following definition states the definition of stratification and module of a program P . Definition 4. Let P be a normal program which can be partitioned into the disjoint sets of rules {P 1 , ..., P n }. Let P i , P j ∈ {P 1 , ..., P n }, P i = P j , we say that P i < P j if ∃r ∈ P j : ∃r ∈ P i : H(r ) ∈ B(r), if from this condition we do not conclude that P i < P j or P j < P i then we can choose to hold whether P i < P j or P j < P i as long as the following properties hold. For every X, Y, Z ∈ {P 1 , ..., P n }, the strict partial order relation properties and the totality property hold: Definition 5. Let P be a normal program, C i a strongly connected component of the graph of dependencies of P , and P i the module constructed from C i . We define h(P i , P ) as the atoms which are represented as nodes in C i .

Computing the p-stable models

The purpose of this section is to show how to compute the p-stable models of a program, three approaches to find the p-stable models of a program P are presented. One way is a direct application of the theorem 1, it consist in computing the minimal models of P and choosing those which satisfy the definition of p-stable model. By theorem 2 the p-stable models of P can be computed by computing the p-stable models of the modules of P after the application of certain transformations. Theorem 2. [19] Let P be a normal logic program, and M a model of P with stratification P = P 1 ∪ P 2 , then RED(P, M ) |= M iff RED(P 1 , M 1 ) |= M 1 and RED(P 2 , M 2 ) |= M 2 with P 2 , M 1 , and M 2 defined as follows:

M = M 1 ∪ M 2 , M 1 = h(P 1 , P ) ∩ M , M 2 =

h(P 2 , P ) ∩ M , and P 2 is obtained by transforming P 2 as follows:

1. Removing from P 2 the rules r such that

B − (r ) ∩ M 1 = ∅ or B + (r ) ∩ (h(P 1 , P ) \ M 1 ) = ∅, obtaining a new program P 2 . 2.

For every r ∈ P 2 , removing from B(r) the occurrences of the atoms in h(P 1 , P ), obtaining P 2 .

In other words M is a p-stable model of P iff M 1 is a p-stable model of P 1 and M 2 is a p-stable model of P 2 , where P 2 is obtained by removing from P 2 the occurrences of the atoms in h(P 1 , P ) according to the theorem 2. If P can be stratified as P = P 1 ∪ ... ∪ P n , n > 2, then P = P 1 ∪ Q with Q = P 2 ∪ ... ∪ P n is also an stratification of P that has only two modules, and then we can apply the theorem 2.

From theorems 1 and 2, three different approaches to compute the p-stable models of a program P are known. The first approach has been implemented in [18]. We propose the other two approaches that reduce the search space respecto to the first approach in many practical examples.

1. From theorem 1, it follows that in order to find the p-stable models of P , we can generate minimal models M ∈ MM(P ) and accept as p-stable models those for which the consequence test RED(P, M ) |= M is true. To implement the consequence test we take advantage of the fact that RED(P, M ) |= M ⇐⇒ RED(P, M ) ∪ {¬M } is unsatisfiable, to test if RED(P, M ) ∪ {¬M } is unsatisfiable it is used a SAT solver, in this case we used MINISAT [1], the consequence test is implemented in the algorithm consequence test(...)(not presented here for lack of space). Using this approach the search space to find the p-stable models of P is M M (P ). The computation of the p-stable models following this approach is implemented in new P S(...).

2. As we have said, if P can be stratified into n modules P = P 1 ∪ ... ∪ P n , then P can also be stratified into two modules P = P 1 ∪ Q, where Q = P 2 ∪ ... ∪ P n , n > 2, and now we can apply the theorem 2 to find the pstable models of P , this approach is based on the fact that Q (obtained from Q according to theorem 2) can be stratified as

Q = Q 2 ∪ ... ∪ Q n

where Q i , 2 ≤ i ≤ n is obtained by removing from P i the occurrences of L P1 according to theorem 2. If n > 3, to compute the p-stable models of Q , we argument the same way but now instead of P , we have Q with stratification

Q = Q 2 ∪ ... ∪ Q n .

We can proceed this way whenever we want to compute the p-stable models of a program stratified into more than two modules, when it only has two modules, we just apply the theorem 2. The search space to find all the p-stable models of a program P using this approach is in the worst case M M (P ), but sometime this search space is bigger than in the third approach. The advantage of this approach over the third approach is that it is not necessary to compute the stratification of a module before computing its p-stable models, we compute only once the stratification of P .

3. Again following the theorem 2, to compute a p-stable model of P with stratification P = P 1 ∪ P 2 (as we have said a program with n modules can also be stratified into two modules), we can compute a p-stable model of P 1 and one p-stable model of P 2 , and if P 2 can be stratified into

P 2 = Q 1 ∪ Q 2 ,

we can apply again the theorem and compute the p-stable models of Q 1 and Q 2 .

The difference with the second approach is that in the second approach the stratification is computed only once, and in this approach we compute the stratification with getM odules(...) each time we want to compute a p-stable model of a module. Using this approach the search space is in many cases considerably smaller than M M (P ), this is because the problem of finding the p-stable models of a program is translated into the problem of finding the p-stable models of many small subprograms, the smaller these subprogram, more chances are to reduce the search space. We distinguish between finding the first and the subsequent p-stable models, to find the first p-stable model use the f irst P S recursive(...) algorithm and to find the another p-stable model use next P S recursive(...).

We illustrate the second approach by finding the p-stable models of the program Π 5 that resulted from the application of the transformations in the example 1. In the graph 1 we see the graph of dependencies of Π 5 , the dotted edges trace maximal cycles, and determine the strongly connected components of Π 5 .

We encounter the two p-stable models of P 2 , {{x, u}, {x, v}}, from which we find another two p-stable models of Π 5 , {{t, x, u}, {t, x, v}}. When trying to generate another p-stable model of P 2 we can not find any so we go to P 1 , and can not find another p-stable model of P 1 so we stop. We end up with the four pstable models of Π 5 , PS(Π 5 ) = {{t, x, u}, {t, x, v}, {r, v, z}, {r, u}}. Recall form the example 1 that b was found to be a fact after the application of the transformations to P , for instance PS(P ) = {{b, t, x, u}, {b, t, x, v}, {b, r, v, z}, {b, r, u}}.

When using the third approach, we stratify Π 5 into Π 5 = P 1 ∪ P 2 as in the second approach, but after obtaining P 2 , try to stratify P 2 , we can see in the graph of dependencies of P 2 (graph 2), that P 2 can be stratified into two modules, so P 2 is stratified into P 2 = Q 1 ∪Q 2 which can be seen in the next figure

Q 1 ={ r 1 : u ← not v. r 2 : v ← not u.} Q 2 = { r 4 : x ← y. r 5 : y ← not x, z, not v. r 8 : z ← not u, not x.} Q 2 ={ r 4 : x ← y. r 8 : z ← not x.} R 1 ={} R 2 ={x ← y.} R 3 ={z ← not x.} R 2 ={} R 3 ={z ←.}

Applying again the theorem 2, first choose a minimal model of Q 1 , {v} and when doing the consequence test we find that {v} is a p-stable model of Q

1 . Now obtain Q 2 (see the anterior figure) which is further partitioned into Q 2 = R 1 ∪ R 2 ∪ R 3 which

are respectively the sets of rules with head y, x and z. Then compute a p-stable model of R 1 , the only p-stable model of R 1 is the empty set, R 2 is also empty and also has an empty p-stable model. R 3 (obtained by removing from R 3 the occurrences of L R1 and L R2 ) only has an empty rule z ← and its unique p-stable model is {z}. Merging the p-stable model of the modules P 1 , Q 1 , R 1 , R 2 and R 3 we get a p-stable model of Π 5 , it is {r} ∪ {v} ∪ {} ∪ {} ∪ {z} = {r, v, z}. When trying to generate another p-stable model, first we try to generate another p-stable model of R 3 , it does not have more p-stable models, thus we go back and try on R 2 but it has neither, then try on R 1 that has no more p-stable models, finally we find that Q 1 has another p-stable model, {u}, from this point, to find the other p-stable models of Π 5 , we proceed as we did when we had {v} as a p-stable model of Q 1 .

To show the performance of each approach we use some examples in [2]. In the next table we can see the time in seconds it took to find a p-stable model of some of those examples using each of the three approaches. A "-" character means that we stopped the execution after 10 seconds. In the fifth column is the time to find a stable model by smodels. The sixth and seventh columns show the number of atoms and rules of each test program. In the last column is the number of modules in which the program was initially partitioned. It is worth to mention that if we modify the consequence test(...) such that it always return true, instead of using tranf ormations iterated(...) we apply some similar reductions (see [10]), and if all the tautological rules like a ← b, not b, c are removed, then we end up with a stratified minimal model solver, a detailed description of our stratified minimal model semantics solver can be found in [10].

Conclusions and future work

Some preliminary tests to the p-stable solver presented in this paper, shows a bad performance respect to a stable semantics solver(smodels [11]), for big programs, due to the backtracking driven by the failure of the consequence test, one of the inconveniences of this implementation is that the search space is very big for some programs, research is needed to develop algorithms that reduce the search space or heuristics that show a good performance for some classes of programs.