Computing the Stratified Minimal Models Semantic
Mauricio Osorio1 , Angel Marin-George2 , and Juan Carlos Nieves3
1
Universidad de las Américas - Puebla
CENTIA, Sta. Catarina Mártir, Cholula, Puebla, 72820 México
osoriomauri@googlemail.com
2
Benemérita Universidad Atónoma de Puebla
Facultad de Ciencias de la Computación,
Puebla, Puebla, México
misterilei@hotmail.com
3
Universitat Politècnica de Catalunya
Software Department (LSI)
c/Jordi Girona 1-3, E08034, Barcelona, Spain
jcnieves@lsi.upc.edu
Abstract. 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 re-
cently 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 argumen-
tation semantics CF2.
Keywords: Non-monotonic reasoning, extension-based argumentation semantics
and logic programming.
1 Introduction
Argumentation theory has become an increasingly important and exciting research topic
in Artificial Intelligence (AI), with research activities ranging from developing theoret-
ical models, prototype implementations, and application studies [3]. The main purpose
of argumentation theory is to study the fundamental mechanism, humans use in argu-
mentation, and to explore ways to implement this mechanism on computers.
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 Multi-
Agent 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.
157
Dung’s approach, presented in [7], is a unifying framework which has played an in-
fluential role on argumentation research and AI. This approach is mainly orientated to
manage the interaction of arguments. The interaction of the arguments is supported by
four extension-based argumentation semantics: stable semantics, preferred semantics,
grounded semantics, and complete semantics. The central notion of these semantics
is the acceptability of the arguments. It is worth mentioning that although these ar-
gumentation semantics represents different pattern of selection of arguments, all these
argumentation semantics are based on the concept of admissible set.
An important point to remark w.r.t. the argumentation semantics based on admissi-
ble sets is that these semantics exhibit a variety of problems which have been illustrated
in the literature [17, 2, 3]. For instance, let AF be the argumentation framework which
appears in Figure 1. We can see that there are five arguments: a, b, c, c and e. The arrows
in the figure represent conflict between arguments. For example, we can see that the ar-
gument e is attacked by the argument d, the argument d is attacked by the arguments a,
b and c. Some authors, as Prakken and Vreeswijk [17], Baroni et al[2], suggest that the
argument e can be considered as an acceptable argument since it is attacked by the ar-
gument d which is attacked by three arguments: a, b, c. Observe that the arguments a, b
and c form a cyclic of attacks. However, none of the argumentation semantics suggested
by Dung is able to infer the argument e as acceptable.
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 [2] is maybe
the most general solution defined until now for improving Dung’s approach. This ap-
proach is based on a solid concept in graph theory which is a strongly connected com-
ponent (SCC). Based on this concept, Baroni et al, describe a recursive approach for
generating new argumentation semantics. For instance, the argumentation semantics
CF2 suggested in [2] is able to infer the argument e as an acceptable argument from the
argumentation framework of Figure 1.
Fig. 1. Graph representation of the following argumentation framework:
h{a, b, c, d, e}, {(a, c), (c, b), (b, a), (a, d), (c, d), (b, d), (d, e)}i.
Since Dung’s approach was introduced in [7], it was viewed as a special form of
logic programming with negation as failure. For instance, in [7] it was proved that
the grounded semantics can be characterized by the well-founded semantics [9], and
the stable argumentation semantics can be characterized by the stable model semantics
[10]. Also in [4], it was proved that the preferred semantics can be characterized by
the p-stable semantics [16]. In fact, the preferred semantics can be also characterized
by the minimal models and the stable models of a logic program [13]. By regarding an
158
argumentation framework in terms of logic programs, it has been shown that one can
construct intermediate argumentation semantics between the grounded and preferred
semantics [11]. Also it is possible to define extensions of the preferred semantics [14].
Recently, it was proved that the argumentation semantics CF2 can be characterized
by the stratified minimal model semantics (M M r ) [15]. M M r in is an interesting logic
programming semantic which satisfies some relevant properties as it is always defined
and satisfies that property of relevance. The construction of M M r is based on a recur-
sive function and minimal models. These features allow the construction of a M M r ’s
solver based on algorithms of general purpose as UNSAT algorithms.
In this paper, we introduce a solver of M M r . This solver is based on the MINISAT
solver [8] and standard graph’s algorithms. We will see that this solver presents quite
efficient running time executions that suggest that the actual version of our M M r ’s
solver is an efficient implementation.
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 §2, we present introduce some basic
concepts w.r.t. logic programming and argumentation theory. In §3, the stratified argu-
mentation semantics is introduced. In §4, 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 §5, we describe a little in detail the
implementation of the M M r ’s solver. In §6, we presents our conclusions. In Appendix
A, we present the general algorithms that where implemented in the M M r ’s solver.
2 Background
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 {a1 , ..., an }, we write ¬{a1 , ..., an } to denote the set of atoms {¬a1 , ..., ¬an }.
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 {b1 , . . . , bn }
will be denoted by B + , and the set {bn+1 , . . . , bn+m } 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 ←.
159
We write LP , to denote the set of atoms that appear in the clauses of P . We denote
by HEAD(P ) the set {a|a ← B + , ¬B− ∈ P }.
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 {a | x depends on a}. 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 = {e ← e, c ← c, a ← ¬b ∧ c, b ← ¬a ∧ ¬e, d ← b}.
The dependency relations between the atoms of LS are as follows:
dependencies-of (a) = {a, b, c, e}; dependencies-of (b) = {a, b, c, e}; dependencies-
of (c) = {c}; dependencies-of (d) = {a, b, c, e}; and dependencies-of (e) = {e}.
We can also see that, [a] = [b] = {a, b}, [d] = {d}, [c] = {c}, and [e] = {e}.
We take 0, M Mcr (P ) = M ∈M M (P0 ) {M } ∗ M Mcr (RW F S (Q, A))
where Q = P \ P0 and A = hM ; LP0 \ M i.
We call a model in M M r (P ) a stratified minimal model of P .
162
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 [11, 12] for details).
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 Stratified Argumentation Semantics
In this section, we show that by considering the stratified minimal model semantics, one
can perform argumentation reasoning based on extension-based argumentation seman-
tics 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 frame-
work 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.
1
Definition 3. Let AF = hAR, attacksi be an argumentation framework, PAF =
{d(a) ← ¬d(b1 ), . . . , d(a) ← ¬d(bn )S| a ∈ AR and {b1 , . . . , bn } = {bi ∈
2
AR | (bi , a) ∈ attacks}}; and PAF = a∈AR {a(a) ← ¬d(a)}. We define: PAF =
1 2
PAF ∪ PAF .
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.
1
Observe that, essentially, PAF is capturing the basic principle of conflict-freeness (this
means that any set of acceptable argument will not contain two arguments which attack
2
each other). The idea PAF 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
1 2
PAF = PAF ∪ PAF is:
1 2
PAF : PAF :
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).
163
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 [11].
Once we have defined a mapping from an argumentation framework into logic pro-
grams, 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
r
M of PAF such that Am = {x|a(x) ∈ M }. We write M MArg (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 nor-
mal program defined in Example 4. In order to infer the stratified argumentation se-
mantics, we infer the stratified minimal models of PAF . As we can see PAF has three
stratified minimal models : {d(a), d(b), d(d), a(c), a(e)}{d(b), d(c), d(d),
a(a), a(e)}{d(a), d(c), d(d), a(b), a(e)}, this means that AF has three stratified ex-
tensions which are: {c, e}, {a, e} and {b, e}. Observe that the stratified argumentation
semantics coincides with the argumentation semantics CF2.
In [15], it was proved that the stratified argumentation semantics and the argumen-
tation semantics CF2 coincide.
Theorem 1. [15] Given an argumentation framework AF = hAR, Attacksi, and E ∈
r
AR, E ∈ M MArg (AF ) if and only if E ∈ CF 2(AF ).
5 Implementation of the Stratified Minimal Model Semantics
In this section we describe our implementation of a M M r solver4 . The implementation
was made in C++ and despite the use of an external SAT-solver(MINISAT) to find the
minimal models, which implies the duplication of the data, we got a good performance.
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 |B(r)| = 1, for a M M r solver we also may have rules r with
|B(r)| > 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 Para-
consistent Logic [16]
164
5.1 Theoretical Justification
From the definition 2 we can design an algorithm that computes the M M r semantics.
To compute a stratified minimal model of P using the definition 2, first the input pro-
gram P is split into its relevant modules P0 , ..., Pn , then compute a minimal model M
of P0 and then compute a stratified minimal model of RW F S (Q, A) where Q = P \ P0
and A = hM ; LP0 \ M i, which involves the computation of the relevant modules of
RW F S (Q, A). As we will see next, it is possible to take advantage of the relevant mod-
ules already computed P0 , ..., Pn to find the relevant modules of RW F S (Q, A), and
thus optimizing the implementation.
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 ) ∪ {x ← x : x ∈ LP \ H(P )})
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 ) = {M } ∗ M Mcr (RW F S (Q, A))
M ∈M Mcr (P0 ∪...∪Pi )
where i ∈ {0, ..., n}, Q = P \ (P0 ∪ ... ∪ Pi ) y A = hM, LP0 ∪...∪Pi \ M i.
If we take i = n − 1 we get
[
M Mcr (P ) = {M } ∗ M Mcr (RW F S (Pn , hM, LP \Pn \ M i))
M ∈M Mcr (P \Pn )
To apply the reductions it is not necessary to consider the atoms which are not in
LPn , so this equation becomes
[
M Mcr (P ) = {M }∗M Mcr (RW F S (Pn , hM ∩LPn , (LP \Pn \M )∩LPn i))
M ∈M Mcr (P \Pn )
When translating this last equation into an iterative form, we get an iterative defini-
tion for M Mcr (P )
r
Definition 6. Let P be a normal program of order n, we define M Mc,i as follows
r
M Mc,0 = M M (P0 )
[
r
M Mc,1 = {M } ∗ M Mcr (RW F S (P1 , hM ∩ LP1 , (LP0 \ M ) ∩ LP1 i))
r
M ∈M Mc,0
[
r
M Mc,2 = {M } ∗ M Mcr (RW F S (P2 , hM ∩ LP2 , (LP0 ∪P1 \ M ) ∩ LP2 i))
r
M ∈M Mc,1
165
...
[
r
M Mc,n = {M }∗M Mcr (RW F S (Pn , hM ∩LPn , (LP0 ∪,...,∪Pn−1 \M )∩LPn i))
r
M ∈M Mc,n−1
M Mcr (P ) = M Mc,n
r
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 ) ∪ {x ← x : x ∈ LPT \ H(P )}.
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 con-
nected 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 \ 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 [5] to find the strongly connected components
of the graph of dependencies G of P 0 . A strongly connected C component of G is a
maximum set of atoms such that each pair of atoms in C is mutually dependent. This
algorithm gives a set C0 , ..., Cn of strongly connected components of G such that for
any pair of components Ci , Cj such that i > j, none of the atoms in Cj depends on an
atom in Ci . We take advantage of this sequence of strongly connected components to
compute the relevant modules of P . See the algorithm create modules(M odule P ).
The algorithm three in one(M odule Pi ) computes
RED = RW F S (Pi , hM ∩ LPi , (LP0 ∪,...,∪Pi−1 \ 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.
166
– 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 ∈ 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 algo-
rithms 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 [8], each time next minimal(P ) is called, it tries to com-
pute a minimal model of P different than the already computed, if another minimal
model of P was found, returns true, otherwise discards the SAT solver and returns
f alse.
Before explaining the main algorithms that we use to compute M Mcr (P ), we ex-
plain 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 se-
quence 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 back-
tracking 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 mini-
mal 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.
167
Table 1. Performance of the M M r solver
Na /104 size/nrules n t tnext
7 2 1 8.35 .3
15 2 339 9.5 .45
23 2 7046 8.72 .192
10 3 1 11.45 .41
16 3 26 11.50 .44
23 3 5314 10.20 .11
15 4 2 13.93 .44
20 4 650 12.81 .32
23 4 238 10.97 .001
7 5 1 15.5 .34
12 5 1 16.7 .39
17 5 3 16.02 .43
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 Conclusions
Since extension-based argumentation reasoning was introduced, it was shown that one
can perform practical argumentation reasoning by considering logic programming tools
[7]. One of the main issue in argumentation community is the definition of argumen-
tation tools able to perform reasoning by considering well-accepted argumentation se-
mantics. One of the possible reasoning of the lack of real practical argumentation sys-
tems is that the well accepted argumentation semantics as the preferred semantics and
CF2 are hard computable.
In this paper, we have introduced a solver for the stratified minimal model seman-
tics. 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 [2, 1].
As we seen in Table 1, the current version of our stratified minimal models se-
mantics’ solver is quite efficient. Hence, we argue that our actual prototype can be
168
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.
Acknowledgement
This research has been partially supported by the EC founded project ALIVE (FP7-
IST-215890). The views expressed in this paper are not necessarily those of the ALIVE
consortium.
References
1. P. Baroni and M. Giacomin. On principle-based evaluation of extension-based argumentation
semantics. Artificial Intelligence., 171(10-15):675–700, 2007.
2. P. Baroni, M. Giacomin, and G. Guida. SCC-recursiveness: a general schema for argumen-
tation semantics. Artificial Intelligence, 168:162–210, October 2005.
3. T. J. M. Bench-Capon and P. E. Dunne. Argumentation in artificial intelligence. Artificial
Intelligence, 171(10-15):619–641, 2007.
4. J. L. Carballido, J. C. Nieves, and M. Osorio. Inferring Preferred Extensions by Pstable
Semantics. Iberoamerican Journal of Artificial Intelligence (Inteligencia Artificial) ISSN:
1137-3601, 13(41):38–53, 2009 (doi: 10.4114/ia.v13i41.1029).
5. T. H. Cormen, C. E. Leiserson, R. L. Riverst, and C. Stein. Introduction to Algorithms. MIT
Press, second edition, 2001.
6. J. Dix, M. Osorio, and C. Zepeda. A General Theory of Confluent Rewriting Systems for
Logic Programming and its applications. Annals of Pure and Applied Logic, 108(1–3):153–
188, 2001.
7. P. M. Dung. On the acceptability of arguments and its fundamental role in nonmonotonic
reasoning, logic programming and n-person games. Artificial Intelligence, 77(2):321–358,
1995.
8. N. Een and N. Sorensson. An Extensible SAT-Solver. In SAT-2003, 2003.
9. A. V. Gelder, K. A. Ross, and J. S. Schlipf. The well-founded semantics for general logic
programs. Journal of the ACM, 38(3):620–650, 1991.
10. M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In
R. Kowalski and K. Bowen, editors, 5th Conference on Logic Programming, pages 1070–
1080. MIT Press, 1988.
11. J. C. Nieves. Modeling arguments and uncertain information — A non-monotonic reasoning
approach. PhD thesis, Software Department (LSI), Technical University of Catalonia, 2008.
12. J. C. Nieves and M. Osorio. A General Schema For Generating Argumentation Semantics
From Logic Programming Semantics. Research Report LSI-08-32-R, Technical University
of Catalonia, Software Department (LSI), http://www.lsi.upc.edu/dept/techreps/buscar.php,
2008.
13. J. C. Nieves, M. Osorio, and U. Cortés. Preferred Extensions as Stable Models. Theory and
Practice of Logic Programming, 8(4):527–543, July 2008.
14. J. C. Nieves, M. Osorio, U. Cortés, I. Olmos, and J. A. Gonzalez. Defining new
argumentation-based semantics by minimal models. In Seventh Mexican International Con-
ference on Computer Science (ENC 2006), pages 210–220. IEEE Computer Science Press,
September 2006.
169
15. J. C. Nieves, M. Osorio, and C. Zepeda. Expressing Extension-Based Semantics based on
Stratified Minimal Models. In H. Ono, M. Kanazawa, and R. de Queiroz, editors, Proceed-
ings of WoLLIC 2009, Tokyo, Japan, volume 5514 of FoLLI-LNAI subseries, pages 305–319.
Springer Verlag, 2009.
16. M. Osorio, J. A. Navarro, J. R. Arrazola, and V. Borja. Logics with Common Weak Com-
pletions. Journal of Logic and Computation, 16(6):867–890, 2006.
17. H. Prakken and G. A. W. Vreeswijk. Logics for defeasible argumentation. In D. Gabbay and
F. Günthner, editors, Handbook of Philosophical Logic, volume 4, pages 219–318. Kluwer
Academic Publishers, Dordrecht/Boston/London, second edition, 2002.
Appendix A: Algorithms
In this appendix, we make a detailed presentation of the functions that are relevant in
Algorithm 1 function next minimal(M odule P )
the implementation
Require: Module P of the M M r solver.
{P.S is the MINISAT solver associated to P }
if P.S = null then
Algorithm
create a1new
function nextwith
solver P.S minimal(M
the rules in odule
P P)
end if Module P
Require:
{P.S is the MINISAT
if P.S.solve() {A newsolver
minimalassociated P}
model istocomputed} then
if P.S = null
for all a ∈ Lthen
P that are in the new model generated P.S.model do
create a new solver
set state(a) P.S with the rules in P
= one
endend
if for
for all a ∈ L{A
if P.S.solve() neware
P that minimal
not in model is computed}
P.S.model do then
forset a ∈ LP that
allstate(a) are in the new model generated P.S.model do
= zero
endsetforstate(a) = one
end
add to forP.S a clause with the atoms in the minimal model generated but negated
for
return ∈ LP that are not in P.S.model do
all atrue
else set state(a) = zero
end
set P.Sfor = null
add to P.S
return a clause with the atoms in the minimal model generated but negated
f alse
endreturn
if 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
Algorithm
for all a ∈ 2Lfunction create modules(M odule P, Graph G))
P , set ord(a) = −1
Require:
{we write C[i] toP refer to the i-th strongly connected component of the sequence C, |C[i]| as
Module
array of integer
the number B[n] of C, ord(a) is the order of the atom a}
of element
Obtain
initializethethe elementsCof=BCto
sequence 0 , ...,
−1Cn of relevant modules of G using the Kosaraju’s algorithm
i =a0∈toLnP ,do
for all set ord(a) = −1
{we all aC[i]
forwrite to refer
∈ C[i], to theord(a)
initialize i-th strongly
= B[i]connected
+1 component of the sequence C, |C[i]| as
thefor
number
all a ∈ of C[i] do of C, ord(a) is the order of the atom a}
element
initialize the belements
for all that depends to −1
of B immediately on a (the edge (a, b) is in G) do
for i = 0settoB[k]
n do= B[i] + 1, k is such that b ∈ C[k]
all afor
forend ∈ C[i], initialize ord(a) = B[i] + 1
for all
end fora ∈ C[i] do
end forfor all b that depends immediately on a (the edge (a, b) is in G) do
Let m =set B[k] = B[i]: +
max{ord(a) a∈1, Lk Pis}such that
{m is ∈ C[k]
theb order of P }
Createend for of rules P0 , ..., Pm {these will be the relevant modules of P }
m sets
forend
all afor
∈ LP do
endaddforthe rules whose head is a to Pord(a)
Let m
end for= 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
170
Algorithm 3 function three in one(M odule P )
Algorithm 3 function three in one(M odule P )
Require: Module P
Require: Module P
Graph G{empty graph}
Graph G{empty graph}
bool strat af f ected = f alse {heuristic variable }
bool strat af f ected = f alse {heuristic variable }
for all A in HEAD(P ){Apply the reductions} do
for all A in HEAD(P ){Apply the reductions} do
for all r ∈ P such that head(r) = A do
for all r ∈ P such that head(r) = A do
for all a ∈ B(r) do
for all a ∈ B(r) do
if state(a) = one then
if state(a) += one then
if a ∈ B +(r) then
if a ∈ B (r) then +
remove a from B +(r))
remove a from B (r))
else
else
remove r from P )
remove r from P )
end if
end if
else
else
if state(a) = zero then
if state(a) += zero then
if a ∈ B +(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
Algorithm
return false 5 function f irst EM M (M odule P )
Algorithm
Require: Module 5 function
P f irst EM M (M odule P )
Algorithm 5 function f irst EM M (M odule P )
Require: Module
if not stratif y(P P ) then
Require:
if not Module
stratif P
y(P ) then
next minimal(P )
if not stratif y(P ) then
elsenext minimal(P )
next minimal(P )
elseset Q =the first element of submodules(P )
elseset Q =the first element of submodules(P )
next minimal(Q)
set
next Q =the first element of submodules(P )
set Q minimal(Q)
= next(Q)
next Q minimal(Q)
=
set
while Q next(Q)
6= null do
set
while Q =
Q next(Q)
6= null do
f irst EM M (Q)
while
fset Q 6=
irst EMnull do
M (Q)
Q= next(Q)
f irst
Q= EM M (Q)
next(Q)
endsetwhile
set Q = next(Q)
endendif while
end end
if while
return
end
returnif
return
Algorithm 6 function next EM M (M odule P )
Algorithm 6 function
Require: Module P next EM M (M odule P )
Algorithm 6 function next EM M (M odule P )
Require: Module P
if |subcomponent(P )| = 0 then
Require: Module P
if |subcomponent(P
if next minimal(P)|) = 0 then
then
if |subcomponent(P
if next minimal(P )|) = 0 then
then
return true
if next minimal(P ) then
endreturn
if true
return true
elseend if
end if
elseset Q =the last element of subcomponents(P )
elseset Q =the last element of subcomponents(P )
if next EM M (Q) then
if Q =the
setnext EM last thenof subcomponents(P )
element
M (Q)
return true
if next EM M (Q) then
endreturn
if true
return true
endend if if
end endif if
{backtracks iff back(P ) 6= null}
end if
{backtracks back(P
iffnull ) 6=next
null}EM M (back(P )) then
if back(P ) = or not
{backtracks back(P
iffnull ) 6=next
null}EM M (back(P )) then
return )false
if back(P = or not
if back(P
return )false
= null or not next EM M (back(P )) then
end if
return false
end if module(P )
reset
end if module(P )
freset
irst EM M (P )
irst module(P
reset )
freturn EMtrueM (P )
freturn
irst EM trueM (P )
return true
Algorithm 7 function all EM M (P rogram P M M )
Algorithm
Require: 7 function
Program P MM all EM M (P rogram P M M )
Algorithm 7 function all EM M (P rogram P M M )
Require:
Let M be a emptyPset
Program MM of models
Require: Program P MM
fromMP be
Let MMa empty
createset
itsofgraph
models
of dependencies G
Let MP beM a empty
M createset ofgraph
models
from
create modules(P its
M M, G)of dependencies G
from
createP M M create
modules(P M)M, G)of dependencies G
its graph
f irst EM M (P M M
create
f irst modules(P
(P M MM)M, G)
add to EM Mmodel
M the computed
f irst
add EM
to next (P M M
Mmodel
M the )
computed
while EM M (P M M ) do
add to M the model
M (Pcomputed
M ) do
addnext
while to M EM
the model Mcomputed
while
add next
to
end while M EM
the M (P M
model M ) do
computed
to M the model computed
171
endadd
while
return M
end while
return M
return M