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 [3]. The main purpose of argumentation theory is to study the fundamental mechanism, humans use in argumentation, 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.
Dung's approach, presented in [7], is a unifying framework which has played an influential 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 argumentation 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 admissible 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 argument 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 argument 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 approach is based on a solid concept in graph theory which is a strongly connected component (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. 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 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 recursive 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 argumentation 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.
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.
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 , ...,
where a and each of the b i 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 {b 1 , . . . , b n } will be denoted by B + , and the set {b n+1 , . . . , b n+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 ←.
We write L P , 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 L P . 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 L P as follows: -
-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 P i with 0 ≤ i ≤ n, such that P i is the set of rules for which the head of each clause is of order i (w.r.t. P ). We say that P 0 , . . . , P n are the relevant modules of P .
Example 2. By considering the equivalent classes of the program S in Example 1, the following relations hold: {c, e} < S {a, b} < S {d}. 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 S 0 , S 1 , S 2 :
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 T ; F 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 = T ; F be a pair of sets of atoms. The reduction R W 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 ∈ T , and we replace every atom x that occurs in the bodies of P by 0 if x ∈ 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. R W F S (P, A) = norm CS (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 [6]) and norm CS (P ) denotes the uniquely determined normal form of a program P with respect to the system CS.
We want to point out that this reduction does not coincide with the Gelfond-Lifschitz reduction [10].
Example 3. Let us consider the normal program S of Example 1. Let P be the normal program S \ S 0 , and let A be the pair of sets of atoms {c}; {e} . This means that we obtain the following programs:
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 {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.
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 {M ∩ L | M ∈ Q}. For instance, let Q be {{a, c}, {c, d}} and L be {c, d, e}, hence Q restricted to L is {{c}, {c, d}}.
Let P be a program and P 0 , . . . , P n its relevant modules. We say that a semantics S satisfies the property of relevance if for every i,
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. [7] An argumentation framework is a pair AF = AR, attacks , where AR is a finite set of arguments, and attacks is a binary relation on AR, i.e. attacks ⊆ AR × AR. We write AF AR to denote the set of all the argumentation frameworks defined over AR.
We say that a attacks b (or b is attacked by a) if (a, b) ∈ attacks holds. Usually an extension-based argumentation semantics S Arg is applied to an argumentation framework AF in order to infer sets of acceptable arguments from AF . An extension-based argumentation semantics S Arg is a function from AF AR to 2 AR . S Arg can be regarded as a pattern of selection of sets of arguments from a given argumentation framework AF .
Given an argumentation framework AF = AR, attacks , we will say that an argument a ∈ AR is acceptable, if a ∈ E such that E ∈ S Arg (AF ).
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 [11,12]).
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
-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:
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 [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 L P , 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.
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. The intended meaning of the clauses of the form d(a) ← ¬d(b i ), 1 ≤ i ≤ n, is that an argument a will be defeated when anyone of its adversaries b i is not defeated. Observe that, essentially, P 1 AF 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 P 2 AF 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 P AF = P 1 AF ∪ P 2 AF is:
a
Two relevant properties of the mapping P AF are that the stable models of P AF characterize the stable argumentation semantics and the well founded model of P AF characterizes the grounded semantics [11].
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.
Arg (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 P AF be the normal program defined in Example 4. In order to infer the stratified argumentation semantics, we infer the stratified minimal models of P AF . As we can see P AF 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 extensions 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 argumentation semantics CF2 coincide. Theorem 1. [15] Given an argumentation framework AF = AR, Attacks , and E ∈ AR, E ∈ M M r Arg (AF ) if and only if E ∈ CF 2(AF ).
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.
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 program P is split into its relevant modules P 0 , ..., P n , then compute a minimal model M of P 0 and then compute a stratified minimal model of R W F S (Q, A) where Q = P \ P 0 and A = M ; L P 0 \ M , which involves the computation of the relevant modules of R W F S (Q, A). As we will see next, it is possible to take advantage of the relevant modules already computed P 0 , ..., P n to find the relevant modules of R W 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
where i ∈ {0, ..., n}, Q = P \ (P 0 ∪ ...
If we take i = n − 1 we get
To apply the reductions it is not necessary to consider the atoms which are not in L Pn , so this equation becomes
When translating this last equation into an iterative form, we get an iterative definition for M M r c (P ) Definition 6. Let P be a normal program of order n, we define M M r c,i as follows
-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 P i ) 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 P i ) 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 P i ) constructs the graph of dependencies of RED.
The function stratif y(P i ) computes the relevant modules of P i using the algorithms three in one(P i ) and create modules(P i ). 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 compute 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 M r c (P ), we explain some notation used. We associate a sequence (a list) of relevant modules submodules(P ) to P . Let P 0 , ..., P n be the relevant modules of P . If n > 0, submodules(P ) is the sequence of relevant modules P 0 , ..., P n . If n = 0, submodules(P ) has no elements. We define the following operations over the elements of submodules(P ): next(P i ) = P i+1 if 0 ≤ i < n, back(P i ) = P i+1 if 0 ≤ i < n, and next(P n ) = back(P 0 ) = null.
To compute M M r c (P ), we use two algorithms, the algorithm f irst EM M (P ) computes one model of M M r c (P ). 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 ) be the list of relevant modules to which P belongs. When next EM M (back(P )) returns f alse, it means that P 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 ). 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 10 4 ), 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 10 4 ), 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:
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 argumentation tools able to perform reasoning by considering well-accepted argumentation semantics. One of the possible reasoning of the lack of real practical argumentation systems 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 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 [2,1].
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 (FP7-IST-215890). The views expressed in this paper are not necessarily those of the ALIVE consortium.
This definition gives the procedure we use to compute M M r c .
Given a normal program P T , the computation of M M r (P T ) can be outlined as follows:
1. Compute P = f reeT aut(P T ) ∪ {x ← x : x ∈ L P T \ H(P )}. (c) Compute the relevant modules P 0 , ..., P n of P according to the strongly connected components of G. 3. Use the procedure given by the definition 6 to compute M M r c (P ). For i = 0 to n we have to do the following (a) Compute the reduction
When i = 0, RED = P 0 . (b) Compute the relevant modules of RED. (c) Compute minimal models of RED when RED is of order 0. (d) Recursively compute M M r c (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 we base on the well known Kosaraju's algorithm [5] to find the strongly connected components of the graph of dependencies G of P . 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 C 0 , ..., C n of strongly connected components of G such that for any pair of components C i , C j such that i > j, none of the atoms in C j depends on an atom in C i . 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 P i ) computes
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.
In this appendix, we make a detailed presentation of the functions that are relevant in the implementation of the M M r solver.