In this paper we review some theoretical results about the p-stable semantics, and based on that, we design some algorithms that search for the p-stable models of a normal program. An important point is that some of these algorithms can also be used to compute the strati ed minimal models of a normal program.
Currently, is a promising approach to model features of commonsense reasoning.
In order to formalize NMR the research community has applied monotonic logics.
In [
In [
In [
One major recent result of the p-stable semantics is in the context of
argumentation theory [
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 [
It is important to mention that the p-stable semantics, which can be dened in terms of paraconsistent logics, shares several properties with the stable semantics, but is closer to classical logic. For example, the following program P = fa :b; a b; b ag does not have stable models. However, the set fa; bg could be considered the intended model for P in classical logic. In fact, it is the only p-stable model of P .
In [
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. 2
2.1
In this section, we de ne some basic concepts in terms of logic programming semantics, including the de nitions of the transformations, which are used to simplify a program.
A signature L is a nite 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 fa1; :::; ang, we write :fa1; :::; ang to denote the set of atoms f:a1; :::; :ang. A normal clause or normal rule, r, 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, 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 fb1; : : : ; bng will be denoted by B+(r), the set fbn+1; : : : ; bn+mg 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 de ne a normal program P , as a nite set of normal clauses. If for a normal clause r, B(r) = ;, H(r) is known as a fact . We write LP , to denote the set of atoms that appear in the clauses of P . 2.2
From now on, we assume that the reader is familiar with the single notion of
minimal model [
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 de nition of p-stable model semantics for normal programs.
De nition 1. [
De nition 2. [
We say that two normal programs P and P 0 are equivalent if and only if they
have the same set of p-stable models, this relation is denoted by P P 0. An
important theorem relating the p-stable and minimal models is the following.
Theorem 1. [
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 [
B+(r0); H(r) = H(r0). 2. TAUT(P ) = P n fr0g () r0 2 P , H(r0) 2 B+(r0). 3. EQUIV(P ) = (P n fr0g) [ frg () r0 2 P; H(r0) 2 B (r0); B (r) = B (r0) n fH(r0)g; B+(r) = B+(r0); H(r) = H(r0). 4. SUCC(P ) = (P n fr0g) [ frg () r0 2 P; B (r) = B (r0); H(r) = H(r0); 9r00 2
P : B(r00) = ;; H(r00) 2 B+(r0); B+(r) = B+(r0) n fH(r00)g. 5. RED+(P ) = (P n fr0g) [ frg () r0 2 P; B+(r) = B+(r0); H(r) = H(r0); 9a 2
LP : a 2 B (r0); B (r) = B (r0) n fag; 6 9r00 2 P : H(r00) = a: 6. RED (P ) = P n fr0g () r0 2 P; 9r00 2 P : B(r00) = ;; H(r00) 2 B (r0). 7. NAF(P ) = P n fr0g () r0 2 P; 9a 2 LP : a 2 B+(r0); 6 9r00 2 P : H(r00) = a. 8. LOOP(P ) = fr0 : r0 2 P; B+(r0) M g, where M is the unique minimal model of MM(POS(P )). The de nition of POS(P ) is given by
POS(P ) = fr0 : B (r0) = ;, 9r 2 P : B+(r) = B+(r0); H(r) = H(r0)g.
Proposition 1. [
Now we present the implementation of a p-stable model solver. To nd the p-stable models of a program P we can rst apply the transformations to P , however the application of the transformations is not absolutely necessary nor su cient to nd 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 nd 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.
Given a program P as input to the p-stable solver, we associate to each atom a 2 LP three sets that are used for the application of the transformations, those sets are initialized as follows, 1. H(a) = fr : r 2 P; H(r) = ag. 2. P (a) = fr : a 2 P; B+(r)g. 3. N (a) = fr : a 2 P; B (r)g.
With the information in those sets it is e cient 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 2 LP 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
ine cient and in most cases only a few rules were deleted. The LOOP
transform was implemented using the Dowling-Gallier algorithm [
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 2 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 2 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, jBj = 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 Example 1. Example of the execution of transf ormations iterated P =f 1 =f r1 : u not v: r1 : u not v: r2 : v not u: r2 : v not u: r3 : u not r; not x; b: r3 : u not r; not x; b: r4 : x y; r; not c: r4 : x y; r; not c: r5 : y not x; z; not v: r5 : y not x; z; not v: r6 : x not z; t; not d: r6 : x not z; t; not d: r7 : z t; v: r7 : z t; v: r8 : z r; not u; not x: r8 : z r; not u; not x: r9 : r not t; not a: r9 : r not t; not a: r10 : t not r; b: r10 : t not r; b: r11 : a not a; c: r11 : a c: r12 : b not d: r12 : b not d: r13 : d c; d: r14 : c not a; b; d; z: r14 : c not a; b; d; z: r15 : c not b; a; x: r15 : c not b; a; x: r16 : b not a; not u:g r16 : b not a; not u:g Lp = fg, Lf = fdg.
2 =f r1 : u not v: r2 : v not u: r3 : u not r; not x; b: r4 : x y; r; not c: r5 : y not x; z; not v: r6 : x not z; t: r7 : z t; v: r8 : z r; not u; not x: r9 : r not t; not a: r10 : t not r; b: r11 : a c: r12 : b : r15 : c not b; a; x: r16 : b not a; not u:g Lp = fbg, Lf = fg.
3 =f r1 : u not v: r2 : v not u: r3 : u not r; not x: r4 : x y; r; not c: r5 : y not x; z; not v: r6 : x not z; t: r7 : z t; v: r8 : z r; not u; not x: r9 : r not t; not a: r10 : t not r: r11 : a c:g Lp = fg, Lf = fcg.
4 =f r1 : u not v: r2 : v not u: r3 : u not r; not x: r4 : x y; r: r5 : y not x; z; not v: r6 : x not z; t: r7 : z t; v: r8 : z r; not u; not x: r9 : r not t; not a: r10 : t not r:g Lp = fg, Lf = fag.
5 =f r1 : u not v: r2 : v not u: r3 : u not r; not x: r4 : x y; r: r5 : y not x; z; not v: r6 : x not z; t: r7 : z t; v: r8 : z r; not u; not x: r9 : r not t: r10 : t not r:g Lp = fg, Lf = fg.
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 rst 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 [ fb g, 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 fbg), and the state of the atoms that were added to Lf was set to state no f act (fd; a; cg), it means that b must be in all the p-stable models of P and fd; a; cg 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. 3.2
In most cases the application of the transformations is not enough to nd 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 de nition De nition 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 ah a1; a2; :::; am; not am+1; not am+2; :::; not an:, ah is dependent of all the a0is; i = 1:::n, in a graph this dependencies can be represented with the directed edges (ai; ah); i = 1; :::; n. The graph of dependencies of a program P represents all the dependencies between the atoms in LP , given by all the rules of P .
The following de nition states the de nition of strati cation and module of a program P .
De nition 4. Let P be a normal program which can be partitioned into the disjoint sets of rules fP1; :::; Png. Let Pi; Pj 2 fP1; :::; Png; Pi 6= Pj , we say that Pi < Pj if 9r 2 Pj : 9r0 2 Pi : H(r0) 2 B(r), if from this condition we do not conclude that Pi < Pj or Pj < Pi then we can choose to hold whether Pi < Pj or Pj < Pi as long as the following properties hold. For every X; Y; Z 2 fP1; :::; Png, the strict partial order relation properties and the totality property hold: 1. X < X is false (this property holds trivially). 2. If X < Y then (Y < X is false). 3. If (X < Y and Y < Z) then X < Z. 4. P1 < ::: < Pn then we refer to this partition as the strati cation of P , sometimes we will write it as P = P0 [ ::: [ Pn. And we will refer to Pi; 1 i n as a module of P .
Fortunately we do not have to worry about how to construct this order
because there exists a well known algorithm [
Now we de ne h(Pi; P ) De nition 5. Let P be a normal program, Ci a strongly connected component of the graph of dependencies of P , and Pi the module constructed from Ci. We de ne h(Pi; P ) as the atoms which are represented as nodes in Ci. 3.3
The purpose of this section is to show how to compute the p-stable models of a program, three approaches to nd 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 de nition 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. [
2
In other words M is a p-stable model of P i M1 is a p-stable model of P1 and M2 is a p-stable model of P 0, where P20 is obtained by removing from P2 2 the occurrences of the atoms in h(P1; P ) according to the theorem 2. If P can be strati ed as P = P1 [ ::: [ Pn, n > 2, then P = P1 [ Q with Q = P2 [ ::: [ Pn is also an strati cation of P that has only two modules, and then we can apply the theorem 2.
From theorems 1 and 2, three di erent approaches to compute the p-stable
models of a program P are known. The rst approach has been implemented in
[
We illustrate the second approach by nding 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. Based on the graph of dependencies of 5 (graph 1), we see that 5 can be strati ed into two modules 5 = P1 [ P2. To compute a p-stable model of 5 we start by nding a p-stable model of P1, in this case we found frg to be a p-stable model of P1. Then compute P20 by removing the occurrences of the atoms r and t from P2 according to the theorem 2, in the next gure you can see P1, P2 and P 0 2 P2 =f P1 =f r1 : u not v: r9 : r not t: r2 : v not u: r10 : t not r:g r3 : u not r; not x: P20 = f r4 : x y; r: r1 : u not v: r5 : y not x; z; not v: r2 : v not u: r6 : x not z; t: r4 : x y: r7 : z t; v: r5 : y not x; z; not v: r8 : z r; not u; not x:g r8 : z not u; not x:g
Then nd a minimal model of P20 and do the consequence test, a minimal model of P20 is fv; xg, but when doing the consequence test we nd that RED(P20; fv; xg) [ f:fv; xgg = RED(P20; fv; xg) [ f:v _ :xg is satis able, thus fv; xg is not a p-stable model of P 0. We generate another minimal model of 2 P 0, fv; zg, this time RED(P20; fv; zg) [ f:v _ :zg is unsatis able and fv; zg is 2 accepted as a p-stable model of P 0. Merging the p-stable model of P1 and the 2 p-stable model of P20 we obtain a p-stable of 5, fr; v; zg. To look for another p-stable model of 5, we start by looking for another p-stable model of P20, we nd that fug is a p-stable model of P20, for instance another p-stable model of 5 is fr; ug. Again we try to generate another p-stable model of P20, but we note that all the p-stable models of P20 have been generated (all M 2 M M (P20) have been computed), then we go to the anterior module(P1) and try to generate another p-stable model of P1, we nd that ftg is another p-stable model of P1, then compute P20 again : P20 =f r1 : u r2 : v r3 : u r5 : y r6 : x r7 : z not v: not u: not x: not x; z; not v: not z: v:g We encounter the two p-stable models of P 0, ffx; ug; fx; vgg, from which 2 we nd another two p-stable models of 5, fft; x; ug; ft; x; vgg. When trying to generate another p-stable model of P20 we can not nd any so we go to P1, and can not nd another p-stable model of P1 so we stop. We end up with the four pstable models of 5, PS( 5) = fft; x; ug; ft; x; vg; fr; v; zg; fr; ugg. 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 ) = ffb; t; x; ug; fb; t; x; vg; fb; r; v; zg; fb; r; ugg. y: not x; z; not v: not u; not x:g
Applying again the theorem 2, rst choose a minimal model of Q1, fvg and when doing the consequence test we nd that fvg is a p-stable model of Q1. Now obtain Q02 (see the anterior gure) which is further partitioned into Q02 = R1 [ R2 [ R3 which are respectively the sets of rules with head y, x and z. Then compute a p-stable model of R1, the only p-stable model of R1 is the empty set, R20 is also empty and also has an empty p-stable model. R30 (obtained by removing from R3 the occurrences of LR1 and LR2 ) only has an empty rule z and its unique p-stable model is fzg. Merging the p-stable model of the modules P1, Q1, R1, R20 and R30 we get a p-stable model of 5, it is frg [ fvg [ fg [ fg [ fzg = fr; v; zg. When trying to generate another p-stable model, rst we try to generate another p-stable model of R30, it does not have more p-stable models, thus we go back and try on R20 but it has neither, then try on R1 that has no more p-stable models, nally we nd that Q1 has another p-stable model, fug, from this point, to nd the other p-stable models of 5, we proceed as we did when we had fvg as a p-stable model of Q1.
To show the performance of each approach we use some examples in [
problem blocks world blocks world variant
n queens spanning tree planning from initial
weight constraints planning in observations
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 [
Some preliminary tests to the p-stable solver presented in this paper, shows a bad
performance respect to a stable semantics solver(smodels[
ModuleList modules flist of modulesg create the graph of dependencies G numerate the nodes of G according to the DFS exiting time transpose the graph(compute GT ) Do a DFS(depth rst search), and in the main loop choose the nodes with bigger exiting time rst. fEach tree found by the DFS represents a strongly connected componentg for each strongly connected component c do create a new module mod for each atom a in c do
add to mod all the rules r that H(r) = a end for modules.add(mod) end for Algorithm 2 function transf ormations iterated(M odule P ))
Algorithm 4 function bool new P S(M odule P ) Algorithm 5 function bool f irst P S recursive(M odule P ) fstratify(P) returns true i P could be strati ed into more than two modules g fIf P is strati ed into P = P1 [ ::: [ Pn, as the modules Pi are in the list submodules, head(submodules(P )) = P1, rear(submodules(P )) = Pn, next(Pi) = Pi+1 1 <= i < n, back(Pi) = Pi 1 1 < i <= n, next(Pn) = back(P1) = N U LLg if stratif y(P ) then reductions iterated(P ) set Q = head(submodules(P )) fpicks the rst element of submodules(P )g if not new P S(Q) then
return false end if set Q = next(Q) while Q 6= N U LL fvisits all the modules in submodules(P )g do while not f irst P S recursive(Q) do fbacktrackingg if not next P S recursive(back(Q)) then
return false end if end while set Q = next(Q) end while else if not new P S(P ) then
return false end if end if return true Algorithm 6 function bool next P S recursive(P ) repeat fif P was not divided into more than one modulesg if jsubmodules(P )j = 0 then if new P S(P ) then
return true end if else
Q = rear(submodules(P )) if next P S recursive(Q) then
return true end if end if if back(P ) = N U LL or not next P S recursive(back(P )) then
return false end if fleaves the module as it was when createdg reset component(P ) until f irst P S recursive(P ) return true