It is well-known, in the area of argumentation theory, that there is a direct relationship between extension-based argumentation semantics and logic programming semantics with negation as failure. One of the main implication of this relationship is that one can explore the implementation of argumentation engines by considering logic programming solvers. Recently, it was proved that the argumentation semantics CF2 can be characterized by the stratified minimal model semantics (M M r). The stratified minimal model semantics is also a recently introduced logic programming semantics which is based on a recursive construction and minimal models. In this paper, we introduce a solver based on MINISAT algorithm for inferring the logic programming semantics M M ¤. As one of the applications of the M M r solver, we will argue that this solver is a suitable tool for computing the argumentation semantics CF2.
Argumentation theory has become an increasingly important and exciting research topic
in Artificial Intelligence (AI), with research activities ranging from developing
theoretical models, prototype implementations, and application studies [
Argumentation is also a formal discipline within Artificial Intelligence (AI) where the aim is to make a computer assist in or perform the act of argumentation. In fact, during the last years, argumentation has been gaining increasing importance in MultiAgent Systems (MAS), mainly as a vehicle for facilitating rational interaction (i.e. interaction which involves the giving and receiving of reasons). A single agent may also use argumentation techniques to perform its individual reasoning because it needs to make decisions under complex preferences policies, in a highly dynamic environment.
Dung’s approach, presented in [
An important point to remark w.r.t. the argumentation semantics based on
admissible sets is that these semantics exhibit a variety of problems which have been illustrated
in the literature [
We can recognize two major branches for improving Dung’s approach. On the one hand, we can take advantage of graph theory; on the other hand, we can take advantage of logic programming with negation as failure.
With respect to graph theory, the approach suggested by Baroni et al, in [
Since Dung’s approach was introduced in [
Recently, it was proved that the argumentation semantics CF2 can be characterized
by the stratified minimal model semantics (M M r) [
In this paper, we introduce a solver of M M r. This solver is based on the MINISAT
solver [
As we have pointed out, M M r is a logic programming semantics which is able to characterize the argumentation semantics CF2. Hence, we argue that our M M r’s solver is a quite efficient implementation of CF2. Therefore, one can consider the M M r’s solver for building rational agents whose rational process could be based on CF2 and M M r. It is worth mentioning, that to the best of our knowledge there is not an open implementation of CF2.
The rest of the paper is divided as follows: In x2, we present introduce some basic concepts w.r.t. logic programming and argumentation theory. In x3, the stratified argumentation semantics is introduced. In x4, we present how by considering the stratified minimal model semantics one can perform argumentation reasoning. In particular, we show that M M r is able to characterize CF2. In x5, we describe a little in detail the implementation of the M M r’s solver. In x6, we presents our conclusions. In Appendix A, we present the general algorithms that where implemented in the M M r’s solver. 2
In this section, we define the syntax of the logic programs that we will use in this paper and some basic concepts of logic programming semantics and argumentation semantics. 2.1
Syntax and some operations 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 fa1; :::; ang, we write :fa1; :::; ang to denote the set of atoms f:a1; :::; :ang. A normal clause, C, 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¡. We define a normal program P , as a finite set of normal clauses. If the body of a normal clause is empty, then the clause is known as a fact and can be denoted just by: a Ã.
We write LP , to denote the set of atoms that appear in the clauses of P . We denote by HEAD(P ) the set faja à B+; :B¡ 2 P g.
A program P induces a notion of dependency between atoms from LP . We say that a depends immediately on b, if and only if, b appears in the body of a clause in P , such that a appears in its head. The two place relation depends on is the transitive closure of depends immediately on. The set of dependencies of an atom x, denoted by dependencies-of (x), corresponds to the set fa j x depends on ag. We define an equivalence relation ´ between atoms of LP as follows: a ´ b if and only if a = b or (a depends on b and b depends on a). We write [a] to denote the equivalent class induced by the atom a.
Example 1. Let us consider the following normal program,
S = fe à e; c à c; a à :b ^ c; b à :a ^ :e; d à bg.
The dependency relations between the atoms of LS are as follows: dependencies-of (a) = fa; b; c; eg; dependencies-of (b) = fa; b; c; eg; dependenciesof (c) = fcg; dependencies-of (d) = fa; b; c; eg; and dependencies-of (e) = f g e .
We can also see that, [a] = [b] = fa; bg, [d] = fdg, [c] = fcg, and [e] = feg.
We take <P to denote the strict partial order induced by ´ on its equivalent classes. Hence, [a] <P [b], if and only if, b depends-on a and [a] is not equal to [b]. By considering the relation <P , each atom of LP is assigned an order as follows: – An atom a is of order 0, if [a] is minimal in <P . – An atom a is of order n + 1, if n is the maximal order of the atoms on which a depends.
We say that a program P is of order n, if n is the maximum order of its atoms. We can also break a program P of order n into the disjoint union of programs Pi with 0 · i · n, such that Pi is the set of rules for which the head of each clause is of order i (w.r.t. P ). We say that P0; : : : ; Pn are the relevant modules of P .
Example 2. By considering the equivalent classes of the program S in Example 1, the following relations hold: fc; eg <S fa; bg <S fdg. We also can see that: a is of order 1, d is of order 2, b is of order 1, e is of order 0, and c is of order 0. This means that S is a program of order 2.
The following table illustrates how the program S can be broken into the disjoint union of the following relevant modules S0, S1, S2:
S e à e. c à c. a à :b ^ c: b à :a ^ :e. d à b.
S0 e à e. c à c.
S1
S2 a à :b ^ c: b à :a ^ :e.
d à b.
Now we introduce a single reduction for any normal program. The idea of this reduction is to remove from a normal program any atom which has already fixed to some true value. In fact, this reduction is based on a pair of sets of atoms hT ; F i such that the set T contains the atoms which can be considered as true and the set F contains the atoms which can be considered as false. Formally, this reduction is defined as follows:
Let A = hT ; F i be a pair of sets of atoms. The reduction RW F S (P; A) is obtained
by 2 steps:
1. Let R(P; A) the program obtained in the following steps:
(a) We replace every atom x that occurs in the bodies of P by 1 if x 2 T , and we
replace every atom x that occurs in the bodies of P by 0 if x 2 F ;
(b) we replace every occurrence of :1 by 0 and : 0 by 1;
(c) every clause with a 0 in its body is removed;
(d) finally we remove every occurrence of 1 in the body of the clauses.
2. RW F S (P; A) = normCS (R(P; A)) such that CS is a rewriting system formed
by the transformation rules: RED+, RED¡, Success, F ailure and Loop (the
definition of these transformation rules can be founded in [
We want to point out that this reduction does not coincide with the Gelfond-Lifschitz
reduction [
Example 3. Let us consider the normal program S of Example 1. Let P be the normal program S n S0, and let A be the pair of sets of atoms hfcg; fegi. This means that we obtain the following programs:
P : R(P; A): a à :b ^ c. a à :b: b à :a ^ :e. b à :a: d à b. d à b. 2.2
Semantics restricted to LP0[¢¢¢[Pi .
From now on, we assume that the reader is familiar with the single notion of minimal model. In order to illustrate this basic notion, let P be the normal program fa à :b; b à :a; a à :c; c à :ag. As we can see, P has five models: fag, fb; cg, fa; cg, fa; bg, fa; b; cg; however, P has just two minimal models: fb; cg, fag. 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.
A semantics SEM is a mapping from the class of all programs into the powerset of the set of (2-valued) models. SEM assigns to every program P a (possible empty) set of (2-valued) models of P . If SEM (P ) = ;, then we informally say that SEM is undefined for P .
Given a set of interpretations Q and a signature L, we define Q restricted to L as fM \ L j M 2 Qg. For instance, let Q be ffa; cg; fc; dgg and L be fc; d; eg, hence Q restricted to L is ffcg; fc; dgg.
Let P be a program and P0; : : : ; Pn its relevant modules. We say that a semantics S satisfies the property of relevance if for every i, 0 · i · n, S(P0 [ ¢ ¢ ¢ [ Pi) = S(P ) 2.3
Argumentation basics
Now, we present some basic concepts with respect to extended-based argumentation
semantics. The first concept that we consider is the one of argumentation framework.
An argumentation framework captures the relationships between the arguments.
Definition 1. [
We say that a attacks b (or b is attacked by a) if (a; b) 2 attacks holds. Usually an extension-based argumentation semantics SArg is applied to an argumentation framework AF in order to infer sets of acceptable arguments from AF . An extension-based argumentation semantics SArg is a function from AF AR to 2AR. SArg can be regarded as a pattern of selection of sets of arguments from a given argumentation framework AF .
Given an argumentation framework AF = hAR; attacksi, we will say that an argument a 2 AR is acceptable, if a 2 E such that E 2 SArg(AF ). 3
Stratified Minimal Model Semantics
In this section, we introduce the stratified minimal model semantics. This semantics has
some interesting properties as: it satisfies the property of relevance, and it agrees with
the stable model semantics for the well-known class of stratified logic programs (the
proof of this property can be found in [
In order to define the stratified minimal model semantics M M r, we define the operator ¤ and the function f reeT aut as follows: – Given Q and L both sets of interpretations, we define Q ¤ L := fM1 [ M2 j M1 2
Q; M2 2 Lg. – Given a logic program P , f reeT aut denotes a function which removes from P any tautology.
The idea of the function f reeT aut is to remove any clause which is equivalent to a tautology in classical logic.
Definition 2. Given a normal logic program P , we define the sstratified minimal model semantics M M r as follows: M M r(P ) = M Mcr(f reeT aut(P ) [ fx à x j x 2 LP n HEAD(P )g such that M Mcr(P ) is defined as follows: 1. if P is of order 0, M Mcr(P ) = M M (P ). 2. if P is of order n > 0, M Mcr(P ) = SM2MM(P0)fM g ¤ M Mcr(RW F S (Q; A)) where Q = P n P0 and A = hM ; LP0 n M i.
We call a model in M M r(P ) a stratified minimal model of P .
Observe that the definition of the stratified minimal model semantics is based on a
recursive construction where the base case is the application of M M . It is not difficult
to see that if one changes M M by any other logic programming semantics S, as the
stable model semantics, one is able to construct a relevant version of the given logic
programming semantics (see [
In order to introduce an important theorem of this paper, let us introduce some concepts. We say that a normal program P is basic if every atom x that belongs to LP , then x occurs as a fact in P . We say that a logic programming semantics SEM is defined for basic programs, if for every basic normal program P then SEM (P ) is defined. 4
In this section, we show that by considering the stratified minimal model semantics, one can perform argumentation reasoning based on extension-based argumentation semantics style.
As the stratified minimal model semantics is a semantics for logic programs, we require a function mapping able to construct a logic program from an argumentation framework. Hence, let us introduce a simple mapping to regard an argumentation framework as a normal logic program. In this mapping, we use the predicates d(x), a(x). The intended meaning of d(x) is: “the argument x is defeated” (this means that the argument x is attacked by an acceptable argument), and the intended meaning of a(X) is that the argument X is accepted.
Definition 3. Let AF = hAR; attacksi be an argumentation framework, PA1F = fd(a) Ã :d(b1); : : : ; d(a) Ã :d(bn) j a 2 AR and fb1; : : : ; bng = fbi 2 AR j (bi; a) 2 attacksgg; and PA2F = Sa2ARfa(a) Ã :d(a)g. We define: PAF = PA1F [ PA2F .
The intended meaning of the clauses of the form d(a) Ã :d(bi), 1 · i · n, is that an argument a will be defeated when anyone of its adversaries bi is not defeated. Observe that, essentially, PA1F is capturing the basic principle of conflict-freeness (this means that any set of acceptable argument will not contain two arguments which attack each other). The idea PA2F is just to infer that any argument a that is not defeated is accepted.
Example 4. Let AF be the argumentation framework of Figure 1. We can see that PAF = PA1F [ PA2F is:
PA1F : PA2F : d(a) Ã :d(b). a(a) Ã :d(a): d(b) Ã :d(c). a(b) Ã :d(b): d(c) Ã :d(a). a(c) Ã :d(c): d(d) Ã :d(a). a(d) Ã :d(d): d(d) Ã :d(b). a(e) Ã :d(e): d(d) Ã :d(c). d(e) Ã :d(d).
Two relevant properties of the mapping PAF are that the stable models of PAF
characterize the stable argumentation semantics and the well founded model of PAF
characterizes the grounded semantics [
Once we have defined a mapping from an argumentation framework into logic programs, we are going to define a candidate argumentation semantics which is induced by the stratified minimal model semantics.
Definition 4. Given an argumentation framework A, we define a stratified extension of AF as follows: Am is a stratified extension of AF if exists a stratified minimal model M of PAF such that Am = fxja(x) 2 M g. We write M M Arrg(AF ) to denote the set of stratified extensions of AF . This set of stratified extensions is called stratified argumentation semantics.
In order to illustrate the stratified argumentation semantics, we are going to presents an example.
Example 5. Let AF be the argumentation framework of Figure 1 and PAF be the normal program defined in Example 4. In order to infer the stratified argumentation semantics, we infer the stratified minimal models of PAF . As we can see PAF has three stratified minimal models : fd(a); d(b); d(d); a(c); a(e)gfd(b); d(c); d(d); a(a); a(e)gfd(a); d(c); d(d); a(b); a(e)g, this means that AF has three stratified extensions which are: fc; eg, fa; eg and fb; eg. Observe that the stratified argumentation semantics coincides with the argumentation semantics CF2.
In [
Theorem 1. [
We started implementing a specific-CF2 prototype solver which was a little faster than the current version of M M r solver (when inputting CF2 programs of course).
The difference between a CF2 solver and a M M r solver is that with a CF2 solver we only have rules r with jB(r)j = 1, for a M M r solver we also may have rules r with jB(r)j > 1.
To explain our M M r solver we first give the theoretical justification and then the
implemented algorithms.
4 This implementation was made as part of a project that also includes the implementation of
a p-stable solver. The p-stablesemantics is a logic programming semantics based on
Paraconsistent Logic [
From the definition 2 given in the previous sections, and from the fact that M M r has the property of relevance, we can formulate the following definition for M M r Definition 5. Let P be a normal program, then
M M r(P ) = M Mcr(f reeT aut(P ) [ fx à x : x 2 LP n H(P )g) Where the recursive definition of M Mcr is – If P is of order 0, M Mcr(P ) = M M (P ). – If P is of order n > 0, then
M Mcr(P ) =
[ M2MMcr(P0[:::[Pi)
fM g ¤ M Mcr(RW F S (Q; A)) where i 2 f0; :::; ng, Q = P n (P0 [ ::: [ Pi) y A = hM; LP0[:::[Pi n M i. If we take i = n ¡ 1 we get
M Mcr(P ) =
[
M Mcr(P ) = [
fM g ¤ M Mcr(RW F S (Pn; hM; LP nPn n M i)) fM g¤M Mcr(RW F S (Pn; hM \LPn ; (LP nPn nM )\LPn i))
To apply the reductions it is not necessary to consider the atoms which are not in LPn , so this equation becomes
When translating this last equation into an iterative form, we get an iterative definition for M Mcr(P ) Definition 6. Let P be a normal program of order n, we define M Mcr;i as follows
M Mcr;0 = M M (P0)
M Mcr;1 = M Mcr;2 =
[
[
fM g ¤ M Mcr(RW F S (P1; hM \ LP1 ; (LP0 n M ) \ LP1 i)) fM g ¤ M Mcr(RW F S (P2; hM \ LP2 ; (LP0[P1 n M ) \ LP2 i))
. . .
M Mcr(P ) = M Mcr;n fM g¤M Mcr(RW F S (Pn; hM \LPn ; (LP0[;:::;[Pn¡1 nM )\LPn i)) M Mcr;n =
[
M2MMcr;n¡1
This definition gives the procedure we use to compute M Mcr. 5.2 Implementation Given a normal program PT , the computation of M M r(PT ) can be outlined as follows: 1. Compute P = f reeT aut(PT ) [ fx à x : x 2 LPT n H(P )g. 2. Compute the relevant modules of P .
(a) Construct the graph of dependencies G of P . (b) Find the strongly connected components of G. (c) Compute the relevant modules P0; :::; Pn of P according to the strongly connected components of G. 3. Use the procedure given by the definition 6 to compute M Mcr(P ). For i = 0 to n we have to do the following (a) Compute the reduction
RED = RW F S (Pi; hM \ LPi ; (LP0[;:::;[Pi¡1 n M ) \ LPi i)
When i = 0, RED = P0. (b) Compute the relevant modules of RED. (c) Compute minimal models of RED when RED is of order 0. (d) Recursively compute M Mcr(RED).
To remove the tautologies from P we use a simple algorithm that takes each rule
and removes those that are tautologies. To compute the relevant modules of P 0 we base
on the well known Kosaraju’s algorithm [
The algorithm three in one(M odule Pi) computes
RED = RW F S (Pi; hM \ LPi ; (LP0[;:::;[Pi¡1 n M ) \ LPi i) As we have said, in order to apply the reductions, we have to replace some atoms by 0 or 1. We associate a variable state(a) to each atom a, it indicates the value that ”replaces” a: – state(a) = one if a is to be replaced by 1. – state(a) = zero if a is to be replaced by 0. – state(a) = none if a is not to be replaced.
For optimization purpose, the algorithm three in one(M odule Pi) implements an heuristic that may save some computation in some cases. While computing RED, a rule r may be removed such that the order of the atom H(r) is the same than the order of an atom a 2 B(r). When this happens, the dependence relation between H(r) and a may be removed, it may cause the graph of dependencies of RED to have more than one strongly connected components, and it may cause the order of RED be bigger than 0. When one of those rules is removed, we can not assure that RED is of order bigger that 0, but when none of these rules is remove, we can prove that RED is of order 0. The algorithm three in one(M odule Pi) returns true if one of the rules that may affect the dependency relations was removed, and f alse if none of those rules were removed. After computing RED, the algorithm three in one(M odule Pi) constructs the graph of dependencies of RED.
The function stratif y(Pi) computes the relevant modules of Pi using the algorithms three in one(Pi) and create modules(Pi). Then returns true if and only if the resulting program is of order bigger than zero.
To compute the minimal models of a program P , we use the algorithm next minimal(P )
which is based on MINISAT [
Before explaining the main algorithms that we use to compute M Mcr(P ), we explain some notation used. We associate a sequence (a list) of relevant modules submodules(P ) to P . Let P0; :::; Pn be the relevant modules of P . If n > 0, submodules(P ) is the sequence of relevant modules P0; :::; Pn. If n = 0, submodules(P ) has no elements. We define the following operations over the elements of submodules(P ): next(Pi) = Pi+1 if 0 · i < n, back(Pi) = Pi+1 if 0 · i < n, and next(Pn) = back(P0) = null.
To compute M Mcr(P 0), we use two algorithms, the algorithm f irst EM M (P ) computes one model of M Mcr(P 0). After calling f irst EM M (P ) we use the backtracking algorithm next EM M (P ) to compute more stratified minimal models. Let submodules(P 0) be the list of relevant modules to which P belongs. When next EM M (back(P )) returns f alse, it means that P 0 has no more stratified minimal models, in this case next EM M (P ) also return f alse. If next EM M (back(P )) returns f alse, the algorithm reset module(P ) (not presented in this paper) is used to reset P and leave it as it was when initialized by creates modules(P 0). After the backtracking we start again by calling to f irst EM M (P ).
Finally the algorithm all EM M (P M M ) shows how to put f irst EM M (:::) and next EM M (:::) together to compute M M r(P M M ).
In table 1, it is shown the time it took to the solver to find the stratified minimal models of some randomly generated programs of 500000 rules, the first column shows the number of atoms(divided by 104), in the second, the average cardinality of B+(r) [ B¡(r), then the initial number or modules, the time to find the first model, and the time between the subsequent models. The performance tests were executed in a Linux PC, with Pentium IV processor, 2.8Ghz and 512Mb RAM.
In table 1, it is shown the time it took to the solver to find the stratified minimal models of some randomly generated programs of 500000 rules, the first column shows the number of atoms(divided by 104), in the second, the average cardinality of B+(r) [ B¡(r), then the initial number or modules, the time to find the first model, and the time between the subsequent models.
The interested reader can download our actual version of the M M r solver from: http://www.lsi.upc.edu/»jcnieves/software/MMr.tar Also, one can find in http://www.lsi.upc.edu/»jcnieves/software//MMr-examples.tar some illustrative examples. 6
Since extension-based argumentation reasoning was introduced, it was shown that one
can perform practical argumentation reasoning by considering logic programming tools
[
In this paper, we have introduced a solver for the stratified minimal model
semantics. We have shown that the stratified minimal model semantics is practical enough
for performing argumentation reasoning based on extension-based argumentation style.
An interesting property of the stratified minimal model semantics is it can characterize
a argumentation semantics called CF2. CF2 is an promising argumentation semantics
able to overcome some of unexpected behaviors of argumentation semantics based on
admissible sets [
As we seen in Table 1, the current version of our stratified minimal models semantics’ solver is quite efficient. Hence, we argue that our actual prototype can be considered as a candidate tool for building argumentation systems which could perform reasoning based on M M r and of course CF2. It is worth mentioning, that to the best of our knowledge there is not an open implementation of CF2.
This research has been partially supported by the EC founded project ALIVE (FP7IST-215890). The views expressed in this paper are not necessarily those of the ALIVE consortium.
In this appendix, we make a detailed presentation of the functions that are relevant in
Algorithm 1 function next minimal(M odule P ) the iRmeqpuilree:mMoednuletaPtion of the M M r solver.
{P.S is the MINISAT solver associated to P } if P.S = null then Algocrrietahtmea1nefwunscotlivoenr Pn.eSxtwimthitnhiemrualels( Min oPdule P ) Reeqnudirief: Module P i{fPP.S.Si.s othlveeM()IN{AISnAeTwsmolivneirmaaslsomcoiadteldistocoPm}puted} then if Pfo.Sr a=ll nau∈llLthPenthat are in the new model generated P.S.model do
cresaetetsatanetew(aso)l=veroPne.S with the rules in P endenifd for if Pfo.Sr.aslollave∈()L{PAtnheawtamreiniomt ainl mP.oSd.emliosdceolmdpouted} then forseatllsata∈teL(aP) t=hazteareoin the new model generated P.S.model do endseftosrtate(a) = one eadnd tforP.S a clause with the atoms in the minimal model generated but negated froertuarlnlatr∈uLeP that are not in P.S.model do else set state(a) = zero seentdPf.oSr = null raedtdutronPf.Salaseclause with the atoms in the minimal model generated but negated endreitfurn true else set P.S = null return f alse end if Algorithm 2 function create modules(M odule P, Graph G)) Require: Module P array of integer B[n]
Obtain the sequence C = C0, ..., Cn of relevant modules of G using the Kosaraju’s algorithm Alfgoorrailtlham∈2LfPu,nscettioonrdc(rae)a=te−m1 odules(M odule P, Graph G)) Re{qwueirwe:riMte oCd[uil]etoPrefer to the i-th strongly connected component of the sequence C, |C[i]| as tahrreanyuomf binetreogferelBe m[ne]nt of C, ord(a) is the order of the atom a} iOnbitiailniztehethseeeqlueemnecnetCso=fBCt0o, .−..1,Cn of relevant modules of G using the Kosaraju’s algorithm for aill=a0∈toLnP ,dsoet ord(a) = −1 {wfeorwarlilteaC∈[iC]t[oi],reinfeitriatoliztheeoir-dth(as)tro=ngBly[ic]o+nn1ected component of the sequence C, |C[i]| as thefonrumalblear ∈of Cel[eim]denot of C, ord(a) is the order of the atom a} initialfiozre athllebeltehmatednetspeonfdBs itmom−e1diately on a (the edge (a, b) is in G) do for i = 0setoBn[kd]o= B[i] + 1, k is such that b ∈ C[k] foreanldlafo∈r C[i], initialize ord(a) = B[i] + 1 feonrdaflolra ∈ C[i] do end foforr all b that depends immediately on a (the edge (a, b) is in G) do Let m =semtBax[k{]or=d(Ba[)i]: +a ∈1, LkPis}s{umch itshathtebo∈rdCer[ko]f P } Createnmd sfoerts of rules P0, ..., Pm {these will be the relevant modules of P } foreanldl afo∈r LP do endadfdorthe rules whose head is a to Pord(a) eLnedt mfor= max{ord(a) : a ∈ LP } {m is the order of P } Create m sets of rules P0, ..., Pm {these will be the relevant modules of P } for all a ∈ LP do
add the rules whose head is a to Pord(a) end for else else remove r from P ) remove r from P ) end if end if else else if state(a) = zero then if state(aB)+= zero then if a ∈ (r) then if a ∈ B+(r) then remove r from P ) remove r from P ) else else − remove a from B −(r)) remove a from B (r)) end if end if end if end if end if end if end for end for if r was removed in the loop above then if r was removed in the loop above then if there is an atom b ∈ B(r) with the same order than H(r) then if there is an atom b ∈ B(r) with the same order than H(r) then set strat af f ected = true set strat af f ected = true end if end if end if end if end for end for end for end for W F S(P ){Apply the transformations of the CS system} W F S(P ){Apply the transformations of the CS system} if it was removed a rule by the function W F S(P ) then if it was removed a rule by the function W F S(P ) then set strat af f ected = true set strat af f ected = true end if end if create in G a graph of dependencies from the rules remaining in P . create in G a graph of dependencies from the rules remaining in P . return strat af f ected return strat af f ected Algorithm 4 function stratif y(M oduleP ) Algorithm 4 function stratif y(M oduleP ) Require: Module P Require: Module P if three in one(P ) then if three in one(P ) then create modules(P, G){G is the graph of dependencies created in three in one} create modules(P, G){G is the graph of dependencies created in three in one} if |subcomponents(P )| > 1 then if |subcomponents(P )| > 1 then return true return true end if end if set P = the first element of submodules(P ) set P = the first element of submodules(P ) subcomponents(P ).clear() subcomponents(P ).clear() end if end if return false Alrgeotruirtnhmfal5sefunction f irst EM M (M odule P ) Algorithm 5 function f irst EM M (M odule P ) RAelgqouririeth:mMo5dfuulencPtion f irst EM M (M odule P ) Reiqf uniortes:trMaotidfuyle(PP) then Require: Module P if nnoetxsttrmatiinfim
y(Pal)(Pth)en if not stratif y(P ) then elsenext minimal(P )
next minimal(P ) elseset Q =the first element of submodules(P ) else sneetxQt m=tihneimfirastl(eQle)ment of submodules(P ) set Q =the first element of submodules(P ) sneetxQt m=inneixmta(Ql()Q) next minimal(Q) swehtiQle =Q n6=exntu(lQl)do set Q = next(Q) whfilierQst 6=E MnuMll (dQo ) while Q 6= null do sfeitrQst =E MneMxt((QQ)) f irst EM M (Q) endsewtQhil=e next(Q)
set Q = next(Q) endenifd while
end while erentdurifn end if return return Algorithm 6 function next EM M (M odule P ) Algorithm 6 function next EM M (M odule P ) RAelgqouririeth:mMo6dfuulencPtion next EM M (M odule P ) Reiqf u|isrue:bcMomodpuolneePnt(P )| = 0 then Require: Module P if i|fsunbecxotmmpoinniemnta(lP(P)|) =th0enthen if |subcomponent(P )| = 0 then if nreextutrmnitnruiemal(P ) then if next minimal(P ) then endreitfurn true
return true elseend if
end if elseset Q =the last element of subcomponents(P ) else isfetnQex=ttEheMlaMst (eQle)mtehnetnof subcomponents(P ) set Q =the last element of subcomponents(P ) if nreextutrEn MtruMe (Q) then if next EM M (Q) then endreitfurn true
return true endenifd if
end if e{nbdacikftracks iff back(P ) 6= null} end if i{fbbaacckktr(aPck)s=iffnbualclko(rPn)o6=tnneuxltl}EM M (back(P )) then {backtracks iff back(P ) 6= null} if braectku(rPn )fa=lsenull or not next EM M (back(P )) then if back(P ) = null or not next EM M (back(P )) then endreitfurn false
return false ernesdeitf module(P ) end if rfeirsestt mEModMule((PP)) reset module(P ) rfeitrusrtnEtMrueM (P ) f irst EM M (P ) return true return true Algorithm 7 function all EM M (P rogram P M M ) Algorithm 7 function all EM M (P rogram P M M ) RAelgqouririeth:mPro7gfruamncPtioMn Mall EM M (P rogram P M M )
Praogerma mptyPsMet Mof models ReLqeutirMe: be Require: Program P M M fLreotmMPbe Maemcrpetayteseittsogfrmapohdeolfsdependencies G
M Let M be a empty set of models fcrroematPe MmoMduclreesa(tPeiMts Mgra,pGh)of dependencies G from P M M create its graph of dependencies G cfrierastteEmModMu(lePsM(PMM)M, G) create modules(P M M, G) afdidrstto EMMthMe m(PodMelMco)mputed f irst EM M (P M M ) awdhdilteonMexttheEmodMel(cPoMmpMute)ddo
M awdhdaildteodnMtoexMttheEthmMeomdMeold(cPeolMmcopMmutpe)uddteod while next EM M (P M M ) do endadwdhtioleM the model computed
add to M the model computed erentdurn
whiMle end while return M return M