1: \documentclass{tlp}
2:
3: \usepackage{graphics}
4: \usepackage{times}
5: \usepackage{amssymb}
6: \usepackage[matrix,arrow]{xy}
7: \CompileMatrices
8:
9: \newtheorem{theorem}{Theorem}
10: \newtheorem{proposition}[theorem]{Proposition}
11: \newtheorem{lemma}[theorem]{Lemma}
12: \newtheorem{corollary}[theorem]{Corollary}
13: \newtheorem{definition}{Definition}
14: \newtheorem{example}{Example}
15: \newtheorem{remark}{Remark}
16:
17:
18: \newcommand{\herbrand}{\mathcal{H}}
19: \newcommand{\assm}{{\it assm}}
20: \newcommand{\conc}{{\it conc}}
21: \newcommand{\mycenter}[1]{\hspace*{\fill}#1\hspace*{\fill}}
22:
23: % Notation for variables of notions of attack: math style
24: % Notation for fixed notions of attack: sans serif
25: % Warning: if used in math mode, does not produce spaces,
26: % e.g. \na{strongly attacks} comes out as stronglyattacks.
27: % Can't use \textsf{} either, because that changes
28: % the fontsize to normal in subscripts etc.
29: \newcommand{\na}[1]{{\sf #1}}
30:
31: \author[Ralf Schweimeier and Michael Schroeder]
32: {Ralf Schweimeier and Michael Schroeder\\\\
33: Department of Computing, School of Informatics, City University\\
34: Northampton Square, London EC1V 0HB, UK\\\\
35: Department of Computer Science, Technische Universit\"at Dresden\\
36: 01062 Dresden, Germany\\\\
37: \email{\{ralf,msch\}@soi.city.ac.uk}}
38: \title{A Parameterised Hierarchy of Argumentation Semantics for Extended Logic Programming and its Application to the Well-founded Semantics}
39:
40: \shorttitle{A Hierarchy of Argumentation Semantics}
41:
42: \bibliographystyle{acmtrans}
43: \jdate{Nov 2002}
44: \pubyear{2001}
45: \pagerange{\pageref{firstpage}--\pageref{lastpage}}
46: \doi{S1471068401001193}
47:
48:
49: \submitted{4 December 2002}
50: \revised{29 June 2003}
51: \accepted{12 September 2003}
52:
53:
54: \begin{document}
55:
56:
57:
58: \maketitle
59:
60: \begin{abstract}
61: Argumentation has proved a useful tool in defining formal semantics
62: for assumption-based reasoning by viewing a proof as a process in
63: which proponents and opponents attack each others arguments by
64: undercuts (attack to an argument's premise) and rebuts (attack to an
65: argument's conclusion). In this paper, we formulate a variety of
66: notions of attack for extended logic programs from combinations of
67: undercuts and rebuts and define a general hierarchy of argumentation
68: semantics parameterised by the notions of attack chosen by proponent
69: and opponent. We prove the equivalence and subset relationships
70: between the semantics and examine some essential properties
71: concerning consistency and the coherence principle, which relates
72: default negation and explicit negation. Most significantly, we
73: place existing semantics put forward in the literature in our
74: hierarchy and identify a particular argumentation semantics for
75: which we prove equivalence to the paraconsistent well-founded
76: semantics with explicit negation, WFSX$_p$.
77: Finally, we present a general proof theory,
78: based on dialogue trees, and show that it is sound and complete with
79: respect to the argumentation semantics.
80: \end{abstract}
81:
82: \noindent {\bf Keywords:}
83: Non-monotonic Reasoning, Extended Logic Programming, Argumentation
84: semantics, Well-founded Semantics with Explicit Negation
85:
86:
87: \newpage
88: \tableofcontents
89: \newpage
90:
91:
92: \section{Introduction}
93:
94:
95:
96: Argumentation has attracted much interest in the area of Artificial
97: Intelligence. On the one hand, argumentation is an important way of
98: human interaction and reasoning, and is therefore of interest for
99: research into intelligent agents. Application areas include automated
100: negotiation via
101: argumentation~\cite{PSJ98:AgentsArguing,KSE98:Argument,Sch99:Argument}
102: and legal reasoning~\cite{PS97:Argument}. On the other hand,
103: argumentation provides a formal model for various assumption based (or
104: non-monotonic, or default) reasoning
105: formalisms~\cite{BDKT97:Argument,CML00:LogicalModelsOfArgument}. In
106: particular, various argumentation based semantics have been proposed
107: for logic programming with default
108: negation~\cite{BDKT97:Argument,Dun95:Argument}.
109:
110: Argumentation semantics are elegant since they can be captured in an
111: abstract
112: framework~\cite{Dun95:Argument,BDKT97:Argument,%
113: Vre97:AbstractArgumentationSystems,JV99:RobustSemantics},
114: for which an elegant theory of attack, defence, acceptability, and
115: other notions can be developed, without recourse to the concrete
116: instance of the reasoning formalism at hand. This framework can then
117: be instantiated to various assumption based reasoning formalisms.
118: Similarly, a dialectical proof theory, based on dialogue trees,
119: can be defined for an abstract
120: argumentation framework, and then applied to any instance of such a
121: framework~\cite{SCG94:Dialectics,Dun95:Argument,JV99:DialecticSemantics}.
122:
123: In general, an argument $A$ is a proof which may use a set of
124: defeasible assumptions. Another argument $B$ may have a conclusion
125: which contradicts the assumptions or the conclusions of $A$, and
126: thereby $B$ {\em attacks} $A$. There are two fundamental notions of such
127: attacks: undercut and rebut~\cite{Pol87:Defeasible,PS97:Argument} or equivalently {\em
128: ground-attack} and {\em reductio-ad-absurdum attack}
129: \cite{Dun93:ArgumentExplicit}. We will use the terminology of
130: undercuts and rebuts. Both attacks differ in that an undercut attacks a
131: premise of an argument, while a rebut attacks a
132: conclusion.
133:
134: Given a logic program we can define an argumentation semantics by
135: iteratively collecting those arguments which are acceptable to a
136: proponent, i.e. they can be defended against all opponent attacks. In
137: fact, such a notion of acceptability can be defined in a number of
138: ways depending on which attacks we allow the proponent and opponent to use.
139:
140: Normal logic programs do not have negative conclusions, which means
141: that we cannot use rebuts. Thus both opponents can only launch
142: undercuts on each other's assumptions.
143: Various argumentation semantics have been defined for normal logic programs
144: \cite{BDKT97:Argument,Dun95:Argument,KT99:ComputingArgumentation},
145: some of which are equivalent to
146: existing semantics such as the stable model semantics~\cite{GL88:StableModels}
147: or the well-founded semantics~\cite{GRS91:WFS}.
148:
149: Extended logic programs
150: \cite{GL90:ClassicalNegation,AP96:WFSX,wag94a}, on the other hand,
151: introduce explicit negation, which states that a literal is explicitly
152: false. As a result, both undercuts and rebuts are possible forms of attack;
153: there are further variations depending on whether any kind of counter-attack
154: is admitted. A variety of argumentation semantics arise if one allows
155: one notion of attack as defence for the proponent, and another as attack
156: for the opponent.
157: Various argumentation semantics have been proposed for extended logic programs
158: \cite{Dun93:ArgumentExplicit,PS97:Argument,MA98:Argumentation,}.
159: Dung has shown that a certain argumentation semantics is equivalent to
160: the answer set semantics~\cite{GL90:ClassicalNegation}, a generalisation
161: of the stable model semantics~\cite{GL88:StableModels}.
162: For the well-founded semantics with explicit negation,
163: WFSX~\cite{PA92:WFSX,AP96:WFSX}, there exists a \emph{scenario semantics}
164: \cite{ADP93:ScenarioSemantics} which is similar to an argumentation semantics.
165: This semantics applies only to non-contradictory programs;
166: to our knowledge, no argumentation semantics has yet been found equivalent
167: to the \emph{paraconsistent} well-founded semantics with explicit negation,
168: WFSX$_p$~\cite{Dam96:Thesis,ADP95:LPsystem,AP96:WFSX}.
169:
170: This paper makes the following contributions: we identify various
171: notions of attack for extended logic programs. We set up a general
172: framework of argumentation semantics, parameterised on these notions
173: of attacks. This framework is then used to classify notions of
174: justified arguments, and to compare them to the argumentation
175: semantics of %Dung~
176: \cite{Dun93:ArgumentExplicit} and
177: %Prakken and Sartor~
178: \cite{PS97:Argument}, among others. We examine some properties
179: of the different semantics, concerning consistency, and the coherence
180: principle which relates explicit and implicit negation. One
181: particular argumentation semantics is then shown to be equivalent to
182: the paraconsistent well-founded semantics with explicit
183: negation~\cite{Dam96:Thesis}. Finally, we
184: develop a general dialectical proof theory for the notions of
185: justified arguments we introduce, and show how proof procedures for
186: these proof theories can be derived. This paper builds upon an earlier
187: conference publication \cite{sch02a}, which reports initial findings,
188: while this article provides detailed coverage including all proofs and
189: detailed examples.
190:
191:
192: The paper is organised as follows: First we define arguments and
193: notions of attack and acceptability. Then we set up a framework for
194: classifying different least fixpoint argumentation semantics, based on
195: different notions of attack. Section~\ref{sec:properties} examines
196: some properties (coherence and consistency) of these semantics. In
197: Section~\ref{sec:wfsxarg}, we recall the definition of WFSX$_p$, and prove
198: the equivalence of an argumentation semantics and WFSX$_p$. A general
199: dialectical proof theory for arguments is presented in
200: Section~\ref{sec:proof-theory}; we prove its soundness and
201: completeness and outline how a proof procedure for the proof theory
202: may be derived.
203:
204: \section{Extended Logic Programming and Argumentation}
205: \label{sec:elp}
206:
207: We introduce extended logic programming and summarise the definitions
208: of arguments associated with extended logic programs.
209: We identify various notions of attack between arguments,
210: and define a variety of semantics parametrised on these notions of attack.
211:
212:
213: Extended logic programming extends logic programming by two kinds of
214: negation: \emph{default negation} and \emph{explicit negation}.
215: The former allows the assumption of the falsity of a fact if there is
216: no evidence for this fact. Explicit negation, on the other hand,
217: allows to explicitly assert the falsity of a fact.
218:
219: The default negation of a literal $p$, written $not~p$, states the
220: assumption of the falsity of $p$. The assumption $not~p$ is intended
221: to be true iff there is no evidence of $p$. Thus, the truth of $not~p$
222: relies on a lack of knowledge about $p$.
223: An operational interpretation of default negation is given by
224: \emph{negation as failure} \cite{cla78}:
225: the query $not~p$ succeeds iff the query $p$ fails.
226: Default negation is usually not allowed in the head of a rule: the
227: truth value of $not~p$ is defined in terms of $p$, and so there should
228: not be any other rules that define $not~p$.
229:
230:
231:
232:
233: Default negation thus gives a way of expressing a kind of negation,
234: based on a lack of knowledge about a fact.
235: Sometimes, however, it is desirable to express the explicit knowledge
236: of the falsity of a fact.
237: The explicit negation $\neg p$ of a literal $p$ states that $p$ is
238: known to be false. In contrast to default negation, an explicit
239: negation $\neg p$ is allowed in the head of a rule, and there is no
240: other way of deriving $\neg p$ except by finding an applicable rule
241: with $\neg p$ as its consequence.
242:
243:
244: Consider the following example
245: \footnote{Due to John McCarthy, first published in \cite{GL90:ClassicalNegation}}:
246: ``A school bus may cross the railway tracks under the condition
247: that there is no approaching train.''
248: It may be expressed using default negation as
249: $$cross \gets not~train$$
250: This is a dangerous statement, however: assume that there is no knowledge about
251: an approaching train, e.g. because the driver's view is blocked. In
252: this case, the default negation $not~train$ is true, and we conclude
253: that the bus may cross.
254: Instead, it would be appropriate to demand the explicit knowledge that
255: there is no approaching train, as expressed using explicit negation:
256: $$cross \gets \neg train$$
257: The combination of default and explicit negation also allows for a
258: more cautious statement of positive facts: while the rule
259: $$\neg cross \gets train$$
260: states that the driver should not cross if there is a train approaching,
261: the rule
262: $$\neg cross \gets not~\neg train$$
263: states more cautiously that the driver should not cross if it has not
264: been established that there is no train approaching.
265: In contrast to the former rule, the latter rule prevents a driver from
266: crossing if there is no knowledge about approaching trains.
267:
268: A connection between the two kind of negations may be made by
269: asserting the \emph{coherence principle}
270: \cite{PA92:WFSX,AP96:WFSX}: it states that whenever an
271: explicit negation $\neg p$ is true, then the default negation $not~p$
272: is also true. This corresponds to the statement that
273: if something is known to be false, then it should also be assumed to
274: be false.
275:
276:
277:
278:
279: \subsection{Arguments}
280: \label{subsec:arguments}
281:
282:
283: \begin{definition}
284: An {\em objective literal} is an atom $A$ or its explicit negation
285: $\neg A$. We define $\neg \neg L = L$.
286: A {\em default literal} is of the form $not~L$ where $L$
287: is an objective literal. A {\em literal} is either an objective or a
288: default literal.
289: \\
290: An {\em extended logic program} is a (possibly infinite) set of rules of
291: the form
292:
293: $L_0 \gets L_1,\dots,L_m, not~L_{m+1},\dots, not~L_{m+n}
294: (m, n \ge 0)$,
295: \\
296: where each $L_i$ is an objective literal ($0\leq i \leq m+n$).
297: For such a rule $r$, we call $L_0$ the {\em head} of the rule,
298: $head(r)$, and $L_1,\ldots,not~L_{m+n}$ the {\em body} of the rule,
299: $body(r)$.
300: A rule with an empty body is called a {\em fact}, and we write
301: $L_0$ instead of $L_0 \gets$.
302: \end{definition}
303:
304: Our definition of an argument associated with an extended logic
305: program is based on~\cite{PS97:Argument}.
306: Essentially, an argument is a partial proof, resting on a number of
307: {\em assumptions}, i.e.~a set of default literals.%
308: \footnote{In~\cite{BDKT97:Argument,Dun93:ArgumentExplicit}, an argument
309: {\em is} a set of assumptions; the two approaches are equivalent in
310: that there is an argument with a conclusion $L$ iff there is a set
311: of assumptions from which $L$ can be inferred. See the discussion
312: in~\cite{PS97:Argument}.}
313: Note that we do not consider priorities of rules, as used e.g.\
314: in~\cite{ant02,kak02,PS97:Argument,Bre96:DynamicPreferences,GSC98:Argument,%
315: Vre97:AbstractArgumentationSystems}.
316: Also, we do not distinguish between \emph{strict} rules, which may not
317: be attacked, and \emph{defeasible} rules, which may be attacked
318: \cite{PS97:Argument,SL92:MTDR,GSC98:Argument}.
319:
320: \begin{definition}
321: \label{def:argument}
322: %Argument \hspace{.5cm}
323: Let $P$ be an extended logic program.
324: An {\em argument} associated with $P$ is a finite sequence
325: $A=[r_1,\dots r_n]$ of ground instances of
326: rules $r_i \in P$ such that
327: %
328: %\begin{enumerate}
329: %\item
330: %1.
331: for every $1\le i \le n$, for every objective literal $L_j$ in
332: the body of $r_i$ there is a $k>i$ such that $head(r_k) = L_j$.
333: %
334: %\item
335: % 2. No two distinct rules in the sequence have the same head.
336: %\end{enumerate}
337: %
338: \\
339: A {\em subargument} of $A$ is a subsequence of $A$ which is an argument.
340: The head of a rule in $A$ is called a {\em conclusion} of $A$,
341: and a default literal $not~L$ in the body of a rule of $A$ is called an
342: {\em assumption} of $A$.
343: We write $\assm(A)$ for the set of assumptions and $\conc(A)$ for the
344: set of conclusions of an argument $A$.
345:
346: An argument $A$ with a conclusion $L$ is a {\em minimal argument for $L$}
347: if there is no subargument of $A$ with conclusion $L$.
348: An argument is {\em minimal} if it is minimal for some literal $L$.
349: Given an extended logic program $P$, we denote the set of minimal arguments
350: associated with $P$ by $\mathit{Args}_P$.
351:
352: \end{definition}
353:
354: The restriction to minimal arguments (cf.~\cite{SL92:MTDR})
355: is not essential, but convenient,
356: since it rules out arguments constructed from several unrelated
357: arguments. Generally, one is interested in the conclusions of an
358: argument, and wants to avoid having rules in an argument which do not
359: contribute to the desired conclusion.
360: Furthermore, when designing a proof procedure to compute justified
361: arguments, one generally wants to compute only minimal arguments,
362: for reasons of efficiency.
363:
364: \begin{example}
365: \label{ex:train}
366: Consider the following program:
367: $$\begin{array}{rcl}
368: \neg cross & \gets & not~\neg train \\
369: cross & \gets & \neg train \\
370: train & \gets & see\_train \\
371: \neg train & \gets & not~train, wear\_glasses \\
372: wear\_glasses\\
373: \end{array}$$
374: The program models the example from the introduction to this section.
375: A bus is allowed to cross the railway tracks if it is known that there
376: is no train approaching; otherwise, it is not allowed to cross.
377: A train is approaching if the driver can see the train,
378: and it is known that there is no train approaching if there is no
379: evidence of a train approaching, and the driver is wearing glasses.
380:
381: There is exactly one minimal argument with conclusion $cross$:
382: $$[cross \gets \neg train; \neg train \gets not~train, wear\_glasses;
383: wear\_glasses]$$
384: It contains as subarguments the only minimal arguments for
385: $\neg train$ and $wear\_glasses$:
386: $$[\neg train \gets not~train, wear\_glasses]$$
387: $$[wear\_glasses]$$
388: There is also exactly one minimal argument with conclusion $\neg cross$:
389: $$[\neg cross \gets not~\neg train]$$
390: There is no argument with conclusion $train$, because there is no rule
391: for $see\_train$.
392: \end{example}
393:
394: \subsection{Notions of attack}
395: \label{subsec:attack}
396:
397: There are two fundamental notions of attack: {\em undercut},
398: which invalidates an assumption of an argument, and
399: {\em rebut}, which contradicts a conclusion of an
400: argument~\cite{Dun93:ArgumentExplicit,PS97:Argument}.
401: From these, we may define further
402: notions of attack, by allowing either of the two fundamental kinds of
403: attack, and considering whether any kind of counter-attack is allowed
404: or not. We will now formally define these notions of attack.
405:
406: \begin{definition}
407: \label{def:notionsofattack}
408: Let $A_1$ and $A_2$ be arguments.
409: \begin{enumerate}
410:
411: \item
412: $A_1$ {\em undercuts} $A_2$ if there is an objective literal
413: $L$ such that $L$ is a conclusion of $A_1$ and $not~L$ is an
414: assumption of $A_2$.
415:
416: \item
417: $A_1$ {\em rebuts} $A_2$ if there is an objective literal $L$
418: such that $L$ is a conclusion of $A_1$ and $\neg L$ is a
419: conclusion of $A_2$.
420:
421: \item
422: $A_1$ {\em attacks} $A_2$ if $A_1$ undercuts or rebuts $A_2$.
423:
424: \item
425: $A_1$ {\em defeats} $A_2$ if
426: \begin{itemize}
427: \item $A_1$ undercuts $A_2$, or
428: \item $A_1$ rebuts $A_2$ and $A_2$ does not undercut $A_1$.
429: \end{itemize}
430:
431: \item
432: $A_1$ {\em strongly attacks} $A_2$ if $A_1$ attacks $A_2$ and
433: $A_2$ does not undercut $A_1$.
434:
435: \item
436: $A_1$ {\em strongly undercuts} $A_2$ if $A_1$ undercuts $A_2$
437: and $A_2$ does not undercut~$A_1$.
438: \end{enumerate}
439: \end{definition}
440:
441: The notions of \emph{undercut} and \emph{rebut}, and hence \emph{attack} are
442: fundamental for extended logic
443: programs~\cite{Dun93:ArgumentExplicit,PS97:Argument}. The notion of
444: \emph{defeat} is used in~\cite{PS97:Argument}, along with a notion of
445: \emph{strict defeat}, i.e.\ a defeat that is not counter-defeated.
446: For arguments without priorities, rebuts are symmetrical, and
447: therefore strict defeat coincides with strict
448: undercut, i.e.\ an undercut that is not counter-undercut.
449: For this reason, we use the term {\em strong undercut} instead of
450: {\em strict undercut}, and similarly define {\em strong attack} to be
451: an attack which is not counter-undercut.
452: %
453: We will use the following abbreviations for these notions of attack.
454: \na{r} for rebuts,
455: \na{u} for undercuts,
456: \na{a} for attacks,
457: \na{d} for defeats,
458: \na{sa} for strongly attacks, and
459: \na{su} for strongly undercuts.
460:
461: \begin{example}
462: Consider the program of example~\ref{ex:train}. There are the
463: following minimal arguments:
464: $$\begin{array}{ll}
465: A: & [cross \gets \neg train;
466: \neg train \gets not~train, wear\_glasses;
467: wear\_glasses] \\
468: B: & [\neg cross \gets not~\neg train] \\
469: C: & [\neg train \gets not~train, wear\_glasses] \\
470: D: & [wear\_glasses] \\
471: \end{array}$$
472: The argument $A$ and $B$ rebut each other.
473: The subargument $C$ of $A$ also undercuts $B$, so $A$ also undercuts
474: $B$. Therefore $A$ strongly attacks $B$, while $B$ does not strongly attack
475: or defeat $A$.
476: \end{example}
477:
478: \begin{example}
479: The arguments
480: $[q\gets not~p]$
481: and
482: $[p\gets not~q]$
483: undercut each other. As a result, they do not strongly undercut each other.
484:
485: The arguments $[p\gets not~q]$ and $[\neg p\gets not~r]$ do not
486: undercut each other, but strongly attack each other.
487:
488: The argument $[\neg p\gets not~r]$ strongly undercuts $[p\gets not~
489: \neg p]$ and $[p\gets not~ \neg p]$ attacks - but does not defeat -
490: the argument $[\neg p\gets not~r]$.
491: \end{example}
492:
493: These notions of attack define for any extended logic program a binary
494: relation on the set of arguments associated with that program.
495:
496: \begin{definition}
497: A {\em notion of attack} is a function $x$ which assigns to each
498: extended logic program $P$ a binary relation $x_P$ on the set of
499: arguments associated with $P$,
500: i.e.\ $x_P \subseteq \mathit{Args}_P\times \mathit{Args}_P$.
501: Notions of attack are partially ordered by defining
502: $x \subseteq y \mbox{ ~iff~ } \forall P: x_P \subseteq y_P$
503: \end{definition}
504:
505: \begin{description}
506: \item[Notation] We will use sans-serif font for the specific notions of
507: attack introduced in Definition~\ref{def:notionsofattack} and
508: their abbreviations: $\na{r}$, $\na{u}$, $\na{a}$, $\na{d}$,
509: $\na{sa}$, and $\na{su}$. We will use $x, y, z, \ldots$ to denote
510: variables for notions of attacks.
511: Arguments are denoted by $A, B, C, \ldots$
512:
513: The term ``attack'' is somewhat overloaded: 1. it is the notion of
514: attack \na{a} consisting of a rebut or an undercut; we use this
515: terminology because it is standard in the
516: literature~\cite{Dun93:ArgumentExplicit,PS97:Argument}. 2. in
517: general, an attack is a binary relation on the set of arguments of a
518: program; we use the term ``notion of attack''. 3. if the
519: argumentation process is viewed as a dialogue between an proponent
520: who puts forward an argument, and an opponent who tries to dismiss
521: it, we may choose one notion of attack for the use of the proponent,
522: and another notion of attack for the opponent. In such a setting,
523: we call the former notion of attack the ``defence'', and refer to
524: the latter as ``attack'', in the hope that the meaning of the term
525: ``attack'' will be clear from the context.
526: \end{description}
527:
528:
529: \begin{definition}
530: Let $x$ be a notion of attack. Then
531: the {\em inverse} of $x$, denoted by $x^{-1}$, is defined as
532: $x^{-1}_P = \{ (B,A) ~|~ (A,B) \in x_P \}$.
533: \end{definition}
534:
535: In this relational notation,
536: Definition~\ref{def:notionsofattack} can be rewritten as
537: $\na{a} = \na{u} \cup \na{r}$, $\na{d} = \na{u} \cup (\na{r} - \na{u}^{-1})$,
538: $\na{sa} = (\na{u} \cup \na{r}) - \na{u}^{-1}$,
539: and $\na{su} = \na{u} - \na{u}^{-1}$.
540:
541:
542: \begin{proposition}
543: The notions of attack of
544: Definition~\ref{def:notionsofattack} are partially ordered according
545: to the diagram in Figure~\ref{fig:notions-of-attack}.
546: \end{proposition}
547:
548: \begin{proof}
549: A simple exercise, using the set-theoretic laws $A-B \subseteq A
550: \subseteq A \cup C$ and $(A \cup B) - C = (A - C) \cup (B - C)$
551: (for any arbitrary sets $A$, $B$, and $C$).
552: \end{proof}
553:
554: \begin{figure}
555: \hspace{-2em}
556: $$\xymatrixnocompile@C=-2em@R=4ex{
557: & \parbox{3.5cm}{\begin{center}\na{attacks} $= \na{a} = \na{u} \cup \na{r}$\end{center}\vspace{-1ex}} \ar@{-}[d] \\
558: & \parbox{5cm}{\vspace{-1.5ex}\begin{center}\na{defeats} $= \na{d} = \na{u} \cup (\na{r} - \na{u}^{-1})$\end{center}\vspace{-1ex}}
559: \ar@{-}[dl] \ar@{-}[dr] \\
560: \parbox{3.5cm}{\vspace{-1.5ex}\begin{center}\na{undercuts} $= \na{u}$\end{center}\vspace{-1ex}} \ar@{-}[dr] &&
561: \hspace{-2cm}\parbox{6cm}{\vspace{-1.5ex}\begin{center}\na{strongly attacks} $= \na{sa} = (\na{u} \cup \na{r}) - \na{u}^{-1}$\end{center}\vspace{-1ex}}
562: \ar@{-}[dl] \\
563: & \parbox{5.5cm}{\hspace{-2cm}\vspace{-1.5ex}\begin{center}\na{strongly undercuts} $= \na{su} = \na{u} - \na{u}^{-1}$\end{center}} \\
564: }$$
565: \caption{Notions of Attack}
566: \label{fig:notions-of-attack}
567: \end{figure}
568:
569: As mentioned above, we will work with notions of attack as examined in
570: previous literature. Therefore Figure~\ref{fig:notions-of-attack}
571: contains the notions of
572: \na{undercut} \cite{Dun93:ArgumentExplicit,PS97:Argument},
573: \na{attack} \cite{Dun93:ArgumentExplicit,PS97:Argument},
574: \na{defeat} \cite{PS97:Argument},
575: \na{strong undercut} \cite{PS97:Argument},
576: and \na{strong attack} as an intermediate
577: notion between \na{strongly undercuts} and \na{defeats}.
578: All of these notions of attack are extensions of \na{undercuts}.
579: The reason is
580: that undercuts are asymmetric, i.e. for two arguments $A$, $B$, $A
581: \na{u} B$ does not necessarily imply $B \na{u} A$.
582: Rebuts, on the other hand, are symmetric, i.e. $A \na{r} B$ implies
583: $B \na{r} A$. As a consequence, rebuts on their own always lead to a
584: ``draw'' between arguments. There is, however, a lot of work on
585: priorities between arguments
586: \cite{ant02,kak02,PS97:Argument,Bre96:DynamicPreferences,%
587: GSC98:Argument,Vre97:AbstractArgumentationSystems}, which implies that
588: rebuts become asymmetric and therefore lead to more interesting
589: semantics. But the original, more basic approach does not consider
590: this extension, and hence undercuts play the prime role and notions of
591: attack mainly based on rebuts, such as $\na{r}$ or $\na{r-u^{-1}}$,
592: are not considered.
593:
594:
595: The following example shows that the inclusions in
596: Figure~\ref{fig:notions-of-attack} are strict.
597:
598: \begin{example}
599: Consider the following program:
600:
601: \begin{center}
602: $\begin{array}{rcl}
603: p & \gets & not~\neg p \\
604: p & \gets & not~q \\
605: \neg p & \gets & not~r \\
606: q & \gets & not~p \\
607: \neg~q & \gets & not~s \\
608: \end{array}$
609: \end{center}
610:
611: \noindent
612: It has the minimal arguments
613: $\{ [p \gets not~\neg p], [p \gets not~q], [\neg p \gets not~r],
614: [q \gets not~p], [\neg~q \gets not~s] \}$.
615: The arguments $[p \gets not~q]$ and $[q \gets not~p]$ undercut
616: (and hence defeat) each other, but they do not strongly undercut
617: or strongly attack each other.
618: The arguments $[q \gets not~r]$ and $[\neg q \gets not~s]$
619: strongly attack (and hence defeat) each other, but they do not
620: undercut each other.
621: The argument $[p \gets not~\neg p]$ attacks $[\neg p \gets not~r]$,
622: but it does not defeat it, because $[\neg p \gets not~r]$
623: (strongly) undercuts $[p \gets not~\neg p]$.
624: \end{example}
625:
626:
627:
628: \subsection{Acceptability and justified arguments}
629: \label{subsec:acceptable}
630:
631: Given the above notions of attack, we define acceptability of an
632: argument. Basically, an argument is acceptable if it can be defended
633: against any attack. Our definition of acceptability is parametrised
634: on the notions of attack allowed for the proponent and the opponent.
635:
636: Acceptability forms the basis for our argumentation semantics,
637: which is defined as the least fixpoint of a function, which collects
638: all acceptable arguments
639: \cite{Pol87:Defeasible,SL92:MTDR,PS97:Argument,Dun93:ArgumentExplicit}.
640: The {\em least} fixpoint is of particular interest, because it
641: provides a canonical fixpoint semantics and it can be constructed
642: inductively.
643:
644: Because the semantics is based on parametrised acceptability, we
645: obtain a uniform framework for defining a variety of argumentation
646: semantics for extended logic programs. It can be instantiated to a
647: particular semantics by choosing one notion of attack for the
648: opponent, and another notion of attack as a defence for the proponent.
649: The uniformity of the definition makes it a convenient framework for
650: comparing different argumentation semantics.
651:
652: %\subsection*{Definitions of Acceptability}
653: %\label{sec:defacc}
654:
655: \begin{definition}
656: Let $x$ and $y$ be notions of attack. Let $A$ be an argument, and
657: $S$ a set of arguments. Then $A$ is {\em $x/y$-acceptable wrt.\ $S$}
658: if for every argument $B$ such that $(B,A) \in x$ there exists an
659: argument $C \in S$ such that $(C,B) \in y$.
660: \end{definition}
661:
662: Based on the notion of acceptability, we can then define a fixpoint
663: semantics for arguments.
664:
665: \begin{definition}
666: \label{def:just}
667: Let $x$ and $y$ be notions of attack, and $P$ an extended logic
668: program. The operator
669: $F_{P, x/y}:\mathcal{P}(\mathit{Args}_P) \rightarrow \mathcal{P}(\mathit{Args}_P)$
670: is defined as
671: $$F_{P, x/y}(S) = \{ A ~|~ A \mbox{ is $x/y$-acceptable wrt.\ $S$} \}$$
672: We denote the least fixpoint of $F_{P, x/y}$ by $J_{P, x/y}$.
673: If the program $P$ is clear from the context, we omit the subscript $P$.
674: An argument $A$ is called {\em $x/y$-justified} if $A \in J_{x/y}$;
675: an argument is called {\em $x/y$-overruled} if it is attacked by an
676: $x/y$-justified argument; and an argument is called {\em $x/y$-defensible}
677: if it is neither $x/y$-justified nor $x/y$-overruled.
678: \end{definition}
679:
680: Note that this definition implies that the logic associated with
681: justified arguments is 3-valued, with justified arguments corresponding
682: to {\em true} literals, overruled arguments to {\em false} literals,
683: and defensible arguments to {\em undefined} literals.
684: We could also consider arguments which are both justified and overruled;
685: these correspond to literals with the truth value {\em overdetermined}
686: of Belnap's four-valued logic~\cite{Bel77:FourValued}.
687:
688: \begin{proposition}
689: For any program $P$, the operator $F_{P,x/y}$ is monotone.
690: By the Knaster-Tarski fixpoint
691: theorem~\cite{Tar55:Fixpoint,Bir67:LatticeTheory}, $F_{P,x/y}$ has a
692: least fixpoint. It can be constructed by transfinite induction as follows:
693: %
694: \begin{quote}
695: $\begin{array}{llll}
696: J^0_{x/y} & \!\!\!:=\!\!\! & \emptyset \\
697: J^{\alpha+1}_{x/y} & \!\!\!:=\!\!\! & F_{P, x/y}(J^\alpha_{x/y}) &
698: \mbox{for $\alpha \! + \! 1$ a successor ordinal} \\
699: J^\lambda_{x/y} & \!\!\!:=\!\!\! & \bigcup_{\alpha <
700: \lambda}J^\alpha_{x/y} &
701: \mbox{for $\lambda$ a limit ordinal} \\
702: \end{array}$
703: \end{quote}
704: %
705: Then there exists a least ordinal $\lambda_0$ such that
706: $F_{x/y}(J^{\lambda_0}_{x/y}) = J^{\lambda_0}_{x/y} =: J_{x/y}$.
707: \end{proposition}
708:
709: \begin{proof}
710: Let $S_1 \subseteq S_2$, and $A \in F_{P,x/y}$,
711: i.e.~$A$ is $x/y$-acceptable wrt.~$S_1$, i.e.~every $x$-attack against
712: $A$ is $y$-attacked by an argument in $S_1$. Then $A$ is also
713: $x/y$-acceptable wrt.~$S_2$, because $S_1 \subseteq S_2$, i.e.~$S_2$
714: contains more arguments to defend $A$.
715: \end{proof}
716:
717: Note that our general framework encompasses some well-known argumentation
718: semantics for extended logic programs:
719: Dung's grounded semantics~\cite{Dun93:ArgumentExplicit} is $J_{\na{a}/\na{u}}$.
720: Prakken and Sartor's argumentation semantics~\cite{PS97:Argument},
721: without priorities or strict rules is $J_{\na{d}/\na{su}}$.
722: If we regard explicitly negated literals $\neg L$ as new atoms, unrelated
723: to the positive literal $L$, then we can apply the well-founded
724: argumentation semantics of~\cite{BDKT97:Argument,KT99:ComputingArgumentation}
725: to extended logic programs, and obtain $J_{\na{u}/\na{u}}$.
726:
727:
728:
729: \begin{table}[t]
730: \begin{center}
731: $\begin{array}{l||c|c|c|c|c|c|c}
732: & \na{a}/x & \na{d}/x &
733: \parbox{3em}{$\na{u}/\na{u} =$ $\na{u}/\na{su}$} &
734: \parbox{4em}{$\na{u}/\na{a} =$ $\na{u}/\na{d} =$ $\na{u}/\na{sa}$} &
735: \parbox{4em}{$\na{sa}/\na{sa} =$ $\na{sa}/\na{su}$} &
736: \parbox{4em}{$\na{sa}/\na{a} =$ $\na{sa}/\na{d} =$ $\na{sa}/\na{u}$} & \na{su}/x \\ \hline\hline
737: 1 & \emptyset & [s] & [s] & [s] &
738: \parbox[c]{5em}{$[p~\gets~not~q]$, $[s]$} &
739: \parbox[c]{5em}{$[p~\gets~not~q]$, $[s]$} &
740: \parbox[c]{5em}{$[p~\gets~not~q]$, $[q~\gets~not~p]$, $[s]$}
741: \\ \hline
742: 2 & \emptyset & \emptyset & [\neg q \gets not~r] &
743: [\neg q \gets not~r] & \emptyset & [\neg q \gets not~r] &
744: [\neg q \gets not~r] \\ \hline
745: 3 & \emptyset & \emptyset & \emptyset & [p \gets not~q] &
746: \emptyset & \emptyset & \emptyset \\ \hline
747: 4 & \emptyset & \emptyset & \emptyset & \emptyset & \emptyset &
748: \emptyset & \emptyset
749: \end{array}$
750: \caption{Computing justified arguments --
751: the $n$-th row shows the justified arguments
752: added at the $n$-th iteration}
753: \label{tab:justified}
754: \end{center}
755: \end{table}
756:
757:
758: \begin{example}
759: Consider the following program $P$:
760:
761: \begin{center}
762: $\begin{array}{rcl}
763: p & \gets & not~q \\
764: q & \gets & not~p \\
765: \neg q & \gets & not~r \\
766: r & \gets & not~s \\
767: s \\
768: \neg s & \gets & not~s \\
769: \end{array}$
770: \end{center}
771:
772:
773: Table~\ref{tab:justified} shows the computation of justified
774: arguments associated with $P$.
775: The columns show various combinations $x/y$ of attack/defence,
776: and a row $n$ shows those arguments $A$ that get added at iteration
777: stage $n$, i.e. $A \in J^n_{P, x/y}$ and
778: $A \not\in J^{n-1}_{P, x/y}$.
779:
780: The set of arguments associated with $P$ is
781: $\{ [p \gets not~q], [q \gets not~p], [\neg q \gets not~r],
782: [r \gets not~s], [s], [\neg s \gets not~s] \}$.
783:
784: All arguments are undercut by another argument, except $[s]$;
785: the only attack against $[s]$ is a rebut by $[\neg s \gets not~s]$,
786: which is not a defeat. Thus, $[s]$ is identified as a justified argument
787: at stage $0$ in all semantics, except if \na{attacks}
788: is allowed as an attack.
789: In the latter case, no argument is justified at stage $0$, hence the
790: set of justified arguments $J_{\na{a}/x}$ is empty.
791:
792:
793:
794: \end{example}
795:
796:
797: \section{Relationships between Notions of Justifiability}
798: \label{sec:relationship}
799:
800: The definition of justified arguments provides a variety of
801: semantics for extended logic programs, depending on which
802: notion of attack $x$ is admitted to attack an argument,
803: and which notion of attack $y$ may be used as a defence.
804:
805: This section is devoted to an analysis of the relationship
806: between the different notions of justifiability, leading to
807: a hierarchy of notions of justifiability illustrated in
808: Figure~\ref{fig:hierarchy}.
809:
810:
811: \subsection{Equivalence of argumentation semantics}
812: \label{sec:eq}
813:
814: We will prove a series of theorems, which show that some of
815: the argumentation semantics defined above are subsumed by others,
816: and that some of them are actually equivalent.
817: Thus, we establish a hierarchy of argumentation semantics, which
818: is illustrated in Figure~\ref{fig:hierarchy}.
819:
820: First of all, it is easy to see that the least fixpoint increases if
821: we weaken the attacks or strengthen the defence.
822:
823: \begin{theorem}
824: \label{thm:subset-just}
825: Let $x' \subseteq x$ and $y \subseteq y'$ be notions of attack, then
826: $J_{x/y} \subseteq J_{x'/y'}$.
827: \end{theorem}
828:
829: \begin{proof}
830: See \ref{appendix}.
831: \end{proof}
832:
833: Theorem~\ref{thm:strong-nonstrong} states that it does not make a
834: difference if we allow only the strong version of the defence. This is
835: because an argument need not defend itself on its own, but it may rely
836: on other arguments to defend it.
837:
838:
839: \begin{theorem}
840: \label{thm:strong-nonstrong}
841: Let $x$ and and $y$ be notions of attack such that
842: $x \supseteq \na{undercuts}$, and let
843: $sy = y - \na{undercuts}^{-1}$.
844: Then $J_{x/y} = J_{x/sy}$.
845: \end{theorem}
846:
847: \begin{proof}
848: Informally, every $x$-attack $B$ to an $x/y$-justified argument $A$ is
849: $y$-defended by some $x/sy$-justified argument $C$ (by induction).
850: Now if $C$ is {\em not} a $sy$-attack, then it is undercut by $B$,
851: and because $x \supseteq \na{undercuts}$ and
852: $C$ is justified, there exists a {\em strong} defence
853: for $C$ against $B$, which is also a defence of the original
854: argument $A$ against $C$.\\[2ex]
855: %
856: The formal proof is by transfinite induction.
857: By Theorem~\ref{thm:subset-just}, we have $J_{x/sy} \subseteq J_{x/y}$.
858: We prove the inverse inclusion by showing that
859: for all ordinals $\alpha$:
860: $J_{x/y}^\alpha \subseteq J_{x/sy}^\alpha$,
861: by transfinite induction on $\alpha$.
862: See \ref{appendix} for the detailed proof.
863: \end{proof}
864:
865: In particular, the previous Theorem states that undercut and strong
866: undercut are equivalent as a defence, as are attack and strong attack.
867: This may be useful in an implementation, where we may use the stronger
868: notion of defence without changing the semantics, thereby decreasing
869: the number of arguments to be checked.
870: The following Corollary shows that because defeat lies between attack
871: and strong attack, it is equivalent to both as a defence.
872:
873: \begin{corollary}
874: \label{cor:xa-xsa-just}
875: Let $x$ be a notion of attack such that $x \supseteq \na{undercuts}$. Then
876: $J_{x/\na{a}} = J_{x/\na{d}} = J_{x/\na{sa}}$.
877: \end{corollary}
878:
879: \begin{proof}
880: It follows from
881: Theorems~\ref{thm:subset-just} and~\ref{thm:strong-nonstrong} that
882: $J_{x/\na{sa}} \subseteq J_{x/\na{d}} \subseteq J_{x/\na{a}} = J_{x/\na{sa}}$.
883: \end{proof}
884:
885:
886:
887: The following theorem states that defence with \na{undercuts} is
888: equally strong as one with \na{defeats} or with \na{attacks},
889: provided the opponent's permitted attacks include at least the
890: \na{strong attacks}.
891:
892: \begin{theorem}
893: \label{thm:xu-xa-just}
894: Let $x$ be a notion of attack such that
895: $x \supseteq$ \na{strongly attacks}. Then
896: $J_{x/\na{u}} = J_{x/\na{d}} = J_{x/\na{a}}$.
897: \end{theorem}
898:
899:
900:
901: \begin{proof}
902: It is sufficient to show that $J_{x/\na{a}} \subseteq J_{x/\na{u}}$.
903: Then by Theorem~\ref{thm:subset-just},
904: $J_{x/\na{u}} \subseteq J_{x/\na{d}} \subseteq J_{x/\na{a}} = J_{x/\na{u}}$.\\[1ex]
905: %
906: Informally, every $x$-attack $B$ to a $x/\na{a}$-justified argument $A$
907: is attacked by some
908: $x/\na{u}$-justified argument $C$ (by induction).
909: If $C$ is a rebut, but not an
910: undercut, then because $B$ strongly attacks $C$, and because
911: $x \supseteq$ \na{strongly attacks},
912: there must have been an argument defending $C$ by
913: undercutting $B$, thereby also defending $A$ against $B$.\\[1ex]
914: %
915: We prove by transfinite induction that for all ordinals $\alpha$:
916: $J^\alpha_{x/\na{a}} \subseteq J^\alpha_{x/\na{u}}$.
917: See \ref{appendix} for the detailed proof.
918: \end{proof}
919:
920: In analogy to Theorem~\ref{thm:xu-xa-just}, strong undercuts are an
921: equivalent defence to strong attacks if the allowed attacks are
922: strong attacks.
923:
924: \begin{theorem}
925: \label{thm:sasu-sasa-just}
926: $J_{\na{sa}/\na{su}} = J_{\na{sa}/\na{sa}}$
927: \end{theorem}
928:
929:
930: \begin{proof}
931: The proof is similar to the proof of Theorem~\ref{thm:xu-xa-just}.
932: See \ref{appendix}.
933: \end{proof}
934:
935:
936:
937:
938:
939: \begin{theorem}
940: \label{thm:sua-sud-just}
941: $J_{\na{su}/\na{a}} = J_{\na{su}/\na{d}}$
942: \end{theorem}
943:
944:
945: \begin{proof}
946: %
947: By Theorem~\ref{thm:subset-just},
948: $J_{\na{su}/\na{d}} \subseteq J_{\na{su}/\na{a}}$.\\[1ex]
949: %
950: We now show the inverse inclusion. Informally, every strong
951: undercut $B$ to a $\na{su}/\na{a}$-justified argument $A$ is attacked by some
952: $\na{su}/\na{d}$-justified argument $C$ (by induction). If $C$ does not
953: defeat $A$, then there is some argument $D$ defending $C$ by
954: defeating $B$, thereby also defending $A$ against $B$.\\[1ex]
955: %
956: Formally, we show that
957: for all ordinals $\alpha$:
958: $J_{\na{su}/\na{a}}^\alpha \subseteq J_{\na{su}/\na{d}}^\alpha$,
959: by transfinite induction on $\alpha$.
960: See \ref{appendix} for the detailed proof.
961: \end{proof}
962:
963: These results are summarised in a hierarchy of argumentation semantics
964: in Theorem~\ref{thm:hierarchy} and Figure~\ref{fig:hierarchy}.
965:
966: \subsection{Distinguishing argumentation semantics}
967: \label{sec:ex}
968:
969: The previous section showed equality and subset relationships for a
970: host of notions of justified arguments. In this section we complement
971: these positive findings by negative findings stating for which
972: semantics there are no subset relationships. We prove these negative
973: statements by giving counter-examples distinguishing various notions of
974: justifiability.
975:
976:
977:
978: The first example shows that, in general, allowing only strong forms
979: of attack for the opponent leads to a more credulous semantics,
980: because in cases where only non-strong attacks exist, every argument
981: is justified.
982:
983: \begin{example}\hspace{0cm}
984: \label{ex:loop}
985: Consider the following program:
986: \begin{center}
987: $\begin{array}{rcl}
988: p & \gets & not~q \\
989: q & \gets & not~p \\
990: \end{array}$
991: \end{center}
992: For any notion of attack $x$, we have
993: $J_{\na{su}/x} = J_{\na{sa}/x} = \{ [p \gets not~q], [q \gets not~p] \},$
994: because there is no strong undercut or strong attack to any
995: of the arguments.
996: %
997: However,
998: $J_{\na{a}/x} = J_{\na{d}/x} = J_{\na{u}/x} = \emptyset,$
999: because every argument is undercut (and therefore defeated and
1000: attacked).
1001:
1002: Thus, in general, $J_{s/x} \not\subseteq J_{w/y}$, for
1003: $s \in \{\na{su}, \na{sa}\}$, $w \in \{\na{a}, \na{u}, \na{d}\}$, and any notions of
1004: attack $x$ and $y$.
1005: \end{example}
1006:
1007: The following example shows that some interesting properties need not
1008: hold for all argumentation semantics: a fact (i.e. a rule with an
1009: empty body) need not necessarily lead to a justified argument;
1010: this property distinguishes Dung's~\cite{Dun93:ArgumentExplicit} and
1011: Prakken and Sartor's~\cite{PS97:Argument} semantics from most of the
1012: others.
1013:
1014:
1015: \begin{example}\hspace{0em}
1016: \label{ex:coherence}
1017: Consider the following program:
1018: \begin{center}
1019: %
1020: $\begin{array}{rcl}
1021: p & \gets & not~q \\
1022: q & \gets & not~p \\
1023: \neg p \\
1024: \end{array}$
1025: %
1026: \end{center}
1027: %
1028: Let $x$ be a notion of attack. Then
1029: $J_{\na{d}/x} = J_{\na{a}/x} = \emptyset,$
1030: because every argument is defeated (hence attacked).
1031: $J_{\na{sa}/\na{su}} = J_{\na{sa}/\na{sa}} = \{ [q \gets not~p] \},$
1032: because $[q \gets not~p]$ is the only argument which is not
1033: strongly attacked, but it does not strongly attack any other
1034: argument.
1035: $J_{\na{u}/\na{su}} = J_{\na{u}/\na{u}} = \{ [\neg p] \},$
1036: because there is no undercut to $[\neg p]$, but
1037: $[\neg p]$ does not undercut any other argument.
1038: $J_{\na{u}/\na{a}} = \{ [\neg p], [q \gets not~p] \},$
1039: because there is no undercut to $[\neg p]$, and the undercut
1040: $[p \gets not~p]$ to $[q \gets not~p]$ is attacked by
1041: $[\neg p]$. We also have
1042: $J_{\na{sa}/\na{u}} = \{ [\neg p], [q \gets not~p] \},$
1043: because $[q \gets not~p]$ is not strongly attacked, and the strong
1044: attack $[p \gets not~q]$ on $[\neg p]$ is undercut by
1045: $[q \gets not~p]$.
1046:
1047:
1048: Thus, in general, $J_{\na{u}/x} \not\subseteq J_{\na{d}/x}$,
1049: $J_{\na{u}/x} \not\subseteq J_{\na{a}/x}$,
1050: $J_{\na{sa}/sx} \not\subseteq J_{\na{u}/y}$ (where $sx \in \{ \na{su}, \na{sa} \}$ and
1051: $y \in \{ \na{u}, \na{su} \}$), and
1052: $J_{\na{u}/y} \not\subseteq J_{\na{sa}/sx}$ (where $sx \in \{ \na{su}, \na{sa} \}$ and
1053: $y \in \{ \na{u}, \na{a}, \na{d}, \na{su}, \na{sa}\}$).
1054: \end{example}
1055:
1056: The following example is similar to the previous example,
1057: except that all the undercuts are strong, whereas in the previous
1058: example there were only non-strong undercuts.
1059:
1060: \begin{example}\hspace{0cm}
1061: \label{ex:coherence-big}
1062: Consider the following program:
1063: \begin{center}
1064: %
1065: $\begin{array}{rcl}
1066: p & \gets & not~q \\
1067: q & \gets & not~r \\
1068: r & \gets & not~s \\
1069: s & \gets & not~p \\
1070: \neg p \\
1071: \end{array}$
1072: %
1073: \end{center}
1074: %
1075: Let $x$ be a notion of attack.
1076: Then $J_{\na{sa}/x} = \emptyset,$
1077: because every argument is strongly attacked.
1078:
1079: $J_{\na{su}/\na{u}} = J_{\na{su}/\na{su}} = \{ [\neg p] \},$ because
1080: all arguments except $[\neg p]$ are strongly undercut, but $[\neg
1081: p]$ does not undercut any argument. And $J_{\na{u}/\na{a}} =
1082: J_{\na{su}/\na{sa}} = J_{\na{su}/\na{a}} = \{ [\neg p], [q \gets
1083: not~r], [s \gets not~p] \}$, because $[\neg p]$ is not undercut, and it
1084: defends $[s \gets not~p]$ against the strong undercut $[p \gets not~q]$ (by
1085: rebut), and in turn, $[s \gets not~p]$ defends $[q \gets not~r]$ against the
1086: strong undercut $[r \gets not~s]$ (by strong undercut).
1087:
1088: Thus, $J_{\na{u}/\na{a}} \not\subseteq J_{\na{su}/y}$,
1089: $J_{\na{su}/\na{sa}} \not\subseteq J_{\na{su}/y}$, and
1090: $J_{\na{su}/\na{a}} \not\subseteq J_{\na{su}/y}$, for $y \in \{
1091: \na{u}, \na{su} \}$.
1092: \end{example}
1093:
1094: The following example shows that in certain circumstances,
1095: non-strong defence allows for more justified arguments than
1096: strong defence.
1097:
1098: \begin{example}\hspace{0cm}
1099: \label{ex:loop-plus}
1100: Consider the following program:
1101: \begin{center}
1102: %
1103: $\begin{array}{rcl}
1104: p & \gets & not~q \\
1105: q & \gets & not~p \\
1106: r & \gets & not~p \\
1107: \end{array}$
1108: %
1109: \end{center}
1110: %
1111: Let $x$ be a notion of attack. Then
1112: $J_{\na{u}/x} = J_{\na{d}/x} = J_{\na{a}/x} = \emptyset,$
1113: because every argument is undercut.
1114: $J_{\na{su}/\na{su}} = J_{\na{su}/\na{sa}} = J_{\na{sa}/\na{su}} = J_{\na{sa}/\na{sa}} =
1115: \{ [p \gets not~q], [q \gets not~p] \}$ :
1116: In these cases, the strong attacks are precisely the strong undercuts;
1117: the argument $[r \gets not~p]$ is not justified, because the
1118: strong undercut $[p \gets not~q]$ is undercut, but not strongly
1119: undercut, by $[q \gets not~p]$. And finally,
1120: $J_{\na{su}/\na{u}} = J_{\na{su}/\na{a}} = J_{\na{sa}/\na{u}} = J_{\na{sa}/\na{a}} =
1121: \{ [p \gets not~q], [q \gets not~p], [r \gets not~p] \}$ :
1122: Again, undercuts and attacks, and strong undercuts and strong
1123: attacks, coincide; but now $[r \gets not~p]$ is justified,
1124: because non-strong undercuts are allowed as defence.
1125:
1126: Thus, in general, $J_{x/\na{u}} \not\subseteq J_{x/\na{su}}$ and
1127: $J_{x/\na{a}} \not\subseteq J_{x/\na{sa}}$, where $x \in \{ \na{su}, \na{sa} \}$.
1128: \end{example}
1129:
1130: The following example distinguishes the argumentation semantics
1131: of Dung~\cite{Dun93:ArgumentExplicit} and
1132: Prakken and Sartor~\cite{PS97:Argument}.
1133:
1134: \begin{example}\hspace{0cm}
1135: \label{ex:defeat}
1136: Consider the following program:
1137: \begin{center}
1138: %
1139: $\begin{array}{rcl}
1140: p & \gets & not~\neg p \\
1141: \neg p \\
1142: \end{array}$
1143: %
1144: \end{center}
1145: %
1146: Then $J_{\na{a}/x} = \emptyset$, because both arguments attack each
1147: other, while $J_{\na{d}/x} = \{[\neg p]\}$, because $[\neg p]$ defeats
1148: $[p \gets not~\neg p]$, but not vice versa.
1149:
1150: Thus, $J_{\na{d}/x} \not\subseteq J_{\na{a}/x}$.
1151: \end{example}
1152:
1153: The final example shows that if we do not allow any rebuts as attacks,
1154: then we obtain a strictly more credulous semantics.
1155:
1156: \begin{example}\hspace{0cm}
1157: \label{ex:loop-neg}
1158: Consider the following program:
1159: \begin{center}
1160: %
1161: $\begin{array}{rcl}
1162: \neg p & \gets & not~q \\
1163: \neg q & \gets & not~p \\
1164: p \\
1165: q \\
1166: \end{array}$
1167: %
1168: \end{center}
1169: %
1170: Let $x$ be a notion of attack. Then
1171: $J_{\na{sa}/x} = J_{\na{d}/x} = J_{\na{a}/x} = \emptyset,$
1172: because every argument is strongly attacked (hence defeated and attacked),
1173: while
1174: $J_{\na{u}/x} = J_{\na{su}/x} = \{ [p], [q] \}.$
1175:
1176: Thus, in general, $J_{v/x} \not\subseteq J_{w/y}$, where $v \in \{
1177: \na{u}, \na{su} \}$, $w \in \{ \na{a}, \na{d}, \na{sa} \}$, and $x$
1178: and $y$ are any notions of attack.
1179: \end{example}
1180:
1181:
1182:
1183:
1184: \subsection{A hierarchy of argumentation semantics}
1185:
1186: We now summarise the results of this section, establishing a complete
1187: hierarchy of argumentation semantics, parametrised on a pair of
1188: notions of attack $x/y$ where $x$ stands for the attacks on an argument,
1189: and $y$ for the possible defence.
1190: We locate in this hierarchy
1191: the argumentation semantics of Dung~\cite{Dun93:ArgumentExplicit}
1192: and Prakken and Sartor~\cite{PS97:Argument}, as well as the
1193: well-founded semantics for normal logic programs~\cite{GRS91:WFS}.
1194: In Section~\ref{sec:wfsxarg} we will show that the paraconsistent
1195: well-founded semantics with explicit negation,
1196: WFSX$_p$~\cite{Dam96:Thesis},
1197: can also be found in our hierarchy.
1198: As a corollary, we obtain precise relationships between these well-known
1199: semantics and our argumentation semantics.
1200:
1201:
1202:
1203: \begin{theorem}
1204: \label{thm:hierarchy}
1205: The notions of justifiability are ordered (by set inclusion)
1206: according to the diagram in Figure~\ref{fig:hierarchy},
1207: where $x/y$ lies below $x'/y'$ iff $J_{x/y} \subsetneq J_{x'/y'}$.
1208: \end{theorem}
1209:
1210: \begin{proof}
1211: All equality and subset relationships (i.e. arcs between notions of
1212: justifiability) depicted in Figure~\ref{fig:hierarchy} are underpinned
1213: by the theorems in section \ref{sec:eq}. Two notions of
1214: justifiability are not subsets of each other iff they are not equal
1215: and not connected by an arc in Figure~\ref{fig:hierarchy}.
1216: These findings are underpinned by the counter-examples of section
1217: \ref{sec:ex}.
1218: \end{proof}
1219:
1220:
1221:
1222: \begin{figure}[htbp]
1223: \begin{center}
1224: \footnotesize $\xymatrix@C=-2em@R=3ex{ &&
1225: \na{su}/\na{a} = \na{su}/\na{d} \\ & \na{su}/\na{u} \ar@{-}[ru] &&
1226: \na{su}/\na{sa} \ar@{-}[lu] \\ \na{sa}/\na{u} = \na{sa}/\na{d} =
1227: \na{sa}/\na{a} \ar@{-}[ru] && \na{su}/\na{su} \ar@{-}[lu]
1228: \ar@{-}[ru] && \na{u}/\na{a} = \na{u}/\na{d} = \na{u}/\na{sa}
1229: \ar@{-}[lu] \\ & \na{sa}/\na{su} = \na{sa}/\na{sa} \ar@{-}[lu]
1230: \ar@{-}[ru] && \na{u}/\na{su} = \na{u}/\na{u} \ar@{-}[lu]
1231: \ar@{-}[ru] \\ && \na{d}/\na{su} = \na{d}/\na{u} = \na{d}/\na{a} =
1232: \na{d}/\na{d} = \na{d}/\na{sa} \ar@{-}[lu] \ar@{-}[ru] \\ &&
1233: \na{a}/\na{su} = \na{a}/\na{u} = \na{a}/\na{a} = \na{a}/\na{d} =
1234: \na{a}/\na{sa} \ar@{-}[u] \\ }$
1235:
1236: \caption{Hierarchy of Notions of Justifiability}
1237: \label{fig:hierarchy}
1238: \end{center}
1239: % \vspace{-3ex}
1240: \end{figure}
1241: %\vspace{-5ex}
1242: %
1243:
1244:
1245:
1246:
1247: By definition, Prakken and Sartor's semantics~\cite{PS97:Argument},
1248: if we disregard priorities, amounts to $\na{d}/\na{su}$-justifiability.
1249:
1250: Similarly, Dung's grounded argumentation semantics~%
1251: \cite{Dun93:ArgumentExplicit} is exactly $\na{a}/\na{u}$-justifiability;
1252: and if we treat explicitly negated literals as new atoms, we can
1253: apply the least fixpoint argumentation semantics for normal logic
1254: programs~\cite{Dun95:Argument,BDKT97:Argument} to extended logic programs,
1255: which is then, by definition, $\na{u}/\na{u}$-justifiability.
1256:
1257: Note that these latter semantics use a slightly different notation to
1258: ours: arguments are sets of assumptions (i.e.~default literals), and a
1259: conclusion of an argument is a literal that can be derived from these
1260: assumptions. This approach can be translated to ours by taking as
1261: arguments all those derivations of a conclusion from an argument.
1262: Then the definitions of the notions of attack and the fixpoint
1263: semantics coincide. See also the discussion in \cite{PS97:Argument}.
1264:
1265: As corollaries to Theorem~\ref{thm:hierarchy} we obtain relationships of
1266: these semantics to the other notions of justifiability.
1267:
1268:
1269: \begin{corollary}
1270: Let $J_{Dung}$ be the set of justified arguments according to
1271: Dung's grounded argumentation semantics~\cite{Dun93:ArgumentExplicit}.
1272: Then $J_{Dung}=J_{\na{a}/\na{su}}=J_{\na{a}/\na{u}}=J_{\na{a}/\na{a}}=J_{\na{a}/\na{d}}=J_{\na{a}/\na{sa}}$ and
1273: $J_{Dung} \subsetneq J_{x/y}$ for all notions of attack $x \not= \na{a}$ and $y$.
1274: Thus, in Dung's semantics, it does not matter which notion of attack, \na{su,u,a,d,sa},
1275: is used as a defence, and Dung's semantics is more sceptical than
1276: the others.
1277: \end{corollary}
1278:
1279: \begin{corollary}
1280: Let $J_{PS}$ be the set of justified arguments according to Prakken
1281: and Sartor's argumentation semantics~\cite{PS97:Argument}, where all
1282: arguments have the same priority. Then
1283: $J_{PS}=J_{\na{d}/\na{su}}=J_{\na{d}/\na{u}}=J_{\na{d}/\na{a}}=J_{\na{d}/\na{d}}=J_{\na{d}/\na{sa}}$,
1284: $J_{PS} \subsetneq J_{x/y}$ for all notions of attack $x \not\in
1285: \{\na{a},\na{d}\}$ and $y$, and $J_{PS} \supsetneq J_{\na{a}/y}$ for
1286: all notions of attack $y$. Thus, in Prakken and Sartor's semantics,
1287: it does not matter which notion of attack, \na{su,u,a,d,sa}, is used
1288: as a defence, and $J_{PS}$ is more credulous than Dung's semantics, but
1289: more sceptical than all the others.
1290: \end{corollary}
1291:
1292: \begin{corollary}
1293: Let $J_{WFS}$ be the set of justified argument according to the
1294: well-founded argumentation semantics for normal logic programs
1295: \cite{Dun95:Argument,BDKT97:Argument}, where an explicitly negated
1296: atom $\neg L$ is treated as unrelated to the positive atom $L$. Then
1297: $J_{WFS} = J_{\na{u}/\na{u}} = J_{\na{u}/\na{su}}$, $J_{WFS}
1298: \supsetneq J_{\na{d}/y} \supsetneq J_{\na{a}/y}$, $J_{WFS}
1299: \subsetneq J_{\na{su}/y}$, and $J_{WFS} \subsetneq J_{\na{u}/\na{a}}
1300: = J_{\na{u}/\na{d}} = J_{\na{u}/\na{sa}}$, for all notions of attack
1301: $y$. Thus, in contrast to Dung's and Prakken and Sartor's semantics,
1302: for WFS it makes a difference whether rebuts are permitted in the
1303: defence (\na{a,d,sa}) or not (\na{u,su}).
1304: \end{corollary}
1305:
1306:
1307:
1308:
1309: \begin{remark}\hspace{0cm}
1310: 1. The notions of $\na{a}/x$-, $\na{d}/x$- and $\na{sa}/x$-justifiability are
1311: particularly sceptical in that even a fact $p$ may not be justified, if there
1312: is a rule $\neg p \gets B$ (where $not~p \not\in B$) that is not
1313: $x$-attacked. On the other hand this is useful in terms of
1314: avoiding inconsistency.
1315:
1316: \noindent
1317: 2. $sx/y$-justifiability is particularly credulous,
1318: because it does not take into account non-strong attacks, so e.g.\
1319: the program $\{ p \gets not~q, q \gets not~p \}$ has the justified
1320: arguments $[p \gets not~q]$ and $[q \gets not~p]$.
1321:
1322: \end{remark}
1323:
1324: \begin{remark}
1325: One might ask whether any of the semantics in Figure~\ref{fig:hierarchy}
1326: are equivalent for {\em non-contradictory} programs, i.e.\ programs for
1327: which there is no literal $L$ such that there exist justified
1328: arguments for both $L$ and $\neg L$.
1329: The answer to this question is no: all the examples in Section \ref{sec:ex} distinguishing
1330: different notions of justifiability involve only non-contradictory
1331: programs.
1332:
1333: In particular, even for non-contradictory programs,
1334: Dung's and Prakken and Sartor's semantics differ, and
1335: both differ from $\na{u}/\na{a}$-justifiability, which will be shown equivalent to
1336: the paraconsistent well-founded semantics WFSX$_p$~\cite{Dam96:Thesis,PA92:WFSX,AP96:WFSX} in
1337: Section~\ref{sec:wfsxarg}.
1338: \end{remark}
1339:
1340:
1341: \section{Properties of Argumentation Semantics}
1342: \label{sec:properties}
1343:
1344: We will now state some important properties which a semantics for
1345: extended logic programs may have, and examine for which of the
1346: argumentation semantics these properties hold.
1347:
1348:
1349: \subsection{The coherence principle}
1350: \label{sec:coherence}
1351:
1352: The coherence principle for extended logic
1353: programming~\cite{AP96:WFSX} states that ``explicit negation implies
1354: implicit negation''. If the intended meaning of $not~L$ is ``if there
1355: is no evidence for $L$, assume that $L$ is false'', and the intended
1356: meaning of $\neg L$ is ``there is evidence for the falsity of $L$'',
1357: then the coherence principle states that explicit evidence is
1358: preferred over assumption of the lack of evidence. Formally, this can
1359: be stated as: if $\neg L$ is in the semantics, then $not~L$ is also in
1360: the semantics. In an argumentation semantics, we have not defined what
1361: it means for a default literal to be ``in the semantics''. This can
1362: easily be remedied, though, and for convenience we introduce the
1363: following transformation.\footnote{The purpose of the transformation
1364: could be equally achieved by defining that $not~L$ is $x/y$-justified
1365: if all arguments for $L$ are overruled.}
1366:
1367: \begin{definition}
1368: Let $P$ be an extended logic program, and $x$ and $y$ notions of attack,
1369: and let $L$ be an objective literal.
1370: Then $L$ is {\em $x/y$-justified} if there exists
1371: a $x/y$-justified argument for $L$.
1372:
1373: Let $nL$ be a fresh atom, and $P' = P \cup \{ nL \gets not~L \}$.
1374: Then $not~L$ is {\em $x/y$-justified} if $[ nL \gets not~L ]$ is
1375: a $x/y$-justified argument associated with $P'$.
1376: \end{definition}
1377: %
1378: Note that because $nL$ is fresh, then either $J_{x/y}(P') = J_{x/y}(P)$ or
1379: $J_{x/y}(P') = J_{x/y}(P) \cup \{ [ nL \gets not~L ] \}$.
1380:
1381:
1382: \begin{definition}
1383: A least fixpoint semantics $J_{x/y}$
1384: {\em satisfies the coherence principle} if
1385: for every objective literal $L$,
1386: if $\neg L$ is $x/y$-justified, then $not~L$ is
1387: $x/y$-justified.
1388: \end{definition}
1389:
1390: The following result states that a least fixpoint semantics satisfies
1391: the coherence principle exactly in those cases where we allow any
1392: attack for the defence.
1393: Informally, this is because the only way of attacking a default
1394: literal $not~L$ is by undercut, i.e.\ an argument for $L$, and in
1395: general, such an argument can only be attacked by an argument for
1396: $\neg L$ by a rebut.
1397:
1398: \begin{theorem}
1399: Let $x,y \in \{ \na{a}, \na{u}, \na{d}, \na{su}, \na{sa} \}$.
1400: Then $J_{x/y}$ satisfies the coherence principle
1401: iff $J_{x/y} = J_{x/\na{a}}$.
1402: \end{theorem}
1403:
1404: \begin{proof}
1405: \begin{itemize}
1406: \item For the ``only if'' direction, we show that for those notions
1407: of justifiability $x/y \not= x/\na{a}$, the coherence principle does
1408: not hold.
1409:
1410: \begin{itemize}
1411: \item Consider the program $P$:
1412:
1413: $\begin{array}{rcl}
1414: p & \gets & not~q \\
1415: q & \gets & not~r \\
1416: r & \gets & not~s \\
1417: s & \gets & not~p \\
1418: \neg p \\
1419: \end{array}$
1420:
1421: Then $J_{\na{u}/\na{u}}(P') = J_{\na{su}/\na{u}}(P') =
1422: J_{\na{su}/\na{su}}(P') = \{ [\neg p] \}$,
1423: where $P' = P \cup \{ np \gets not~p \}$.
1424: In these cases, the coherence principle is not satisfied, because
1425: $\neg p$ is justified, but $not~p$ is not justified.
1426: %
1427: \item Now consider the program $Q$:
1428:
1429: $\begin{array}{rcl}
1430: p & \gets & not~\neg p \\
1431: \neg p & \gets & not~p \\
1432: \end{array}$
1433:
1434: Then $J_{\na{su}/\na{sa}}(Q') = J_{\na{sa}/\na{sa}}(Q') =
1435: \{ [p \gets not~\neg p], [\neg p \gets not~p] \}$,
1436: where $Q' = Q \cup \{ np \gets not~p \}$.
1437: Again, the coherence principle is not satisfied, because
1438: $\neg p$ is justified, but $not~p$ is not justified.
1439: \\[1ex]
1440:
1441: \end{itemize}
1442:
1443: \item For the ``if'' direction, let $x$ be any notion of attack.
1444: %
1445: Let $P$ be an extended logic program, and
1446: $\neg L$ a $x/\na{a}$-justified literal,
1447: i.e.\ there is an argument $A = [ \neg L \gets Body, \ldots ]$
1448: and an ordinal $\alpha$ s.t.~$A \in J_{x/\na{a}}^\alpha$.
1449:
1450: Let $A' = [ nL \gets not~L ]$, and $(B,A') \in x$.
1451: Because $nL$ is fresh, the only possible attack on $A'$ is
1452: a strong undercut, i.e.\ $L$ is a conclusion of $B$.
1453: Then $A$ attacks $B$, and so $[ nL \gets not~L ] \in
1454: J_{x/\na{a}}^{\alpha+1}$.
1455:
1456: \end{itemize}
1457: \end{proof}
1458:
1459:
1460:
1461: \subsection{Consistency}
1462: \label{sec:consistency}
1463:
1464: Consistency is an important property of a logical system. It states
1465: that the system does not support contradictory conclusions. In
1466: classical logic ``ex falso quodlibet'', i.e.\ if both $A$ and $\neg A$
1467: hold, then any formula holds.
1468: In paraconsistent systems~\cite{DP98:Paraconsistent}, this property
1469: does not hold, thus allowing both $A$ and $\neg A$ to hold for a
1470: particular formula $A$, while not supporting any other contradictions.
1471:
1472: A set of arguments is \emph{consistent}, or
1473: \emph{conflict-free}~\cite{PS97:Argument,Dun95:Argument},
1474: if it does not contain two arguments
1475: such that one attacks the other. There are several notions of
1476: consistency, depending on which notion of attack is considered
1477: undesirable.
1478:
1479: \begin{definition}
1480: Let $x$ be a notion of attack, and $P$ an extended logic program.
1481: Then a set of arguments associated with $P$ is called
1482: \emph{$x$-consistent} if it does not contain arguments $A$ and $B$ such
1483: that $(A,B) \in x_P$.
1484: \end{definition}
1485:
1486: The argumentation semantics of an extended logic program need not
1487: necessarily be consistent; because of explicit negation, there exist
1488: contradictory programs such as $\{ p, \neg p \}$, for which there
1489: exist sensible, but inconsistent arguments ($[p]$ and $[\neg p]$ in
1490: this case).
1491:
1492: A general result identifies cases in which the set of justified arguments
1493: for a program is consistent. It states that if we allow the attack to
1494: be at least as strong as the defence, i.e.\ if we are
1495: {\em sceptical}, then the set of justified arguments is
1496: consistent.
1497:
1498: \begin{theorem}
1499: Let $x$ and $y$ be notions of attack such that $x \!\supseteq\! y$,
1500: and let $P$ be an extended logic program.
1501: Then the set of $x/y$-justified arguments is $x$-consistent.
1502: \end{theorem}
1503:
1504: \begin{proof}
1505: We show that $J_{x/y}^\alpha$ is $x$-consistent for all
1506: ordinals $\alpha$, by transfinite induction on $\alpha$.
1507:
1508: \noindent {\it Base case} $\alpha=0$: Trivial.
1509:
1510: \noindent {\it Successor ordinal} $\alpha \leadsto \alpha+1$:
1511: Assume $A,B \in J_{x/y}^{\alpha+1}$ and $(A,B) \in x$.
1512: Then there exists $C \in J_{x/y}^\alpha$ such that
1513: $(C,A) \in y \subseteq x$. Then by induction hypothesis,
1514: because $C \in J_{x/y}^\alpha$, then $A \not\in J_{x/y}^\alpha$.
1515: Because $A \in J_{x/y}^{\alpha+1}$, there exists
1516: $D \in J_{x/y}^\alpha$ such that $(D,C) \in y \subseteq x$.
1517: This contradicts the induction hypothesis, so we have to retract
1518: the assumption and conclude that $J_{x/y}^{\alpha+1}$ is
1519: $x$-consistent.
1520:
1521: \noindent {\it Limit ordinal $\lambda$:}
1522: Assume $A, B \in J_{x/y}^\lambda$ and $(A,B) \in x$.
1523: Then there exist $\alpha, \beta < \lambda$ s.t.~$A \in J_{x/y}^\alpha$ and
1524: $B \in J_{x/y}^\beta$. W.l.o.g. assume that $\alpha \leq \beta$.
1525: Then because $J_{x/y}^\alpha \subseteq J_{x/y}^\beta$, we have
1526: $A \in J_{x/y}^\beta$, contradicting the induction hypothesis that
1527: $J_{x/y}^\beta$ is $x$-consistent.
1528: %
1529: \end{proof}
1530:
1531: The following example shows that, in general, the set of justified
1532: arguments may well be inconsistent.
1533:
1534: \begin{example}
1535: Consider the following program:
1536: \begin{center}
1537: %
1538: $\begin{array}{rcl}
1539: q & \gets & not~p \\
1540: p \\
1541: \neg p
1542: \end{array}$
1543: %
1544: \end{center}
1545: Then $J_{\na{u}/\na{a}} = \{ [q \gets not~p], [p], [\neg p] \}$,
1546: and $[p]$ and $[\neg p]$ rebut each other, and
1547: $[p]$ strongly undercuts $[q \gets not~p]$.
1548: \end{example}
1549:
1550:
1551:
1552: \section{Argumentation Semantics and WFSX}
1553: \label{sec:wfsxarg}
1554:
1555: In this section we will prove that the argumentation semantics
1556: $J_{\na{u}/\na{a}}$ is equivalent to the paraconsistent well-founded semantics
1557: with explicit negation WFSX$_p$~\cite{Dam96:Thesis,AP96:WFSX}.
1558: First, we summarise the definition of WFSX$_p$.
1559:
1560: \subsection{Well-founded semantics with explicit negation}
1561: \label{sec:wfsx}
1562:
1563: We recollect the definition of the paraconsistent well-founded semantics for
1564: extended logic programs, WFSX$_p$. We use the definition of~\cite{ADP95:LPsystem},
1565: because it is closer to our definition of argumentation semantics than
1566: the original definition of~\cite{PA92:WFSX}.
1567:
1568: \begin{definition}
1569: The set of all objective literals of a program $P$ is
1570: called the {\em Herbrand base} of $P$ and denoted by $\herbrand(P)$.
1571: A {\em paraconsistent interpretation} of a program $P$ is a set
1572: $T \cup not~F$ where $T$ and $F$ are subsets of $\herbrand(P)$.
1573: An {\em interpretation} is a paraconsistent interpretation where the
1574: sets $T$ and $F$
1575: are disjoint. An interpretation is called {\em two-valued} if
1576: $T \cup F = \herbrand(P)$.
1577: \end{definition}
1578:
1579:
1580: \begin{definition}
1581: Let $P$ be an extended logic program, $I$ an interpretation, and let
1582: $P'$ (resp.~$I'$) be obtained from $P$ (resp.~$I$) by replacing
1583: every literal $\neg A$ by a new atom, say $\neg\_A$. The
1584: GL-transformation $\frac{P'}{I'}$ is the program obtained from $P'$
1585: by removing all rules containing a default literal $not~A$ such that
1586: $A \in I'$, and then removing all remaining default literals from
1587: $P'$, obtaining a definite program $P''$. Let $J$ be the least
1588: model of $P''$, i.e. $J$ is the least fixpoint of $T_{P''}(I) :=
1589: \{A~|~~\exists A\gets B_1,\dots,B_n \in P'' \mbox{ s.t. } B_i \in
1590: I\}$. Then $\Gamma_P I$ is obtained from $J$ by replacing the introduced
1591: atoms $\neg\_A$ by $\neg A$.
1592: \end{definition}
1593:
1594: \begin{definition}
1595: The {\em semi-normal} version of a program $P$ is the program $P_s$
1596: obtained from $P$ by replacing every rule $L \gets Body$ in $P$ by
1597: the rule $L \gets not~\neg L, Body$. If the program $P$ is clear
1598: from the context, we write $\Gamma I$ for $\Gamma_P I$ and $\Gamma_s
1599: I$ for $\Gamma_{P_s} I$.
1600: \end{definition}
1601:
1602: Note that the set $\Gamma_P I$ is just a set of literals; we will now
1603: use it to define the semantics of $P$ as a (paraconsistent) interpretation.
1604:
1605: \begin{definition}%(WFSX)
1606: Let $P$ be a program whose least fixpoint of $\Gamma \Gamma_s$ is $T$.
1607: Then the {\em paraconsistent well-founded model of $P$} is
1608: the paraconsistent interpretation
1609: $WFM_p(P) = T \cup not~(\herbrand(P) - \Gamma_s T)$.
1610: If $WFM_p(P)$ is an interpretation, then
1611: $P$ is called {\em non-contradictory},
1612: and $WFM_p(P)$ is the {\em well-founded model of $P$},
1613: denoted by $WFM(P)$.
1614: \end{definition}
1615: %
1616: The paraconsistent well-founded model can be defined iteratively by
1617: the transfinite sequence $\{I_\alpha\}$:
1618:
1619: \begin{tabular}{llll}
1620: $I_0$ & := & $\emptyset$ \\
1621: $I_{\alpha+1}$ & := & $\Gamma \Gamma_s I_\alpha$ &
1622: for successor ordinal $\alpha+1$ \\
1623: $I_\lambda$ & := & $\bigcup_{\alpha < \lambda} I_\alpha$ &
1624: for limit ordinal $\lambda$ \\
1625: \end{tabular}
1626:
1627: \noindent
1628: There exists a smallest ordinal $\lambda_0$ such that $I_{\lambda_0}$
1629: is the least fixpoint of $\Gamma \Gamma_s$, and \linebreak
1630: $WFM_p(P) := I_{\lambda_0} \cup not~(\herbrand(P) - \Gamma_s I_{\lambda_0})$.
1631:
1632:
1633: \subsection{Equivalence of argumentation semantics and WFSX$_p$}
1634:
1635: In this section, we will show that the argumentation semantics
1636: $J_{\na{u}/\na{a}}$ and the well-founded model coincide. That is, the
1637: conclusions of justified arguments are exactly the objective literals
1638: which are true in the well-founded model; and those objective literals
1639: all of whose arguments are overruled are exactly the literals which
1640: are false in the well-founded model. The result holds also for
1641: contradictory programs under the {\em paraconsistent} well-founded
1642: semantics. This is important, because it shows that contradictions in
1643: the argumentation semantics are precisely the contradictions under the
1644: well-founded semantics, and allows the application of contradiction
1645: removal (or avoidance) methods to the argumentation semantics
1646: \cite{sch97c}. For non-contradictory programs, the
1647: well-founded semantics coincides with the paraconsistent well-founded
1648: semantics~\cite{AP96:WFSX,Dam96:Thesis}; consequently, we obtain as a corollary that
1649: argumentation semantics and well-founded semantics coincide for
1650: non-contradictory programs.
1651:
1652: Before we come to the main theorem, we need
1653: the following Lemma, which shows a precise connection between arguments and
1654: consequences of a program $\frac{P}{I}$.
1655: \begin{lemma}
1656: \label{lemma:model-arg}
1657: Let $I$ be a two-valued interpretation.
1658: \begin{enumerate}
1659: \item \label{lemma:model-arg:u}
1660: $L \in \Gamma(I)$ iff $\exists$ argument $A$ with conclusion $L$
1661: such that $\assm(A) \subseteq I$.
1662: \item \label{lemma:model-arg:a}
1663: $L \in \Gamma_s(I)$ iff $\exists$ argument $A$ with conclusion $L$
1664: such that $\assm(A) \subseteq I$ and
1665: $\neg\conc(A) \cap I = \emptyset$.
1666: \item \label{lemma:model-arg:u-neg}
1667: $L \not\in \Gamma(I)$ iff $\forall$ arguments $A$ with conclusion $L$,
1668: $\assm(A) \cap I \not\subseteq \emptyset$.
1669: \item \label{lemma:model-arg:a-neg}
1670: $L \not\in \Gamma_s(I)$ iff $\forall$ arguments $A$ with
1671: conclusion $L$, $\assm(A) \cap I \not\subseteq \emptyset$
1672: or $\neg\conc(A) \cap I \not= \emptyset$.
1673: \end{enumerate}
1674: \end{lemma}
1675: %
1676: \begin{proof}
1677: See \ref{appendix}.
1678: \end{proof}
1679:
1680:
1681: In order to compare the argumentation semantics with the well-founded
1682: semantics, we extend the definition $\conc(A)$ of the conclusions of a
1683: single argument $A$ to work on a set of arguments $\mathcal{A}$.
1684: The extended definition $\conc(\mathcal{A})$ includes all positive and
1685: negative conclusions of arguments in $\mathcal{A}$; i.e. those
1686: literals $L \in \conc(\mathcal{A})$, as well as the default literals
1687: $not~L$ where all arguments for $L$ are overruled by some argument
1688: $A\in\mathcal{A}$.
1689: We will use this definition of $\conc$ for the set
1690: of justified arguments $J_{\na{u/a}}$ to compare the ``argumentation
1691: model'' $\conc(J_{\na{u/a}})$ to $WFM_p(P)$, the well-founded model.
1692:
1693: \begin{definition}
1694: Let $\mathcal{A}$ be a set of arguments. Then
1695: $$\conc(\mathcal{A}) = \bigcup_{A\in\mathcal{A}} \conc(A) \cup \{ not~L~~|~ \mbox{all arguments for } L \mbox{ are overruled by an argument } A\in\mathcal{A}\}$$
1696: \end{definition}
1697:
1698: With the above definition, we can formulate the main theorem that
1699: $\na{u/a}$-justified arguments coincide with the well-founded
1700: semantics.
1701:
1702: \begin{theorem}
1703: \label{thm:wfsxarg}
1704: Let $P$ be an extended logic program.
1705: Then $WFM_p(P) = \conc(J_{\na{u/a}})$.
1706: \end{theorem}
1707:
1708: \begin{proof}
1709: First, note that $A$ undercuts $B$ iff
1710: $\exists~L$ s.t.\ $L \in \conc(A)$ and $not~L \in \assm(B)$;
1711: and $A$ rebuts $B$ iff $\exists~L \in \conc(A) \cap \neg\conc(B)$.\\[2ex]
1712: %
1713: We show that for all ordinals $\alpha$, $I_\alpha =
1714: \conc(J^\alpha_{\na{u/a}})$, by transfinite induction on
1715: $\alpha$. The proof proceeds in two stages. First, we show that all
1716: objective literals $L$ in $WFM_p(P)$ are conclusions of
1717: $\na{u/a}$-justified arguments and second, that for all default
1718: negated literals $not~L$ in $WFM_p(P)$, all arguments for $L$ are
1719: overruled. \\[0.5ex]
1720: %
1721: \textit{Base case $\alpha=0$:}
1722: $I_\alpha = \emptyset = \conc(J^\alpha_{\na{u/a}})$
1723: \\[0.5ex]
1724: %
1725: \textit{Successor ordinal $\alpha \leadsto \alpha+1$}:\\[0.5ex]
1726: %
1727: $L \in I_{\alpha+1}$ \\
1728: \mycenter{iff (Def.\ of $I_{\alpha+1}$)} \\
1729: $L \in \Gamma \Gamma_s I_\alpha$ \\
1730: \mycenter{iff (Lemma~\ref{lemma:model-arg}(\ref{lemma:model-arg:u}))} \\
1731: $\exists$~argument $A$ for $L$ such that
1732: $\assm(A) \subseteq \Gamma_s I_\alpha$ \\
1733: \mycenter{iff (Def.\ of $\subseteq$, and $\Gamma_s I_\alpha$
1734: is two-valued)} \\
1735: $\exists$~argument $A$ for $L$ such that
1736: $\forall~not~L \in \assm(A), L \not\in \Gamma_s I_\alpha$ \\
1737: \mycenter{iff (Lemma~\ref{lemma:model-arg}(\ref{lemma:model-arg:a-neg}))} \\
1738: $\exists$~argument $A$ for $L$ such that $\forall~not~L \in \assm(A)$,
1739: for any argument $B$ for $L$,
1740: ( $\exists~not~L' \in \assm(B) ~s.t.\ L' \in I_\alpha$
1741: or $\exists~L'' \in \conc(B) ~s.t.\ \neg L'' \in I_\alpha$ ) \\
1742: \mycenter{iff (Induction hypothesis)} \\
1743: $\exists$~argument $A$ for $L$ such that $\forall~not~L \in \assm(A)$,
1744: for any argument $B$ for $L$,
1745: ( $\exists~not~L' \in \assm(B) ~s.t.\ \exists$
1746: argument $C \in J^\alpha_{\na{u/a}}$ for $L'$,
1747: or $\exists~L'' \in \conc(B) ~s.t.\ \exists$~
1748: argument $C \in J_{\na{u/a}}^\alpha$ for $\neg L''$) \\
1749: \mycenter{iff (Def.\ of undercut and rebut)} \\
1750: $\exists$~argument $A$ for $L$ such that for any undercut $B$ to $A$,
1751: ( $\exists$~argument $C \in J_{\na{u/a}}^\alpha$ s.t.\
1752: $C$ undercuts $B$,
1753: or $\exists$~argument $C \in J_{\na{u/a}}^\alpha$ s.t.\
1754: $C$ rebuts $B$) \\
1755: \mycenter{iff} \\
1756: $\exists$~argument $A$ for $L$ such that for any undercut $B$ to $A$,
1757: $\exists$~argument $C \in J_{\na{u/a}}^\alpha$ s.t.\ $C$ attacks $B$ \\
1758: \mycenter{iff (Def.\ of $J_{\na{u/a}}^{\alpha+1}$)} \\
1759: $\exists$~argument $A \in J_{\na{u/a}}^{\alpha+1}$ for $L$ \\
1760: \mycenter{iff (Def.\ of $\conc$)}\\
1761: $L \in \conc(J_{\na{u/a}}^{\alpha+1})$\\[0.5ex]
1762: %
1763: \textit{Limit ordinal $\lambda$:}\\
1764: $I_\lambda = \bigcup_{\alpha < \lambda} I_\alpha$ and
1765: $J_{\na{u/a}}^\lambda = \bigcup_{\alpha < \lambda} J_{\na{u/a}}^\alpha$,
1766: so by induction hypothesis ($I_\alpha = \conc(J_{\na{u/a}}^\alpha)$ for all $\alpha < \lambda$),
1767: $I_\lambda = \conc(J_{\na{u/a}}^\lambda)$.\\[2ex]
1768: %
1769: Next we will show that a literal $not~L$ is in the well-founded semantics
1770: iff every argument for $L$ is overruled, i.e.
1771: $not~L \in WFM_p(P)$ implies
1772: $not~L \in \conc(J_{\na{u/a}})$.\\[0.5ex]
1773: %
1774: $not~L \in WFM_p(P)$ \\
1775: \mycenter{iff (Def.\ of $WFM_p(P)$)} \\
1776: $L \not\in \Gamma_s I_\lambda$ \\
1777: \mycenter{iff (Lemma~\ref{lemma:model-arg}(\ref{lemma:model-arg:a-neg})} \\
1778: for all arguments $A$ for $L$,
1779: ( $\exists~not~L' \in \assm(A) ~s.t.\ L' \in I_\lambda$, or
1780: $\exists~L'' \in \conc(A) ~s.t.\ \neg L'' \in I_\lambda$ ) \\
1781: \mycenter{iff ($I_\lambda=\conc(J_{\na{u/a}}^\lambda)$)} \\
1782: for all arguments $A$ for $L$,
1783: ( $\exists ~not~L' \in \assm(A) ~s.t.\
1784: \exists$~argument $B \in J_{\na{u/a}}^\lambda$ for $L'$, or
1785: $\exists~L'' \in \conc(A) ~s.t.\
1786: \exists$~argument $B \in J_{\na{u/a}}^\lambda$ for $\neg L''$ ) \\
1787: \mycenter{iff (Def.\ of undercut and rebut)} \\
1788: for all arguments $A$ for $L$,
1789: ( $\exists$~argument $B \in J_{\na{u/a}}^\lambda$ s.t.\ $B$ undercuts $A$, or
1790: $\exists$~argument $B \in J_{\na{u/a}}^\lambda$ s.t.\ $B$ rebuts $A$ ) \\
1791: \mycenter{iff} \\
1792: every argument for $L$ is attacked by a justified argument in $J_{\na{u/a}}^\lambda$ \\
1793: \mycenter{iff (Def.\ of overruled)} \\
1794: every argument for $L$ is overruled \\
1795: \mycenter{iff (Def.\ of $\conc(J_{\na{u/a}})$)} \\
1796: $not~L \in \conc(J_{\na{u/a}})$
1797: \end{proof}
1798:
1799: \begin{corollary}
1800: Let $P$ be a non-contradictory program. Then $WFM(P) = \conc(J_{\na{u/a}})$.
1801: \end{corollary}
1802:
1803: \begin{remark}
1804: In a similar way, one can show that the $\Gamma$ operator corresponds
1805: to undercuts, while the $\Gamma_s$ operator corresponds to attacks, and so
1806: the least fixpoints of $\Gamma\Gamma$, $\Gamma_s\Gamma$, and
1807: $\Gamma_s\Gamma_s$ correspond to $J_{\na{u}/\na{u}}$, $J_{\na{a}/\na{u}}$, and $J_{\na{a}/\na{a}}$,
1808: respectively.
1809: In~\cite{ADP95:LPsystem}, the least fixpoints of these operators are
1810: shown to be ordered as
1811: $lfp(\Gamma_s\Gamma) \subseteq lfp(\Gamma_s\Gamma_s) \subseteq
1812: lfp(\Gamma\Gamma_s)$, and
1813: $lfp(\Gamma_s\Gamma) \subseteq lfp(\Gamma\Gamma) \subseteq
1814: lfp(\Gamma\Gamma_s)$.
1815: Because $J_{\na{a}/\na{u}} = J_{\na{a}/\na{a}} \subseteq J_{\na{u}/\na{u}} \subseteq J_{\na{u}/\na{a}}$ by
1816: Theorem~\ref{thm:hierarchy}, we can strengthen this statement
1817: to $lfp(\Gamma_s\Gamma) = lfp(\Gamma_s\Gamma_s) \subseteq
1818: lfp(\Gamma\Gamma) \subseteq lfp(\Gamma\Gamma_s)$.
1819: \end{remark}
1820:
1821:
1822: The following corollary summarises the results so far.
1823:
1824: \begin{corollary}
1825: The least fixpoint argumentation semantics of
1826: Dung~\cite{Dun93:ArgumentExplicit}, denoted $\mathbf{J_{Dung}}$,
1827: of Prakken and Sartor~\cite{PS97:Argument}, denoted $\mathbf{J_{PS}}$,
1828: and the well-founded semantics
1829: for normal logic programs \textbf{WFS}~\cite{BDKT97:Argument,GRS91:WFS}
1830: and for logic programs with explicit negation
1831: \textbf{WFSX$_p$}~\cite{PA92:WFSX,AP96:WFSX} are related to
1832: the other least fixpoint argumentation semantics as illustrated in
1833: Figure~\ref{fig:compare-hierarchy}.
1834: \end{corollary}
1835:
1836:
1837: \begin{figure}[htbp]
1838: \begin{center}
1839: $\xymatrix@C=-2em@R=3ex{
1840: && \na{su}/\na{a} = \na{su}/\na{d} \\
1841: & \na{su}/\na{u} \ar@{-}[ru] && \na{su}/\na{sa} \ar@{-}[lu] \\
1842: \na{sa}/\na{u} = \na{sa}/\na{d} = \na{sa}/\na{a}
1843: \ar@{-}[ru] &&
1844: \na{su}/\na{su} \ar@{-}[lu] \ar@{-}[ru] &&
1845: {\makebox[10em]{\hspace{-5em}$\na{u}/\na{a} = \na{u}/\na{d} = \na{u}/\na{sa} = $\textbf{WFSX$_p$}}}
1846: \ar@{-}[lu] \\
1847: & \na{sa}/\na{su} = \na{sa}/\na{sa} \ar@{-}[lu] \ar@{-}[ru] &&
1848: {\makebox[10em]{\hspace{5em}$\na{u}/\na{su} = \na{u}/\na{u} = $\textbf{WFS}}}
1849: \ar@{-}[lu] \ar@{-}[ru] \\
1850: && {\makebox[10em]{$\na{d}/\na{su} = \na{d}/\na{u} = \na{d}/\na{a} = \na{d}/\na{d} = \na{d}/\na{sa} =
1851: \mathbf{J_{PS}}$}}
1852: \ar@{-}[lu] \ar@{-}[ru] \\
1853: && {\makebox[10em]{$\na{a}/\na{su} = \na{a}/\na{u} = \na{a}/\na{a} = \na{a}/\na{d} = \na{a}/\na{sa} =
1854: \mathbf{J_{Dung}}$}}
1855: \ar@{-}[u] \\
1856: }$
1857: \caption{Hierarchy of Notions of Justifiability and Existing Semantics}
1858: \label{fig:compare-hierarchy}
1859: \end{center}
1860: \end{figure}
1861:
1862:
1863: \section{Proof Theory}
1864: \label{sec:proof-theory}
1865:
1866: One of the benefits of relating the argumentation semantics $J_{\na{u}/\na{a}}$ to
1867: WFSX$_p$ is the existence of an efficient top-down proof procedure for
1868: WFSX$_p$~\cite{ADP95:LPsystem},
1869: which we can use to compute justified arguments in $J_{\na{u}/\na{a}}$.
1870: On the other hand, {\em dialectical} proof theories, based on dialogue trees,
1871: have been defined for a variety of argumentation semantics
1872: \cite{SCG94:Dialectics,PS97:Argument,JV99:DialecticSemantics,KT99:ComputingArgumentation}.
1873: In this section we present a sound and complete dialectical proof theory for
1874: the least fixpoint argumentation semantics $J_{x/y}$ for any
1875: notions of attack $x$ and $y$.
1876:
1877:
1878: \subsection{Dialogue trees}
1879:
1880: We adapt the dialectical proof theory of~\cite{PS97:Argument} to
1881: develop a general sound and complete proof theory for
1882: $x/y$-justified arguments.
1883:
1884: \begin{definition}
1885: \label{def:dialog}
1886: Let $P$ be an extended logic program.
1887: An {\em $x/y$-dialogue} is a finite nonempty sequence of
1888: moves $move_i = (\mathit{Player}_i,Arg_i) (i > 0)$, such that
1889: $Player_i \in \{P,O\}$, $Arg_i \in \mathit{Args}_P$, and
1890: \begin{enumerate}
1891: \item $\mathit{Player}_i = P$ iff $i$ is odd; and
1892: $\mathit{Player}_i = O$ iff $i$ is even.
1893: \item If $\mathit{Player}_i = \mathit{Player}_j = P$ and $i \not= j$,
1894: then $Arg_i \not= Arg_j$.
1895: \item \label{item:minimal} If $\mathit{Player}_i = P$ and $i > 1$, then
1896: $Arg_i$ is a minimal argument such that $(Arg_i,Arg_{i-1}) \in y$.
1897: \item If $\mathit{Player}_i = O$, then $(Arg_i,Arg_{i-1}) \in x$.
1898: \end{enumerate}
1899: \end{definition}
1900:
1901: The first condition states that the players $P$ (Proponent) and
1902: $O$ (Opponent) take turns, and $P$ starts.
1903: The second condition prevents the proponent from repeating a move.
1904: The third and fourth conditions state that both players have to
1905: attack the other player's last move, where the opponent is allowed
1906: to use the notion of attack $x$, while the proponent may use $y$ to
1907: defend its arguments.
1908: Note that the minimality condition in~\ref{item:minimal} is redundant,
1909: because {\em all} arguments in $\mathit{Args}_P$ are required
1910: to be minimal by Definition~\ref{def:argument}.
1911: We have explicitly repeated this condition, because it is important
1912: in that it prevents the proponent from repeating an argument by adding
1913: irrelevant rules to it.
1914:
1915: \begin{definition}
1916: \label{def:dialogtree}
1917: An {\em $x/y$-dialogue tree} is a tree of moves such that
1918: every branch is a $x/y$-dialogue, and for all moves $move_i = (P, Arg_i)$,
1919: the children of $move_i$ are all those moves $(O,Arg_j)$ such that
1920: $(Arg_j,Arg_i) \in x$.\\
1921: The {\em height} of a dialogue tree is $0$ if it consists only of
1922: the root, and otherwise $height(t) = sup \{ height(t_i) \} + 1$ where
1923: $t_i$ are the trees rooted at the grandchildren of $t$.
1924: \end{definition}
1925:
1926: \begin{example}
1927: Consider the following program:
1928: \begin{center}
1929: %
1930: $\begin{array}{rcl}
1931: p & \gets & q, not~r \\
1932: q & \gets & not~s \\
1933: \neg q & \gets & u\\
1934: r & \gets & not~t \\
1935: s & \gets & not~t \\
1936: t & \gets & not~w \\
1937: u & \gets & not~v \\
1938: v & \gets & not~r \\
1939: \neg v & \gets & not~t
1940: \end{array}$
1941: %
1942: \end{center}
1943: A $\na{a}/\na{u}$-dialogue tree rooted at the argument
1944: $[p \gets q, not~r; q \gets not~s]$ is given by Figure~\ref{fig:tree}.
1945: Each node is marked with $P$ for proponent or $O$ for opponent,
1946: and an edge $\xymatrix{A \ar[r]^x & B}$ denotes that $A$ attacks $B$
1947: with the notion of attack $x$, i.e.~$(A,B) \in x$.
1948: \begin{figure}[htbp]
1949: $$\xymatrix{
1950: & P:[p \gets q, not~r; q \gets not~s] \\
1951: O:[r \gets not~t] \ar[ru]^{\na{u}} &
1952: O:[\neg q \gets u; u \gets not~v] \ar[u]^{\na{r}} &
1953: O:[s \gets not~t] \ar[lu]_{\na{u}} \\
1954: P:[t \gets not~w] \ar[u]^{\na{u}} &
1955: P:[v \gets not~r] \ar[u]^{\na{u}} &
1956: P:[t \gets not~w] \ar[u]^{\na{u}} \\
1957: & O:[r \gets not~t] \ar[u]^{\na{u}} &
1958: O:[\neg v \gets not~t] \ar[lu]_{\na{r}} \\
1959: & P:[t \gets not~w] \ar[u]^{\na{u}} &
1960: P:[t \gets not~w] \ar[u]^{\na{u}} \\
1961: }$$
1962: \caption{An $\na{a}/\na{u}$-dialogue tree}
1963: \label{fig:tree}
1964: \end{figure}
1965: %
1966: \end{example}
1967: %
1968: Note that although dialogues are required to be finite, dialogue trees
1969: may be infinitely branching. Therefore dialogue trees need not be
1970: finite, nor need their height be finite.
1971:
1972: \begin{example}
1973: Consider the following program $P$
1974: \footnote{Note that by definition, programs are not allowed to contain
1975: variables. Here, $X$ denotes a variable, and $P$ is an abbreviation
1976: for the (infinite) program obtained by substituting the terms $s^n(0)$
1977: for the variable $X$, in all the rules.}:
1978: \begin{center}
1979: %
1980: $\begin{array}{rcl}
1981: p(0) \\
1982: p(s(X)) & \gets & not~q(X) \\
1983: q(X) & \gets & not~p(X) \\
1984: r & \gets & q(X) \\
1985: s & \gets & not~r \\
1986: \end{array}$
1987: %
1988: \end{center}
1989: For each $n \in \mathbb{N}$, there is exactly one minimal argument $A_n$
1990: with conclusion $p(s^n(0))$, namely $[p(0)]$ for $n=0$, and
1991: $[p(s^n(0)) \gets not~q(s^{n-1}(0))]$ for $n > 0$.
1992: Similarly, there is exactly one minimal argument $B_n$ with conclusion
1993: $q(s^n(0))$, namely $[q(s^n(0)) \gets not~p(s^n(0))]$.\\
1994: Therefore, a $\na{u}/\na{u}$-dialogue tree rooted at $A_{n+1}$ consists
1995: of just one dialogue $T_{n+1}$ of the form
1996: $( (P, A_{n+1}), (O, B_{n}), T_n )$. A $\na{u}/\na{u}$-dialogue tree
1997: rooted at $A_0$ consists only of the root, because there are no
1998: undercuts to $A_0$. Thus, the height of the dialogue tree $T_n$ is $n$.\\
1999: Now consider the $\na{u}/\na{u}$-dialogue tree rooted at the argument
2000: $C = [s \gets not~r]$. The argument $C$ is undercut by infinitely many
2001: arguments $D_n = [r \gets q(s^n(0)); q(s^n(0)) \gets not~p(s^n(0))]$;
2002: each $D_n$ is undercut by exactly one argument: $A_n$.
2003: A dialogue in the $\na{u}/\na{u}$-dialogue tree $T_C$ rooted at
2004: argument $C$ is therefore a sequence $( (P, C), (O, B_n), T_n )$.
2005: Because $\mathit{height}(T_n)=n$, then by Definition~\ref{def:dialogtree}:
2006: $\mathit{height}(T_C) =
2007: \mathit{sup} \{ \mathit{height}(T_n) ~|~ n \in \mathbb{N} \} + 1 =
2008: \omega + 1$.
2009: \end{example}
2010:
2011: \begin{definition}
2012: \label{def:windialogtree}
2013: A player {\em wins an $x/y$-dialogue} iff the other player cannot move.
2014: A player {\em wins an $x/y$-dialogue tree} iff it wins all branches
2015: of the tree. An $x/y$-dialogue tree which is won by the proponent
2016: is called a {\em winning $x/y$-dialogue tree}.
2017: \end{definition}
2018:
2019: We show that the proof theory of $x/y$-dialogue trees is sound and
2020: complete for any notions of attack $x$ and $y$.
2021:
2022: \begin{theorem}
2023: \label{thm:sound-complete}
2024: An argument $A$ is $x/y$-justified iff there exists a $x/y$-dialogue
2025: tree with $A$ as its root, and won by the proponent.
2026: \end{theorem}
2027:
2028: \begin{proof}
2029: We show by transfinite induction that for all arguments $A$,
2030: for all ordinals $\alpha$:
2031: $A \in J^{\alpha}_{x/y}$ if and only if
2032: there exists a winning $x/y$-dialogue tree of height $\leq \alpha$
2033: for $A$.
2034: See \ref{appendix} for the detailed proof.
2035: \end{proof}
2036:
2037:
2038:
2039:
2040:
2041:
2042:
2043:
2044:
2045:
2046:
2047:
2048:
2049:
2050: \section{Related Work}
2051:
2052: There has been much work on argument-theoretic semantics for
2053: normal logic programs, i.e. logic programs with default negation~%
2054: \cite{BDKT97:Argument,Dun95:Argument,KT99:ComputingArgumentation}.
2055: Because there is no explicit negation, there is only one form of
2056: attack, the {\em undercut} in our terminology.
2057: An abstract argumentation framework has been defined, which captures
2058: other default reasoning mechanisms besides normal logic programming.
2059: Within this framework, a variety of semantics may be defined,
2060: such as \emph{preferred extensions}; \emph{stable extensions}, which are
2061: equivalent to \emph{stable models}~\cite{GL88:StableModels};
2062: and a least fixpoint semantics based on the acceptability of arguments,
2063: which is equivalent to the \emph{well-founded semantics}~\cite{GRS91:WFS}.
2064: The latter fixpoint semantics forms the basis of our argumentation semantics.
2065: Proof theories and proof procedures for some of these argumentation
2066: semantics have been developed in~\cite{KT99:ComputingArgumentation}.
2067:
2068:
2069: There has been some work extending this argumentation semantics
2070: to logic programs with explicit negation. Dung~\cite{Dun95:Argument}
2071: adapts the framework of~\cite{Dun93:ArgumentExplicit}, by distinguishing
2072: between {\em ground attacks} and {\em reductio-ad-absurdum-attacks},
2073: in our terminology undercuts and rebuts. Argumentation semantics analogous to
2074: those of normal logic programs are defined, and the stable extension
2075: semantics is shown to be equivalent to the answer set
2076: semantics~\cite{GL90:ClassicalNegation}, an adaptation of the stable
2077: model semantics to extended logic programs. A least fixpoint semantics
2078: (called {\em grounded} semantics) based on a notion of acceptability
2079: is defined, and related to the well-founded semantics of~\cite{GRS91:WFS},
2080: although only for the case of programs without explicit negation.
2081:
2082: Prakken and Sartor~\cite{PS97:Argument} define an argumentation
2083: semantics for extended logic programs similar to that of Dung.
2084: Their language is more expressive in that it distinguishes between
2085: {\em strict} rules, which may not be attacked, and {\em defeasible}
2086: rules, which may be attacked. Furthermore, rules have priorities, and
2087: rebuts are only permitted against a rule of equal or lower priority.
2088: Thus, rebuts are not necessarily symmetric, as in our setting. Our
2089: language corresponds to Prakken and Sartor's without strict rules,
2090: and either without priorities,
2091: or, equivalently, if all rules have the same priority. The semantics
2092: is given as a least fixpoint of an acceptability operator, analogous
2093: to Dung's grounded semantics. A proof theory, similar to those of
2094: Kakas and Toni~\cite{KT99:ComputingArgumentation} is developed. This
2095: proof theory formed the basis of our general proof theory for
2096: justified arguments.
2097:
2098: In \cite{MA98:Argumentation}, an argumentation semantics for extended
2099: logic programs, similar to
2100: Prakken and Sartor's, is proposed; it is influenced by WFSX, and
2101: distinguishes between sceptical and credulous conclusions of an
2102: argument. It also provides a proof theory based on dialogue trees,
2103: similar to Prakken and Sartor's.
2104:
2105:
2106: Defeasible Logic Programming
2107: \cite{GS03:DeLP,SCG94:Dialectics,GSC98:Argument}
2108: is a formalism very similar to Prakken and Sartor's,
2109: based on the first order logic argumentation framework of \cite{SL92:MTDR}.
2110: It includes logic programming with two kinds of negation,
2111: distinction between strict and defeasible rules, and allowing for
2112: various criteria for comparing arguments.
2113: Its semantics is given operationally, by proof procedures based on
2114: dialectical trees \cite{GS03:DeLP,SCG94:Dialectics}.
2115: In \cite{DCSS02:DefeasibleTransformation}, the semantics of Defeasible
2116: Logic Programming is related to the well-founded semantics, albeit
2117: only for the restricted language corresponding to normal logic programs
2118: \cite{GRS91:WFS}.
2119:
2120:
2121: The answer set semantics for extended logic
2122: programs~\cite{GL90:ClassicalNegation} is defined via extensions which
2123: are stable under a certain program transformation. While this
2124: semantics is a natural extension of stable
2125: models~\cite{GL88:StableModels} and provides an elegant
2126: model-theoretic semantics, there are several drawbacks which the
2127: answer set semantics inherits from the stable models. In particular,
2128: there is no efficient top-down proof procedure for the answer set
2129: semantics, because the truth value of a literal $L$ may depend on the
2130: truth value of a literal $L'$ which does {\em not} occur in the proof
2131: tree below $L$~\footnote{See the extensive discussion
2132: in~\cite{AP96:WFSX} for details.}.
2133: The well-founded semantics~\cite{GRS91:WFS} is an
2134: approximation of the stable model semantics, for which an efficient
2135: top-down proof procedure exists. In~\cite{Prz90:ExtendedStable}, the
2136: well-founded semantics is adapted to extended logic programs.
2137: However, this semantics does not comply with the {\em coherence
2138: principle}, which states that explicit negation implies implicit
2139: negation. In order to overcome this, \cite{PA92:WFSX,AP96:WFSX}
2140: developed WFSX, a well-founded semantics for extended logic programs,
2141: which satisfies the coherence principle. It has several
2142: desirable properties not enjoyed by the answer set semantics; in
2143: particular, an efficient goal-oriented top-down proof procedure for
2144: WFSX is presented in~\cite{ADP95:LPsystem}. WFSX is well established
2145: and e.g. widely available through Prolog implementations such as XSB
2146: Prolog \cite{frssw97}.
2147:
2148: Our own work is complementary to these approaches, in that we fill a
2149: gap by bringing argumentation and WFSX together in our definition of
2150: $\na{u/a}$-justified arguments, which are equivalent to WFSX$_p$
2151: \cite{Dam96:Thesis,AP96:WFSX,ADP95:LPsystem}, the
2152: paraconsistent version of WFSX. Furthermore, the generality of our framework allows us to relate
2153: existing argumentation semantics such as Dung's and Prakken and
2154: Sartor's approach and thus provide a concise characterisation of all
2155: the existing semantics mentioned above.
2156:
2157:
2158:
2159: A number of authors \cite{KSE98:Argument,par96,sie97,PSJ98:AgentsArguing,stt01,tor02,Sch99:Argument,MA98:Argumentation}
2160: work on argumentation for negotiating agents. Of these, the approaches
2161: of \cite{stt01,tor02,Sch99:Argument} are based on logic programming.
2162: The advantage of the logic programming approach for arguing agents
2163: is the availability of
2164: goal-directed, top-down proof procedures. This is vital when
2165: implementing systems which need to react in real-time and therefore
2166: cannot afford to compute {\em all} justified arguments, as would be
2167: required when a bottom-up argumentation semantics would be used.
2168:
2169: In \cite{stt01,tor02}, abduction is used to define agent negotiation
2170: focusing on the generation of negotiation dialogues using
2171: abduction. This work is relevant in that it shows how to embed an
2172: argumentation proof procedure into a dialogue protocol, which is
2173: needed to apply proof procedures of argumentation semantics as defined
2174: in this paper into agent communication languages such as
2175: KQML~\cite{Fin94:KQML} or FIPA ACL~\cite{fipa}.
2176:
2177: With a variety of argument-based approaches being pursued to define
2178: negotiating agents, the problem of how these agents may inter-operate
2179: arises. This paper could serve as a first step towards inter-operation
2180: as existing approaches can be placed in our framework, thus making it
2181: easier to compare them.
2182:
2183:
2184:
2185: \section{Conclusion and Further Work}
2186: \label{sec:conclusion}
2187:
2188: We have identified various notions of attack for extended logic
2189: programs. Based on these notions of attack, we defined notions of
2190: acceptability and least fixpoint semantics. The contributions of this
2191: paper are five-fold.
2192:
2193: \begin{itemize}
2194: \item
2195: First, we defined a parameterised hierarchy of argumentation semantics
2196: by establishing a lattice of justified arguments based on set
2197: inclusion. We showed which argumentation semantics are equal, which
2198: are subsets of one another and which are neither.
2199:
2200: \item
2201: Second, we examined some properties of the different
2202: semantics, and gave a necessary and sufficient condition for a
2203: semantics to satisfy the coherence principle~\cite{AP96:WFSX}, and a
2204: sufficient criterion for a semantics to be consistent.
2205:
2206: \item Third, we identified an argumentation semantics
2207: $J_{\na{u}/\na{a}}$ equal to the paraconsistent well-founded
2208: semantics for logic programs with explicit negation,
2209: WFSX$_p$~\cite{Dam96:Thesis,AP96:WFSX} and proved this equivalence.
2210:
2211: \item
2212: Forth, we established relationships between existing semantics, in
2213: particular that $J_{Dung} \subsetneq J_{PS} \subsetneq
2214: J_{\na{u}/\na{u}} = WFS \subsetneq J_{\na{u}/\na{a}} = WFSX_p$, where
2215: $J_{Dung}$ and $J_{PS}$ are the least fixpoint argumentation semantics
2216: of Dung~\cite{Dun93:ArgumentExplicit} and Prakken and
2217: Sartor~\cite{PS97:Argument}, and $WFS$ is the well-founded semantics
2218: without explicit negation~\cite{GRS91:WFS}.
2219:
2220: \item Fifth, we have defined a
2221: dialectical proof theory for argumentation. For all notions of
2222: justified arguments introduced, we prove that the proof theory is
2223: sound and complete wrt. the corresponding fixpoint argumentation
2224: semantics.
2225: \end{itemize}
2226:
2227:
2228: It remains to be seen whether a variation in the notion of attack
2229: yields interesting variations of alternative argumentation semantics
2230: for extended logic programs such as preferred extensions or stable
2231: extensions~\cite{Dun93:ArgumentExplicit}. It is also an open question
2232: how the hierarchy changes when priorities are added as defined
2233: in~\cite{ant02,kak02,PS97:Argument,Bre96:DynamicPreferences,GSC98:Argument,%
2234: Vre97:AbstractArgumentationSystems}.
2235:
2236:
2237: \subsection*{Acknowledgement}
2238: Thanks to Iara Carnevale de Almeida and Jos\'e J\'ulio Alferes for
2239: fruitful discussions on credulous and sceptical argumentation
2240: semantics for extended logic programming.\\
2241: This work has been supported by EPSRC grant GRM88433.
2242:
2243: %\bibliographystyle{alpha}
2244: %\bibliography{jarglp}
2245:
2246: \begin{thebibliography}{}
2247:
2248: \bibitem[\protect\citeauthoryear{Alferes, Dam\'asio, and Pereira}{Alferes
2249: et~al\mbox{.}}{1995}]{ADP95:LPsystem}
2250: {\sc Alferes, J.~J.}, {\sc Dam\'asio, C.~V.}, {\sc and} {\sc Pereira, L.~M.}
2251: 1995.
2252: \newblock A logic programming system for non-monotonic reasoning.
2253: \newblock {\em {Journal of Automated Reasoning}\/}~{\em 14,\/}~1, 93--147.
2254:
2255: \bibitem[\protect\citeauthoryear{Alferes, Dung, and Pereira}{Alferes
2256: et~al\mbox{.}}{1993}]{ADP93:ScenarioSemantics}
2257: {\sc Alferes, J.~J.}, {\sc Dung, P.~M.}, {\sc and} {\sc Pereira, L.~M.} 1993.
2258: \newblock Scenario semantics for extended logic programming.
2259: \newblock In {\em {Proceedings of the Second International Workshop on Logic
2260: Programming and Non-monotonic Reasoning (LPNMR'93)}}. MIT Press, 334--348.
2261:
2262: \bibitem[\protect\citeauthoryear{Alferes and Pereira}{Alferes and
2263: Pereira}{1996}]{AP96:WFSX}
2264: {\sc Alferes, J.~J.} {\sc and} {\sc Pereira, L.~M.} 1996.
2265: \newblock {\em Reasoning with Logic Programming}.
2266: \newblock LNAI 1111, Springer-Verlag.
2267:
2268: \bibitem[\protect\citeauthoryear{Antoniou}{Antoniou}{2002}]{ant02}
2269: {\sc Antoniou, G.} 2002.
2270: \newblock Defeasible logic with dynamic priorities.
2271: \newblock In {\em {Proceedings of the 15th European Conference on Artificial
2272: Intelligence}}. IOS Press, Lyon, France, 521--525.
2273:
2274: \bibitem[\protect\citeauthoryear{Belnap}{Belnap}{1977}]{Bel77:FourValued}
2275: {\sc Belnap, N.~D.} 1977.
2276: \newblock A useful four-valued logic.
2277: \newblock In {\em Modern Uses of Many-valued Logic}, {G.~Epstein} {and} {J.~M.
2278: Dunn}, Eds. Reidel Publishing Company, 8--37.
2279:
2280: \bibitem[\protect\citeauthoryear{Birkhoff}{Birkhoff}{1967}]{Bir67:LatticeTheor%
2281: y}
2282: {\sc Birkhoff, G.} 1967.
2283: \newblock {\em Lattice Theory\/}, 3rd ed.
2284: \newblock American Mathematical Society.
2285:
2286: \bibitem[\protect\citeauthoryear{Bondarenko, Dung, Kowalski, and
2287: Toni}{Bondarenko et~al\mbox{.}}{1997}]{BDKT97:Argument}
2288: {\sc Bondarenko, A.}, {\sc Dung, P.}, {\sc Kowalski, R.}, {\sc and} {\sc Toni,
2289: F.} 1997.
2290: \newblock An abstract, argumentation-theoretic approach to default reasoning.
2291: \newblock {\em {Artificial Intelligence}\/}~{\em 93,\/}~1-2, 63--101.
2292:
2293: \bibitem[\protect\citeauthoryear{Brewka}{Brewka}{1996}]{Bre96:DynamicPreferenc%
2294: es}
2295: {\sc Brewka, G.} 1996.
2296: \newblock Well-founded semantics for extended logic programs with dynamic
2297: preferences.
2298: \newblock {\em {Journal of Artificial Intelligence Research}\/}~{\em 4},
2299: 19--36.
2300:
2301: \bibitem[\protect\citeauthoryear{Ches{\~{n}}evar, Dix, Stolzenburg, and
2302: Simari}{Ches{\~{n}}evar
2303: et~al\mbox{.}}{2002}]{DCSS02:DefeasibleTransformation}
2304: {\sc Ches{\~{n}}evar, C.~I.}, {\sc Dix, J.}, {\sc Stolzenburg, F.}, {\sc and}
2305: {\sc Simari, G.~R.} 2002.
2306: \newblock Relating defeasible and normal logic programming through
2307: transformation properties.
2308: \newblock {\em {Theoretical Computer Science}\/}~{\em 290,\/}~1, 499--529.
2309:
2310: \bibitem[\protect\citeauthoryear{Ches{\~n}evar, Maguitman, and
2311: Loui}{Ches{\~n}evar et~al\mbox{.}}{2000}]{CML00:LogicalModelsOfArgument}
2312: {\sc Ches{\~n}evar, C.~I.}, {\sc Maguitman, A.~G.}, {\sc and} {\sc Loui, R.~P.}
2313: 2000.
2314: \newblock Logical models of argument.
2315: \newblock {\em {ACM Computing Surveys}\/}~{\em 32,\/}~4 (December), 337--383.
2316:
2317: \bibitem[\protect\citeauthoryear{Chiariglione et~al\mbox{.}}{Chiariglione
2318: et~al\mbox{.}}{1997}]{fipa}
2319: {\sc Chiariglione, L.} {\sc et~al\mbox{.}} 1997.
2320: \newblock Specification version 2.0.
2321: \newblock Tech. rep., Foundations of Intelligent Physical Agents.
2322: \newblock http://www.fipa.org.
2323:
2324: \bibitem[\protect\citeauthoryear{Clark}{Clark}{1978}]{cla78}
2325: {\sc Clark, K.~L.} 1978.
2326: \newblock Negation as failure.
2327: \newblock In {\em {Logic and Databases}}, {Gallaire} {and} {Minker}, Eds.
2328: Plenum Press, New York, 293--322.
2329:
2330: \bibitem[\protect\citeauthoryear{Dam\'asio}{Dam\'asio}{1996}]{Dam96:Thesis}
2331: {\sc Dam\'asio, C.~V.} 1996.
2332: \newblock Paraconsistent extended logic programming with constraints.
2333: \newblock Ph.D. thesis, Universidade Nova de Lisboa.
2334:
2335: \bibitem[\protect\citeauthoryear{Dam{\'a}sio and Pereira}{Dam{\'a}sio and
2336: Pereira}{1998}]{DP98:Paraconsistent}
2337: {\sc Dam{\'a}sio, C.~V.} {\sc and} {\sc Pereira, L.~M.} 1998.
2338: \newblock A survey on paraconsistent semantics for extended logic programs.
2339: \newblock In {\em {Handbook of Defeasible Reasoning and Uncertainty
2340: Management}}, {D.~M. Gabbay} {and} {P.~Smets}, Eds. Vol.~2. Kluwer Academic
2341: Publishers, 241--320.
2342:
2343: \bibitem[\protect\citeauthoryear{Dam\'asio, Pereira, and Schroeder}{Dam\'asio
2344: et~al\mbox{.}}{1997}]{sch97c}
2345: {\sc Dam\'asio, C.~V.}, {\sc Pereira, L.~M.}, {\sc and} {\sc Schroeder, M.}
2346: 1997.
2347: \newblock {REVISE}: Logic programming and diagnosis.
2348: \newblock In {\em {Proceedings of the Conference on Logic Programming and
2349: Non-monotonic Reasoning LPNMR97}}. LNAI 1265, Springer--Verlag, 353--362.
2350:
2351: \bibitem[\protect\citeauthoryear{Dung}{Dung}{1993}]{Dun93:ArgumentExplicit}
2352: {\sc Dung, P.~M.} 1993.
2353: \newblock An argumentation semantics for logic programming with explicit
2354: negation.
2355: \newblock In {\em {Proc. of the 10th International Conference on Logic
2356: Programming ICLP'93}}. MIT Press, 616--630.
2357:
2358: \bibitem[\protect\citeauthoryear{Dung}{Dung}{1995}]{Dun95:Argument}
2359: {\sc Dung, P.~M.} 1995.
2360: \newblock On the acceptability of arguments and its fundamental role in
2361: nonmonotonic reasoning, logic programming and n-person games.
2362: \newblock {\em {Artificial Intelligence}\/}~{\em 77,\/}~2, 321--357.
2363:
2364: \bibitem[\protect\citeauthoryear{Finin, Fritzson, McKay, and McEntire}{Finin
2365: et~al\mbox{.}}{1994}]{Fin94:KQML}
2366: {\sc Finin, T.}, {\sc Fritzson, R.}, {\sc McKay, D.}, {\sc and} {\sc McEntire,
2367: R.} 1994.
2368: \newblock {KQML} as an agent communication lanugage.
2369: \newblock In {\em {Proceedings of the Third International Conference on
2370: Information and Knowledge Management (CIKM'94)}}. ACM Press, 456--463.
2371:
2372: \bibitem[\protect\citeauthoryear{Freire, Rao, Sagonas, Switft, and
2373: Warren}{Freire et~al\mbox{.}}{1997}]{frssw97}
2374: {\sc Freire, J.}, {\sc Rao, P.}, {\sc Sagonas, K.}, {\sc Switft, T.}, {\sc and}
2375: {\sc Warren, D.~S.} 1997.
2376: \newblock {XSB}: A system for efficiently computing the well-founded semantics.
2377: \newblock In {\em {International Workshop on Logic Programming and
2378: Non-monotonic Reasoning}}. 431--441.
2379:
2380: \bibitem[\protect\citeauthoryear{Garc\'{\i}a and Simari}{Garc\'{\i}a and
2381: Simari}{2004}]{GS03:DeLP}
2382: {\sc Garc\'{\i}a, A.~J.} {\sc and} {\sc Simari, G.~R.} 2004.
2383: \newblock Defeasible logic programming: An argumentative approach.
2384: \newblock {\em {Theory and Practice of Logic Programming}\/}~{\em 4,\/}~1.
2385:
2386: \bibitem[\protect\citeauthoryear{Garc{\'\i}a, Simari, and
2387: Ches{\~n}evar}{Garc{\'\i}a et~al\mbox{.}}{1998}]{GSC98:Argument}
2388: {\sc Garc{\'\i}a, A.~J.}, {\sc Simari, G.~R.}, {\sc and} {\sc Ches{\~n}evar,
2389: C.~I.} 1998.
2390: \newblock An argumentative framework for reasoning with inconsistent and
2391: incomplete information.
2392: \newblock In {\em {ECAI'98 Workshop on Practical Reasoning and Rationality}}.
2393: Brighton, UK.
2394:
2395: \bibitem[\protect\citeauthoryear{Gelfond and Lifschitz}{Gelfond and
2396: Lifschitz}{1988}]{GL88:StableModels}
2397: {\sc Gelfond, M.} {\sc and} {\sc Lifschitz, V.} 1988.
2398: \newblock The stable model semantics for logic programming.
2399: \newblock In {\em {Proceedings of the 5th International Conference on Logic
2400: Programming}}, {R.~A. Kowalski} {and} {K.~A. Bowen}, Eds. MIT Press,
2401: 1070--1080.
2402:
2403: \bibitem[\protect\citeauthoryear{Gelfond and Lifschitz}{Gelfond and
2404: Lifschitz}{1990}]{GL90:ClassicalNegation}
2405: {\sc Gelfond, M.} {\sc and} {\sc Lifschitz, V.} 1990.
2406: \newblock Logic programs with classical negation.
2407: \newblock In {\em {Proceedings of the 7th International Conference on Logic
2408: Programming}}. MIT Press, 579--597.
2409:
2410: \bibitem[\protect\citeauthoryear{Jakobovits and Vermeir}{Jakobovits and
2411: Vermeir}{1999a}]{JV99:DialecticSemantics}
2412: {\sc Jakobovits, H.} {\sc and} {\sc Vermeir, D.} 1999a.
2413: \newblock Dialectic semantics for argumentation frameworks.
2414: \newblock In {\em {Proceedings of the Seventh International Conference on
2415: Artificial Intelligence and Law (ICAIL '99)}}. 53--62.
2416:
2417: \bibitem[\protect\citeauthoryear{Jakobovits and Vermeir}{Jakobovits and
2418: Vermeir}{1999b}]{JV99:RobustSemantics}
2419: {\sc Jakobovits, H.} {\sc and} {\sc Vermeir, D.} 1999b.
2420: \newblock Robust semantics for argumentation frameworks.
2421: \newblock {\em {Journal of Logic and Computation}\/}~{\em 9,\/}~2, 215--261.
2422:
2423: \bibitem[\protect\citeauthoryear{Kakas and Toni}{Kakas and
2424: Toni}{1999}]{KT99:ComputingArgumentation}
2425: {\sc Kakas, A.} {\sc and} {\sc Toni, F.} 1999.
2426: \newblock Computing argumentation in logic programming.
2427: \newblock {\em {Journal of Logic and Computation}\/}~{\em 9,\/}~4, 515--562.
2428:
2429: \bibitem[\protect\citeauthoryear{Kakas and Moraitis}{Kakas and
2430: Moraitis}{2002}]{kak02}
2431: {\sc Kakas, A.~C.} {\sc and} {\sc Moraitis, P.} 2002.
2432: \newblock Argumentative agent deliberation, roles and context.
2433: \newblock In {\em {Proceedings of the ICLP-Workshop Computational Logic in
2434: Multi-Agent Systems}}.
2435:
2436: \bibitem[\protect\citeauthoryear{Kraus, Sycara, and Evenchik}{Kraus
2437: et~al\mbox{.}}{1998}]{KSE98:Argument}
2438: {\sc Kraus, S.}, {\sc Sycara, K.}, {\sc and} {\sc Evenchik, A.} 1998.
2439: \newblock Reaching agreements through argumentation: a logical model and
2440: implementation.
2441: \newblock {\em {Artificial Intelligence}\/}~{\em 104,\/}~1-2, 1--69.
2442:
2443: \bibitem[\protect\citeauthoryear{M\'ora and Alferes}{M\'ora and
2444: Alferes}{1998}]{MA98:Argumentation}
2445: {\sc M\'ora, I.~A.} {\sc and} {\sc Alferes, J.~J.} 1998.
2446: \newblock Argumentative and cooperative multi-agent system for extended logic
2447: programming.
2448: \newblock In {\em Proceedings of the 14th Brazilian Symposium on Artificial
2449: Intelligence (SBIA'98)}. 161--170.
2450:
2451: \bibitem[\protect\citeauthoryear{Parsons and Jennings}{Parsons and
2452: Jennings}{1996}]{par96}
2453: {\sc Parsons, S.} {\sc and} {\sc Jennings, N.} 1996.
2454: \newblock Negotiation through argumentation-a preliminary report.
2455: \newblock In {\em {Proceedings of the Second International Conference on
2456: Multi-Agent Systems}}. Kyoto, Japan, 267--274.
2457:
2458: \bibitem[\protect\citeauthoryear{Parsons, Sierra, and Jennings}{Parsons
2459: et~al\mbox{.}}{1998}]{PSJ98:AgentsArguing}
2460: {\sc Parsons, S.}, {\sc Sierra, C.}, {\sc and} {\sc Jennings, N.} 1998.
2461: \newblock Agents that reason and negotiate by arguing.
2462: \newblock {\em {Journal of Logic and Computation}\/}~{\em 8,\/}~3, 261--292.
2463:
2464: \bibitem[\protect\citeauthoryear{Pereira and Alferes}{Pereira and
2465: Alferes}{1992}]{PA92:WFSX}
2466: {\sc Pereira, L.~M.} {\sc and} {\sc Alferes, J.~J.} 1992.
2467: \newblock Well founded semantics for logic programs with explicit negation.
2468: \newblock In {\em {B. Neumann (Ed.), European Conference on Artificial
2469: Intelligence}}. Wiley, 102--106.
2470:
2471: \bibitem[\protect\citeauthoryear{Pollock}{Pollock}{1987}]{Pol87:Defeasible}
2472: {\sc Pollock, J.~L.} 1987.
2473: \newblock Defeasible reasoning.
2474: \newblock {\em {Cognitive Science}\/}~{\em 11}, 481--518.
2475:
2476: \bibitem[\protect\citeauthoryear{Prakken and Sartor}{Prakken and
2477: Sartor}{1997}]{PS97:Argument}
2478: {\sc Prakken, H.} {\sc and} {\sc Sartor, G.} 1997.
2479: \newblock Argument-based extended logic programming with defeasible priorities.
2480: \newblock {\em {Journal of Applied Non-Classical Logics}\/}~{\em 7,\/}~1,
2481: 25--75.
2482:
2483: \bibitem[\protect\citeauthoryear{Przymusinski}{Przymusinski}{1990}]{Prz90:Exte%
2484: ndedStable}
2485: {\sc Przymusinski, T.} 1990.
2486: \newblock Extended stable semantics for normal and disjunctive programs.
2487: \newblock In {\em {Proceedings of the 7th International Conference on Logic
2488: Programming}}. MIT Press, 459--477.
2489:
2490: \bibitem[\protect\citeauthoryear{Sadri, Toni, and Torroni}{Sadri
2491: et~al\mbox{.}}{2001}]{stt01}
2492: {\sc Sadri, F.}, {\sc Toni, F.}, {\sc and} {\sc Torroni, P.} 2001.
2493: \newblock Logic agents, dialogue, negotiation - an abductive approach.
2494: \newblock In {\em {Proceedings of the {AISB} Symposium on Information Agents
2495: for E-commerce}}.
2496:
2497: \bibitem[\protect\citeauthoryear{Schroeder}{Schroeder}{1999}]{Sch99:Argument}
2498: {\sc Schroeder, M.} 1999.
2499: \newblock An efficient argumentation framework for negotiating autonomous
2500: agents.
2501: \newblock In {\em {Proceedings of Modelling Autonomous Agents in a Multi-Agent
2502: World MAAMAW99}}. LNAI1647, Springer-Verlag.
2503:
2504: \bibitem[\protect\citeauthoryear{Schweimeier and Schroeder}{Schweimeier and
2505: Schroeder}{2002}]{sch02a}
2506: {\sc Schweimeier, R.} {\sc and} {\sc Schroeder, M.} 2002.
2507: \newblock Notions of attack and justified arguments for extended logic
2508: programs.
2509: \newblock In {\em {Proceedings of the 15th European Conference on Artificial
2510: Intelligence}}. IOS Press, Lyon, France, 536--540.
2511:
2512: \bibitem[\protect\citeauthoryear{Sierra, Jennings, Noriega, and Parsons}{Sierra
2513: et~al\mbox{.}}{1997}]{sie97}
2514: {\sc Sierra, C.}, {\sc Jennings, N.}, {\sc Noriega, P.}, {\sc and} {\sc
2515: Parsons, S.} 1997.
2516: \newblock A framework for argumentation-based negotiation.
2517: \newblock In {\em {Proc. Fourth Int. Workshop on Agent Theories, Architectures
2518: and Languages (ATAL-97)}}. Springer-Verlag, 167--182.
2519:
2520: \bibitem[\protect\citeauthoryear{Simari, Ches{\~{n}}evar, and
2521: Garc\'{\i}a}{Simari et~al\mbox{.}}{1994}]{SCG94:Dialectics}
2522: {\sc Simari, G.~R.}, {\sc Ches{\~{n}}evar, C.~I.}, {\sc and} {\sc Garc\'{\i}a,
2523: A.~J.} 1994.
2524: \newblock The role of dialectics in defeasible argumentation.
2525: \newblock In {\em {Anales de la XIV Conferencia Internacional de la Sociedad
2526: Chilena para Ciencias de la Computaci\'on}}. Universidad de Concepci\'on,
2527: Concepci\'on (Chile).
2528:
2529: \bibitem[\protect\citeauthoryear{Simari and Loui}{Simari and
2530: Loui}{1992}]{SL92:MTDR}
2531: {\sc Simari, G.~R.} {\sc and} {\sc Loui, R.~P.} 1992.
2532: \newblock A mathematical treatment of defeasible reasoning and its
2533: implementation.
2534: \newblock {\em {Artificial Intelligence}\/}~{\em 53}, 125--157.
2535:
2536: \bibitem[\protect\citeauthoryear{Tarski}{Tarski}{1955}]{Tar55:Fixpoint}
2537: {\sc Tarski, A.} 1955.
2538: \newblock A lattice-theoretical fixpoint theorem and its applications.
2539: \newblock {\em {Pacific Journal of Mathematics}\/}~{\em 5}, 285--309.
2540:
2541: \bibitem[\protect\citeauthoryear{Torroni}{Torroni}{2002}]{tor02}
2542: {\sc Torroni, P.} 2002.
2543: \newblock A study on the termination of negotiation dialogues.
2544: \newblock In {\em {Proceedings of Autonomous Agents and Multi Agent Systems
2545: 2002}}. ACM Press, 1223--1230.
2546:
2547: \bibitem[\protect\citeauthoryear{{van Gelder}, Ross, and Schlipf}{{van Gelder}
2548: et~al\mbox{.}}{1991}]{GRS91:WFS}
2549: {\sc {van Gelder}, A.}, {\sc Ross, K.~A.}, {\sc and} {\sc Schlipf, J.~S.} 1991.
2550: \newblock The well-founded semantics for general logic programs.
2551: \newblock {\em {Journal of the ACM}\/}~{\em 38,\/}~3 (July), 620--650.
2552:
2553: \bibitem[\protect\citeauthoryear{Vreeswijk}{Vreeswijk}{1997}]{Vre97:AbstractAr%
2554: gumentationSystems}
2555: {\sc Vreeswijk, G. A.~W.} 1997.
2556: \newblock Abstract argumentation systems.
2557: \newblock {\em {Artificial Intelligence}\/}~{\em 90,\/}~1--2, 225--279.
2558:
2559: \bibitem[\protect\citeauthoryear{Wagner}{Wagner}{1994}]{wag94a}
2560: {\sc Wagner, G.} 1994.
2561: \newblock {\em Vivid Logic -- Knowledge-Based Reasoning with Two Kinds of
2562: Negation}. Vol. LNAI 764.
2563: \newblock Springer--Verlag.
2564:
2565: \end{thebibliography}
2566:
2567:
2568: \appendix
2569:
2570: \section{Proofs of Theorems}
2571: \label{appendix}
2572:
2573: %\setcounter{theorem}{\ref{thm:subset-just}}
2574: %\addtocounter{theorem}{-1}
2575: % This is theorem 3. (set the counter to theorem number minus one.)
2576: \setcounter{theorem}{2}
2577:
2578: \begin{theorem}
2579: % \label{thm:subset-just}
2580: Let $x' \subseteq x$ and $y \subseteq y'$ be notions of attack, then
2581: $J_{x/y} \subseteq J_{x'/y'}$.
2582: \end{theorem}
2583:
2584: \begin{proof}
2585: We show by transfinite induction that
2586: $J^\alpha_{x/y} \subseteq J^\alpha_{x'/y'}$, for all $\alpha$.
2587:
2588: \noindent {\it Base case}: $\alpha = 0$:
2589: Then $J_{x/y} = \emptyset = J_{x'/y'}$.
2590:
2591: \noindent {\it Successor ordinal}: $\alpha \leadsto \alpha + 1$:
2592:
2593: Let $A \in J^{\alpha+1}_{x/y}$, and $(B,A) \in x'$.
2594: Then also $(B,A) \in x$, and so there exists $C \in J^\alpha_{x/y}$
2595: such that $(C,B) \in y$, so also $(C,B) \in y'$.
2596: By induction hypothesis, $C \in J^\alpha_{x'/y'}$,
2597: and so $A \in J^{\alpha+1}_{x'/y'}$.
2598:
2599: \noindent {\it Limit ordinal} $\lambda$:
2600:
2601: Assume $J_{x/y}^\alpha \subseteq J_{x'/y}^\alpha$ for all $\alpha < \lambda$.
2602: Then
2603:
2604: $J^\lambda_{x/y} = \bigcup_{\alpha < \lambda} J^\alpha_{x/y} \subseteq
2605: \bigcup_{\alpha < \lambda} J^\alpha_{x'/y'} = J^\lambda_{x'/y'}$
2606: %
2607: \end{proof}
2608:
2609:
2610: %\setcounter{theorem}{\ref{thm:strong-nonstrong}}
2611: %\addtocounter{theorem}{-1}
2612: % This is Theorem 4.
2613: \setcounter{theorem}{3}
2614: \begin{theorem}
2615: % \label{thm:strong-nonstrong}
2616: Let $x$ and and $y$ be notions of attack such that
2617: $x \supseteq \na{undercuts}$, and let
2618: $sy = y - \na{undercuts}^{-1}$.
2619: Then $J_{x/y} = J_{x/sy}$.
2620: \end{theorem}
2621:
2622: \begin{proof}
2623: % Informally, every $x$-attack $B$ to an $x/y$-justified argument $A$ is
2624: % $y$-defended by some $x/sy$-justified argument $C$ (by induction).
2625: % Now if $C$ was {\em not} a $sy$-attack, then it is undercut by $B$,
2626: % and because $x \supseteq \na{undercuts}$ and
2627: % $C$ is justified, there exists a {\em strong} defence
2628: % for $C$ against $B$, which is also a defence of the original
2629: % argument $A$ against $C$.\\[2ex]
2630: %%
2631: % The formal proof is by transfinite induction.
2632: By Theorem~\ref{thm:subset-just}, we have $J_{x/sy} \subseteq J_{x/y}$.
2633: We prove the inverse inclusion by showing that
2634: for all ordinals $\alpha$:
2635: $J_{x/y}^\alpha \subseteq J_{x/sy}^\alpha$,
2636: by transfinite induction on $\alpha$.\\[1ex]
2637: %
2638: {\it Base case} $\alpha=0$:
2639: %
2640: $J_{x/y} = \emptyset = J_{x/sy}$.\\[1ex]
2641: %
2642: {\it Successor ordinal } $\alpha \leadsto \alpha+1$:
2643: %
2644: Let $A \in J_{x/y}^{\alpha+1}$, and $(B,A) \in x$.
2645: By definition, there exists $C \in J_{x/y}^\alpha$ such that
2646: $(C,B) \in y$. By induction hypothesis, $C \in J_{x/sy}^\alpha$.
2647:
2648: If $B$ does not undercut $C$, then we are done.
2649: If, however, $B$ undercuts $C$, then because
2650: $C \in J_{x/sy}^\alpha$, and $\na{undercuts} \subseteq x$,
2651: there exists
2652: $D \in J_{x/sy}^{\alpha_0} (\alpha_0 < \alpha)$ such that
2653: $(D,B) \in sy$. It follows that $A \in J_{x/sy}^{\alpha+1}$.\\[1ex]
2654: %
2655: {\it Limit ordinal $\lambda$: }
2656: %
2657: Assume $J_{x/y}^\alpha \subseteq J_{x/sy}^\alpha$ for all $\alpha < \lambda$.
2658: Then
2659: $J_{x/y}^\lambda = \bigcup_{\alpha<\lambda}J_{x/y}^\alpha \subseteq
2660: \bigcup_{\alpha<\lambda}J_{x/sy}^\alpha = J_{x/sy}^\lambda$
2661: %
2662: \end{proof}
2663:
2664:
2665:
2666: %\setcounter{theorem}{\ref{thm:xu-xa-just}}
2667: %\addtocounter{theorem}{-1}
2668: % This is Theorem 6.
2669: \setcounter{theorem}{5}
2670: \begin{theorem}
2671: % \label{thm:xu-xa-just}
2672: Let $x$ be a notion of attack such that
2673: $x \supseteq$ \na{strongly attacks}. Then
2674: $J_{x/\na{u}} = J_{x/\na{d}} = J_{x/\na{a}}$.
2675: \end{theorem}
2676:
2677: \begin{proof}
2678: It is sufficient to show that $J_{x/\na{a}} \subseteq J_{x/\na{u}}$.
2679: Then by Theorem~\ref{thm:subset-just},
2680: $J_{x/\na{u}} \subseteq J_{x/\na{d}} \subseteq J_{x/\na{a}} = J_{x/\na{u}}$.\\[1ex]
2681: %
2682: % Informally, every $x$-attack $B$ to a $x/\na{a}$-justified argument $A$
2683: % is attacked by some
2684: % $x/\na{u}$-justified argument $C$ (by induction).
2685: % If $C$ is a rebut, but not an
2686: % undercut, then because $B$ strongly attacks $C$, and because
2687: % $x \supseteq \mbox{\it strongly attacks}$,
2688: % there must have been an argument defending $C$ by
2689: % undercutting $B$, thereby also defending $A$ against $B$.\\[1ex]
2690: %
2691: We prove by transfinite induction that for all ordinals $\alpha$:
2692: $J^\alpha_{x/\na{a}} \subseteq J^\alpha_{x/\na{u}}$.\\[2ex]
2693: %
2694: {\it Base case: } $\alpha=0$\\[2ex]
2695: %
2696: $J^\alpha_{x/\na{a}} = \emptyset = J^\alpha_{x/\na{u}}$.\\[2ex]
2697: %
2698: {\it Successor ordinal: } $\alpha \leadsto \alpha+1$\\[2ex]
2699: %
2700: Let $A \in J_{x/\na{a}}^{\alpha+1}$, and $(B,A) \in x$.
2701: By definition, there exists $C \in J_{x/\na{a}}^\alpha$ such that
2702: $C$ undercuts or rebuts $B$.
2703: By induction hypothesis, $C \in J_{x/\na{u}}^\alpha$.
2704:
2705: If $C$ undercuts $B$, then we are done.
2706: If, however, $C$ does not undercut $B$, then $C$ rebuts $B$,
2707: and so $B$ also rebuts $C$, i.e.\
2708: $B$ strongly attacks $C$.
2709: Because \na{strongly attacks} $\subseteq x$ and $C \in J_{x/\na{u}}^\alpha$,
2710: there exists
2711: $D \in J_{x/\na{u}}^{\alpha_0} \subseteq J_{x/\na{u}}^\alpha$ ($\alpha_0 < \alpha$)
2712: such that $D$ undercuts $B$. It follows that $A \in J_{x/\na{u}}^{\alpha+1}$.\\[2ex]
2713: %
2714: {\it Limit ordinal $\lambda$: }\\[2ex]
2715: %
2716: Assume $J_{x/\na{a}}^\alpha \subseteq J_{x/\na{u}}^\alpha$ for all $\alpha < \lambda$.
2717: Then
2718: $J_{x/\na{a}}^\lambda = \bigcup_{\alpha<\lambda}J_{x/\na{a}}^\alpha \subseteq
2719: \bigcup_{\alpha<\lambda}J_{x/\na{u}}^\alpha = J_{x/\na{u}}^\lambda$.
2720: %
2721: \end{proof}
2722:
2723:
2724: %\setcounter{theorem}{\ref{thm:sasu-sasa-just}}
2725: %\addtocounter{theorem}{-1}
2726: % This is Theorem 7.
2727: \setcounter{theorem}{6}
2728: \begin{theorem}
2729: % \label{thm:sasu-sasa-just}
2730: $J_{\na{sa}/\na{su}} = J_{\na{sa}/\na{sa}}$
2731: \end{theorem}
2732:
2733: \begin{proof}
2734: By Theorem~\ref{thm:subset-just},
2735: $J_{\na{sa}/\na{su}} \subseteq J_{\na{sa}/\na{sa}}$.
2736:
2737: We prove the inverse inclusion by showing that
2738: for all ordinals $\alpha$:
2739: $J_{\na{sa}/\na{sa}}^\alpha \subseteq J_{\na{sa}/\na{su}}^\alpha$,
2740: by transfinite induction on $\alpha$.\\[2ex]
2741: %
2742: {\it Base case: } $n=0$\\[2ex]
2743: %
2744: $J_{\na{sa}/\na{sa}}^0 = \emptyset = J_{\na{sa}/\na{su}}^0$\\[2ex]
2745: %
2746: {\it Successor ordinal: } $\alpha \leadsto \alpha+1$\\[2ex]
2747: %
2748: Let $A \in J_{\na{sa}/\na{sa}}^{\alpha+1}$, and $B$ strongly attacks $A$.
2749: By definition, there exists $C \in J_{\na{sa}/\na{sa}}^\alpha$ such that
2750: $C$ attacks $B$ and $B$ does not undercut $C$.
2751: By induction hypothesis, $C \in J_{\na{sa}/\na{su}}^\alpha$.
2752:
2753: If $C$ undercuts $B$, then we are done.
2754: If, however, $C$ rebuts $B$ and $C$ does not undercut $B$,
2755: then $B$ also rebuts $C$, i.e.\
2756: $B$ strongly attacks $C$, and so because
2757: $C \in J_{\na{sa}/\na{su}}^\alpha$
2758: there exists
2759: $D \in J_{\na{sa}/\na{su}}^{\alpha_0} \subseteq J_{\na{sa}/\na{su}}^\alpha$ ($\alpha_0 < \alpha$) such that
2760: $D$ strongly undercuts $B$.
2761: It follows that $A \in J_{\na{sa}/\na{su}}^{\alpha+1}(\emptyset)$.\\[2ex]
2762: %
2763: {\it Limit ordinal $\lambda$: }\\[2ex]
2764: %
2765: Assume $J_{\na{sa}/\na{sa}}^\alpha \subseteq J_{\na{sa}/\na{su}}^\alpha$ for all $\alpha < \lambda$.
2766: Then
2767: $J_{\na{sa}/\na{sa}}^\lambda = \bigcup_{\alpha<\lambda}J_{\na{sa}/\na{sa}}^\alpha \subseteq
2768: \bigcup_{\alpha<\lambda}J_{\na{sa}/\na{su}}^\alpha = J_{\na{sa}/\na{su}}^\lambda$.
2769: %
2770: \end{proof}
2771:
2772:
2773: %\setcounter{theorem}{\ref{thm:sua-sud-just}}
2774: %\addtocounter{theorem}{-1}
2775: % This is Theorem 8.
2776: \setcounter{theorem}{7}
2777: \begin{theorem}
2778: % \label{thm:sua-sud-just}
2779: $J_{\na{su}/\na{a}} = J_{\na{su}/\na{d}}$
2780: \end{theorem}
2781:
2782: \begin{proof}
2783: %
2784: By Theorem~\ref{thm:subset-just},
2785: $J_{\na{su}/\na{d}} \subseteq J_{\na{su}/\na{a}}$.\\[1ex]
2786: %
2787: % We now show the inverse inclusion. Informally, every strong
2788: % undercut $B$ to a $\na{su}/\na{a}$-justified argument $A$ is attacked by some
2789: % $\na{su}/\na{d}$-justified argument $C$ (by induction). If $C$ does not
2790: % defeat $A$, then there is some argument $D$ defending $C$ by
2791: % defeating $B$, thereby also defending $A$ against $B$.\\[1ex]
2792: %
2793: For the inverse inclusion, we show that
2794: for all ordinals $\alpha$:
2795: $J_{\na{su}/\na{a}}^\alpha \subseteq J_{\na{su}/\na{d}}^\alpha$,
2796: by transfinite induction on $\alpha$.\\[2ex]
2797: %
2798: {\it Base case: } $\alpha=0$\\[2ex]
2799: %
2800: $J_{\na{su}/\na{a}}^0 = \emptyset = J_{\na{su}/\na{d}}^0$\\[2ex]
2801: %
2802: {\it Successor ordinal: } $\alpha \leadsto \alpha+1$\\[2ex]
2803: %
2804: Let $A \in J_{\na{su}/\na{a}}^{\alpha+1}$, and $B$ strongly undercuts $A$.
2805: By definition, there exists $C \in J_{\na{su}/\na{a}}^\alpha$ such that
2806: $C$ undercuts or rebuts $B$.
2807: By induction hypothesis, $C \in J_{\na{su}/\na{d}}^\alpha$.
2808:
2809: If $C$ undercuts $B$, or $B$ does not undercut $C$, then we are done.
2810:
2811: Otherwise, $B$ strongly undercuts $C$, and so there exists
2812: $D \in J_{\na{su}/\na{d}}^{\alpha_0} \subseteq J_{\na{su}/\na{d}}^\alpha$ ($\alpha_0 < \alpha$)
2813: such that $D$ defeats $B$.
2814: It follows that $A \in J_{\na{su}/\na{d}}^{\alpha+1}$.\\[2ex]
2815: %
2816: {\it Limit ordinal $\lambda$: }\\[2ex]
2817: %
2818: Assume $J_{\na{su}/\na{a}}^\alpha \subseteq J_{\na{su}/\na{d}}^\alpha$ for all $\alpha < \lambda$.
2819: Then
2820: $$J_{\na{su}/\na{a}}^\lambda = \bigcup_{\alpha<\lambda}J_{\na{su}/\na{a}}^\alpha \subseteq
2821: \bigcup_{\alpha<\lambda}J_{\na{su}/\na{d}}^\alpha = J_{\na{su}/\na{d}}^\lambda$$
2822: %
2823: \end{proof}
2824:
2825:
2826:
2827: %\setcounter{theorem}{\ref{lemma:model-arg}}
2828: %\addtocounter{theorem}{-1}
2829: % This is Lemma 15.
2830: \setcounter{theorem}{14}
2831: \begin{lemma}
2832: % \label{lemma:model-arg}
2833: Let $I$ be a two-valued interpretation.
2834: \begin{enumerate}
2835: \item %\label{lemma:model-arg:u}
2836: $L \in \Gamma(I)$ iff $\exists$ argument $A$ with conclusion $L$
2837: such that $\assm(A) \subseteq I$.
2838: \item %\label{lemma:model-arg:a}
2839: $L \in \Gamma_s(I)$ iff $\exists$ argument $A$ with conclusion $L$
2840: such that $\assm(A) \subseteq I$ and
2841: $\neg\conc(A) \cap I = \emptyset$.
2842: \item %\label{lemma:model-arg:u-neg}
2843: $L \not\in \Gamma(I)$ iff $\forall$ arguments $A$ with conclusion $L$,
2844: $\assm(A) \cap I \not= \emptyset$.
2845: \item %\label{lemma:model-arg:a-neg}
2846: $L \not\in \Gamma_s(I)$ iff $\forall$ arguments $A$ with
2847: conclusion $L$, $\assm(A) \cap I \not= \emptyset$
2848: or $\neg\conc(A) \cap I \not= \emptyset$.
2849: \end{enumerate}
2850: \end{lemma}
2851: %
2852: \begin{proof}\hspace{0em}
2853: \begin{enumerate}
2854: \item ``Only If''-direction:
2855: Induction on the length $n$ of the derivation of $L \in \Gamma(I)$.\\[0.5ex]
2856: %
2857: \textit{Base case}: $n = 1$:\\
2858: Then there exists a rule $L \gets not~L_1,\ldots,not~L_n$ in $P$ s.t.\
2859: $L_1,\ldots,L_n \not\in I$,
2860: and $[L \gets not~L_1,\ldots,not~L_n]$ is an argument for $L$
2861: whose assumptions are contained in $I$.\\[0.5ex]
2862: %
2863: \textit{Induction step}: $n \leadsto n+1$:\\
2864: Let $L \in \Gamma^{n+1}(I)$. Then there exists a rule
2865: $r = L \gets L_1,\ldots,L_n,not~L'_1,\ldots,L'_m$ in $P$ s.t.\
2866: $L_i \in \Gamma^n(I)$, and $L'_i \not\in I$.
2867: By induction hypothesis, there exists arguments $A_1,\ldots,A_n$ for
2868: $L_1,\ldots,L_n$ with $\assm(A_i) \subseteq I$.
2869: Then $A = [r] \cdot A_1 \cdots A_n$ is an argument for $L$
2870: such that $\assm(A) \subseteq I$.\\[1ex]
2871: %
2872: ``If'' direction: Induction on the length of the argument.\\[0.5ex]
2873: \textit{Base case}: $n = 1$:\\
2874: Then $A = [L \gets not~L_1,\ldots,not~L_n]$, and
2875: $L_1,\ldots,L_n \not\in I$. Then $L \gets \in \frac{P}{I}$,
2876: and $L \in \Gamma^1(I)$.\\[0.5ex]
2877: %
2878: \textit{Induction step}: $n \leadsto n+1$:\\
2879: Let $A = [L \gets L_1,\ldots,L_n,not~L'_1,\ldots,not~L'_m;r_2,\ldots,r_n]$
2880: be an argument s.t.\ $\assm(A) \subseteq I$.
2881: $A$ contains subarguments $A_1,\ldots,A_n$ for $L_1,\ldots,L_n$,
2882: with $\assm(A_i) \subseteq I$.
2883: Because $L'_1,\ldots,L'_m \not\in I$, then
2884: $L \gets L_1,\ldots,L_n \in \frac{P}{I}$.
2885: By induction hypothesis, $L_i \in \Gamma(I)$.
2886: so also $L \in \Gamma(I)$.
2887: \item ``Only If''-direction:
2888: Induction on the length $n$ of the derivation of $L \in \Gamma_s(I)$.\\[0.5ex]
2889: %
2890: \textit{Base case}: $n = 1$:\\
2891: Then there exists a rule $L \gets not~L_1,\ldots,not~L_n$ in $P$ s.t.\
2892: $\neg L,L_1,\ldots,L_n \not\in I$,
2893: and $[L \gets not~L_1,\ldots,not~L_n]$ is an argument for $L$
2894: whose assumptions are contained in $I$, and $\neg L \not\in I$.\\[0.5ex]
2895: %
2896: \textit{Induction step}: $n \leadsto n+1$:\\
2897: Let $L \in \Gamma^{n+1}(I)$. Then there exists a rule
2898: $r = L \gets L_1,\ldots,L_n,not~L'_1,\ldots,L'm$ in $P$ s.t.\
2899: $L_i \in \Gamma^n(I)$, $L'_i \not\in I$, and $\neg L \not\in I$.
2900: By induction hypothesis, there exists arguments $A_1,\ldots,A_n$ for
2901: $L_1,\ldots,L_n$ with $\assm(A_i) \subseteq I$ and
2902: $\neg \conc(A_i) \cap I = \emptyset$.
2903: Then $A = [r] \cdot A_1 \cdots A_n$ is an argument for $L$
2904: such that $\assm(A) \subseteq I$, and $\neg \conc(A) \cap I = \emptyset$.\\[1ex]
2905: %
2906: ``If'' direction: Induction on the length of the argument.\\[0.5ex]
2907: \textit{Base case}: $n = 1$:\\
2908: Then $A = [L \gets not~L_1,\ldots,not~L_n]$, and
2909: $\neg L,L_1,\ldots,L_n \not\in I$. Then $L \gets \in \frac{P_s}{I}$,
2910: and $L \in \Gamma^1(I)$.\\[0.5ex]
2911: %
2912: \textit{Induction step}: $n \leadsto n+1$:\\
2913: Let $A = [L \gets L_1,\ldots,L_n,not~L'_1,\ldots,not~L'_m;r_2,\ldots,r_n]$
2914: be an argument s.t.\ $\assm(A) \subseteq I$, and
2915: $\neg \conc(A) \cap I = \emptyset$.
2916: $A$ contains subarguments $A_1,\ldots,A_n$ for $L_1,\ldots,L_n$,
2917: with $\assm(A_i) \subseteq I$, and $\neg \conc(A_i) \cap I = \emptyset$.
2918: Because $L'_1,\ldots,L'_m \not\in I$, and $\neg L \not\in I$, then
2919: $L \gets L_1,\ldots,L_n \in \frac{P}{I}$.
2920: By induction hypothesis, $L_i \in \Gamma(I)$,
2921: so also $L \in \Gamma(I)$.
2922: \item and 4. follow immediately from \ref{lemma:model-arg:u}.\ and
2923: \ref{lemma:model-arg:a}.\ because $I$ is two-valued.
2924: \end{enumerate}
2925: \end{proof}
2926:
2927: %\setcounter{theorem}{\ref{thm:sound-complete}}
2928: %\addtocounter{theorem}{-1}
2929: % This is Theorem 19.
2930: \setcounter{theorem}{18}
2931: \begin{theorem}
2932: An argument $A$ is $x/y$-justified iff there exists a $x/y$-dialogue
2933: tree with $A$ as its root, and won by the proponent.
2934: \end{theorem}
2935:
2936: \begin{proof}
2937: ``If''-direction.
2938: We show by transfinite induction: If $A \in J^{\alpha}_{x/y}$, then
2939: there exists a winning $x/y$-dialogue tree of height $\leq \alpha$
2940: for $A$.\\[1ex]
2941: %
2942: {\em Base case $\alpha=0$:}\\
2943: Then there exists no argument $B$ such that $(B,A) \in x$,
2944: and so $A$ is a winning $x/y$-dialogue tree for $A$ of height $0$.\\[0.5ex]
2945: %
2946: {\em Successor ordinal $\alpha+1$:}\\
2947: If $A \in J_{x/y}^{\alpha+1}$, then for any $B_i$ such that $(B_i,A) \in x$
2948: there exists a $C_i \in J_{x/y}^{\alpha}$ such that $(C_i,B_i) \in y$.
2949: By induction hypothesis, there exist winning $x/y$-dialogue trees
2950: for the $C_i$. Furthermore, if any of the $C_i$ contains a move
2951: $m = (P, A)$, then it also contains a winning subtree for $A$ rooted
2952: at $m$ and we are done. Otherwise, we have a winning tree rooted at $A$,
2953: with children $B_i$, whose children are the winning trees for $C_i$.\\[0.5ex]
2954: %
2955: {\em Limit ordinal $\lambda$:}\\
2956: If $A \in J_{x/y}^{\lambda}$, then there exists an $\alpha < \lambda$
2957: such that $A \in J_{x/y}^{\alpha}$; by induction hypothesis,
2958: there exists a winning $x/y$-dialogue tree of height $\alpha$ for $A$.\\[1ex]
2959: %
2960: ``Only-if''-direction.
2961: We prove by transfinite induction:
2962: If there exists a winning tree of height $\alpha$ for $A$,
2963: then $A \in J_{x/y}^{\alpha}$.
2964:
2965: Note that by definition, the height of a dialogue tree is
2966: either $0$ or a successor ordinal $\alpha+1$. So we prove the base
2967: case $0$, and for the induction step, we assume that the induction
2968: hypothesis holds for all $\beta < \alpha+1$.\\[1ex]
2969: %
2970: {\em Base case $\alpha=0$:}\\
2971: Then there are no arguments $B$ such that $(B,A) \in x$, and so
2972: $A \in J_{x/y}^0$.\\[0.5ex]
2973: %
2974: {\em Successor ordinal $\alpha+1$:}\\
2975: Let $T$ be a tree with root $A$, whose children are $B_i$,
2976: and the children of $B_i$ are winning trees rooted at $C_i$.
2977: By induction hypothesis, $C_i \in J_{x/y}^{\alpha}$.
2978: Because the $B_i$ are all those arguments such that $(B_i,A) \in x$,
2979: then $A$ is defended against each $B_i$ by $C_i$, and so
2980: $A \in J_{x/y}^{\alpha+1}$.
2981: \end{proof}
2982:
2983: \end{document}
2984:
2985:
2986: