1: \documentclass{article}
2:
3: \usepackage{nmr}
4:
5: \usepackage{latexsym}
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: \newenvironment{proof}[1][Proof.]{\noindent\textbf{#1} }{\hfill$\Box$}
18:
19: \newcommand{\herbrand}{{\cal H}}
20: \newcommand{\assm}{{\it assm}}
21: \newcommand{\conc}{{\it conc}}
22: \newcommand{\mycenter}[1]{\hspace*{\fill}#1\hspace*{\fill}}
23:
24: \author{Ralf Schweimeier and Michael Schroeder\\
25: Department of Computing\\
26: City University, London, UK\\
27: \{ralf,msch\}@soi.city.ac.uk}
28: \title{Well-Founded Argumentation Semantics for Extended Logic Programming}
29:
30: \begin{document}
31:
32: \maketitle
33:
34: \begin{abstract}
35: This paper defines an argumentation semantics for extended logic
36: programming and shows its equivalence to the well-founded semantics
37: with explicit negation. We set up a general framework in which we
38: extensively compare this semantics to other argumentation semantics,
39: including those of Dung, and Prakken and Sartor. We present a
40: general dialectical proof theory for these argumentation semantics.
41: \end{abstract}
42:
43: \section{Introduction}
44:
45: Argumentation has attracted much interest in the area of AI. On the
46: one hand, argumentation is an important way of human interaction and
47: reasoning, and is therefore of interest for research into intelligent
48: systems. Application areas include automated negotiation via
49: argumentation~\cite{PSJ98:AgentsArguing,KSE98:Argument,Sch99:Argument}
50: and legal reasoning~\cite{PS97:Argument}. On the other hand,
51: argumentation provides a formal model for various assumption based (or
52: non-monotonic, or default) reasoning
53: formalisms~\cite{BDKT97:Argument,CML00:LogicalModelsOfArgument}. In
54: particular, various argumentation based semantics have been proposed
55: for logic programming with default
56: negation~\cite{BDKT97:Argument,Dun95:Argument}.
57:
58: Argumentation semantics are elegant since they can be captured in an
59: abstract
60: framework~\cite{Dun95:Argument,BDKT97:Argument,%
61: Vre97:AbstractArgumentationSystems,JV99:RobustSemantics},
62: for which an elegant theory of attack, defence, acceptability, and
63: other notions can be developed, without recourse to the concrete
64: instance of the reasoning formalism at hand. This framework can then
65: be instantiated to various assumption based reasoning formalisms.
66: Similarly, a dialectical proof theory, based on dialogue trees,
67: can be defined for an abstract
68: argumentation framework, and then applied to any instance of such a
69: framework~\cite{Dun95:Argument,JV99:DialecticSemantics}.
70:
71: In general, an argument $A$ is a proof which may use a set of
72: defeasible assumptions. Another argument $B$ may have a conclusion
73: which contradicts the assumptions or the conclusions of $A$, and
74: thereby $B$ {\em attacks} $A$. There are two fundamental notions of such
75: attacks: undercut and rebut~\cite{PS97:Argument} or equivalently {\em
76: ground-attack} and {\em reductio-ad-absurdum attack}
77: \cite{Dun93:ArgumentExplicit}. We will use the terminology of
78: undercuts and rebuts. Both attacks differ in that an undercut attacks a
79: premise of an argument, while a rebut attacks a
80: conclusion.
81:
82: Given a logic program we can define an argumentation semantics by
83: iteratively collecting those arguments which are acceptable to a
84: proponent, i.e. they can be defended against all opponent attacks. In
85: fact, such a notion of acceptability can be defined in a number of
86: ways depending on which attacks we allow the proponent and opponent to use.
87:
88: Normal logic programs do not have negative conclusions, which means
89: that we cannot use rebuts. Thus both opponents can only launch
90: undercuts on each other's assumptions.
91: Various argumentation semantics have been defined for normal logic programs
92: \cite{BDKT97:Argument,Dun95:Argument,KT99:ComputingArgumentation},
93: some of which are equivalent to
94: existing semantics such as the stable model semantics~\cite{GL88:StableModels}
95: or the well-founded semantics~\cite{GRS91:WFS}.
96:
97: Extended logic programs
98: \cite{GL90:ClassicalNegation,AP96:WFSX,wag94a}, on the other hand,
99: introduce explicit negation, which states that a literal is explicitly
100: false. As a result, both undercuts and rebuts are possible forms of attack;
101: there are further variations depending on whether any kind of counter-attack
102: is admitted. A variety of argumentation semantics arise if one allows
103: one notion of attack as defence for the proponent, and another as attack
104: for the opponent.
105: Various argumentation semantics have been proposed for extended logic programs
106: \cite{Dun93:ArgumentExplicit,PS97:Argument}.
107: Dung has shown that a certain argumentation semantics is equivalent to
108: the answer set semantics~\cite{GL90:ClassicalNegation}, a generalisation
109: of the stable model semantics~\cite{GL88:StableModels}.
110: To our knowledge, no argumentation semantics has yet been found equivalent
111: to the well-founded semantics for extended logic programs,
112: WFSX~\cite{PA92:WFSX,AP96:WFSX}.
113:
114: This paper makes the following contributions: we define a least
115: fixpoint argumentation semantics for extended logic programs, and show
116: its equivalence to the well-founded semantics with explicit
117: negation~\cite{PA92:WFSX,AP96:WFSX,ADP95:LPsystem}. In order to
118: relate this semantics to other argumentation semantics, we set up a
119: general framework to classify notions of justified arguments, and use
120: it to compare our argumentation semantics to those of
121: Dung~\cite{Dun93:ArgumentExplicit} and Prakken and
122: Sartor~\cite{PS97:Argument} among others. We develop a general
123: dialectical proof theory for the notions of justified arguments we
124: introduce.
125:
126:
127: The paper is organised as follows: First we define arguments and
128: notions of attack and acceptability. Then we set up a framework for
129: classifying different least fixpoint argumentation semantics,
130: based on different notions of attack. In Section~\ref{sec:wfsx}, we recall
131: the definition of WFSX, and in Section~\ref{sec:wfsxarg}, we prove
132: the equivalence of an argumentation semantics and WFSX.
133: A general dialectical proof theory for arguments is presented in
134: Section~\ref{sec:proof-theory}, and its soundness and completeness is
135: proven.
136:
137: \section{Extended Logic Programming and Argumentation}
138: \label{sec:elp}
139:
140: We summarise the definitions of arguments for extended logic programs,
141: and define various notions of attack between arguments.
142:
143: \subsection{Arguments}
144: \label{subsec:arguments}
145:
146:
147: \begin{definition}
148: An {\em objective literal} is an atom $A$ or its explicit negation
149: $\neg A$. We define $\neg \neg L = L$.
150: A {\em default literal} is of the form $not~L$ where $L$
151: is an objective literal. A {\em literal} is either an objective or a
152: default literal. \\
153: An {\em extended logic program} is a (possibly infinite) set of rules of
154: the form \vspace{-1ex}
155: $$L_0 \gets L_1,\dots,L_m, not~L_{m+1},\dots, not~L_{m+n}\vspace{-1ex}$$
156: where $m, n \ge 0$, and each $L_i$ is an objective literal
157: $(0\leq i \leq m+n)$. \\
158: For such a rule $r$, we call $L_0$ the {\em head} of the rule,
159: $head(r)$, and $L_1,\ldots,not~L_{m+n}$ the {\em body} of the rule,
160: $body(r)$.
161: \end{definition}
162:
163: Our definition of an argument for an extended logic program is based
164: on~\cite{PS97:Argument}.
165: Essentially, an argument is a partial proof, resting on a number of
166: {\em assumptions}, i.e.~a set of default literals.%
167: \footnote{In~\cite{BDKT97:Argument,Dun93:ArgumentExplicit}, an argument
168: {\em is} a set of assumptions; the two approaches are equivalent in
169: that there is an argument with a conclusion $L$ iff there is a set
170: of assumptions from which $L$ can be inferred. See the discussion
171: in~\cite{PS97:Argument}.}
172:
173: Note that we do not consider priorities of arguments, as used e.g.\
174: in~\cite{PS97:Argument,Vre97:AbstractArgumentationSystems}.
175:
176: \begin{definition}
177: Let $P$ be an extended logic program. \\
178: An {\em argument} for $P$ is a finite sequence
179: $A=[r_1,\dots r_n]$ of rules $r_i \in P$ such that
180: for every $1\le i \le n$, for every objective literal $L_j$ in
181: the body of $r_i$ there is a $k>i$ such that $head(r_k) = L_j$. \\
182: A {\em subargument} of $A$ is a subsequence of $A$ which is an argument.
183: The head of a rule in $A$ is called a {\em conclusion} of $A$,
184: and a default literal $not~L$ in the body of a rule of $A$ is called an
185: {\em assumption} of $A$.
186: We write $\assm(A)$ for the set of assumptions and $\conc(A)$ for the
187: set of conclusions of an argument $A$. \\
188: %
189: An argument $A$ with a conclusion $L$ is a {\em minimal argument for $L$}
190: if there is no subargument of $A$ with conclusion $L$.
191: An argument is {\em minimal} if it minimal for some literal $L$.
192: Given an extended logic program $P$, we denote the set of minimal arguments
193: for $P$ by $\mathit{Args}_P$.
194:
195: \end{definition}
196:
197: The restriction to minimal arguments is not essential, but convenient,
198: since it rules out arguments constructed from several unrelated
199: arguments. Generally, one is interested in the conclusions of an
200: argument, and wants to avoid having rules in an argument which do not
201: contribute to the desired conclusion.
202:
203: \subsection{Notions of Attack}
204: \label{subsec:attack}
205:
206: There are two fundamental notions of attack: {\em undercut},
207: which invalidates an assumption of an argument, and
208: {\em rebut}, which contradicts a conclusion of an
209: argument~\cite{Dun93:ArgumentExplicit,PS97:Argument}.
210: From these, we may define further
211: notions of attack, by allowing either of the two fundamental kinds of
212: attack, and considering whether any kind of counter-attack is allowed
213: or not. We will now formally define these notions of attacks.
214:
215: \begin{definition}
216: \label{def:notionsofattack}
217: Let $A_1$ and $A_2$ be arguments.
218: \begin{enumerate}
219:
220: \item
221: $A_1$ {\em undercuts} $A_2$ if there is an objective literal
222: $L$ such that $L$ is a conclusion of $A_1$ and $not~L$ is an
223: assumption of $A_2$.
224:
225: \item
226: $A_1$ {\em rebuts} $A_2$ if there is an objective literal $L$
227: such that $L$ is a conclusion of $A_1$ and $\neg L$ is a
228: conclusion of $A_2$.
229:
230: \item
231: $A_1$ {\em attacks} $A_2$ if $A_1$ undercuts or rebuts $A_2$.
232:
233: \item
234: $A_1$ {\em defeats} $A_2$ if
235: $A_1$ undercuts $A_2$, or
236: ($A_1$ rebuts $A_2$ and $A_2$ does not undercut $A_1$).
237:
238: \item
239: $A_1$ {\em strongly attacks} $A_2$ if $A_1$ attacks $A_2$ and
240: $A_2$ does not undercut $A_1$.
241:
242: \item
243: $A_1$ {\em strongly undercuts} $A_2$ if $A_1$ undercuts $A_2$
244: and $A_2$ does not undercut~$A_1$.
245: \end{enumerate}
246: \end{definition}
247:
248: The notions of \emph{undercut} and \emph{rebut}, and hence \emph{attack} are
249: fundamental for extended logic
250: programs~\cite{Dun93:ArgumentExplicit,PS97:Argument}. The notion of
251: \emph{defeat} is used in~\cite{PS97:Argument}, along with a notion of
252: \emph{strict defeat}, i.e.\ a defeat that is not counter-defeated.
253: For arguments without priorities, rebuts are symmetrical, and
254: therefore strict defeat coincides with strict
255: undercut, i.e.\ an undercut that is not counter-undercut.
256: Similarly, strict attack coincides with strict undercut.
257: For this reason, we use the term {\em strong undercut} instead of
258: {\em strict undercut}, and similarly define {\em strong attack} to be
259: an attack which is not counter-undercut.
260: %
261: We will use the following abbreviations for these notions of attack.
262: \textit{r} for rebuts,
263: \textit{u} for undercuts,
264: \textit{a} for attacks,
265: \textit{d} for defeats,
266: \textit{sa} for strongly attacks, and
267: \textit{su} for strongly undercuts.
268:
269: These notions of attack define for any extended logic program a binary
270: relation on the set of arguments of that program.
271:
272: \begin{definition}
273: A {\em notion of attack} is a function $x$ which assigns to each
274: extended logic program $P$ a binary relation $x_P$ on the set of
275: arguments of $P$, i.e.\ $x_P \subseteq \mathit{Args}_P^2$. Notions
276: of attack can be partially ordered by defining
277: $x \subseteq y \mbox{ ~iff~ } \forall P: x_P \subseteq y_P$
278: \end{definition}
279:
280: \begin{definition}
281: Let $x$ be a notion of attack. Then
282: the {\em inverse} of $x$, denoted by $x^{-1}$, is defined as
283: $x^{-1}_P = \{ (B,A) ~|~ (A,B) \in x_P \}$.
284: \end{definition}
285:
286: In this relational notation,
287: Definition~\ref{def:notionsofattack} can be rewritten as
288: $a = u \cup r$, $d = u \cup (r - u^{-1})$,
289: $sa = (u \cup r) - u^{-1}$, and $su = u - u^{-1}$.
290: Using the set-theoretic laws $A-B \subseteq A \subseteq A \cup C$ and
291: $(A \cup B) - C = (A - C) \cup (B - C)$ (for all sets $A$, $B$, and $C$),
292: it is easy to see that the notions of attack of
293: Definition~\ref{def:notionsofattack} are partially ordered according
294: to the following Hasse diagram.
295: %
296: \noindent
297: $$\hspace{-1.5cm}\xymatrixnocompile@C=-5em@R=1em{%@R=.2cm{
298: & \parbox{3.5cm}{\begin{center}\textit{attacks} $= a = u \cup r$\end{center}\vspace{-1ex}} \ar@{-}[d] \\
299: & \parbox{4cm}{\vspace{-1ex}\begin{center}\textit{defeats} $=$ $d = u \cup (r - u^{-1})$\end{center}\vspace{-1ex}}
300: \ar@{-}[dl] \ar@{-}[dr] \\
301: \hspace{1cm}\parbox{3.5cm}{\vspace{-1ex}\begin{center}\textit{undercuts} $= u$\end{center}\vspace{-1ex}} \ar@{-}[dr] &&
302: \hspace{-2cm}\parbox{5.5cm}{\vspace{-1ex}\begin{center}\textit{strongly attacks} $=$ $sa = (u \cup r) - u^{-1}$\end{center}\vspace{-1ex}}
303: \ar@{-}[dl] \\
304: & \parbox{5.5cm}{\hspace{-2cm}\vspace{-1ex}\begin{center}\textit{strongly undercuts} $= su = u - u^{-1}$\end{center}} \\
305: }$$
306:
307: This diagram contains the notions of attack used
308: in~\cite{Dun93:ArgumentExplicit,PS97:Argument}, plus
309: \textit{strongly attacks} which seemed a natural intermediate
310: notion between \textit{strongly undercuts} and \textit{defeats}.
311: We have not included \textit{rebuts}, because in the absence of
312: priorities, \textit{rebuts} is somewhat weaker than \textit{undercuts},
313: because it is symmetric: a rebut is always counter-rebutted,
314: while the same does not hold for \textit{undercuts}.
315:
316:
317:
318: \subsection{Acceptability and Justified Arguments}
319: \label{subsec:acceptable}
320:
321: Given the above notions of attack, we define acceptability of an
322: argument. Basically, an argument is acceptable if it can be defended
323: against any attack. Depending on which particular notion of attack we
324: use as defence and which for the opponent's attacks, we obtain a host
325: of acceptability notions.
326:
327: Acceptability forms the basis for our argumentation semantics,
328: which is defined as the least fixpoint of a function, which collects
329: all acceptable arguments. The {\em least} fixpoint is of particular
330: interest \cite{PS97:Argument,Dun93:ArgumentExplicit}, because it
331: provides a canonical fixpoint semantics and it can be constructed
332: inductively.
333:
334:
335: \begin{definition}
336: Let $x$ and $y$ be notions of attack. Let $A$ be an argument, and
337: $S$ a set of arguments. Then $A$ is {\em $x/y$-acceptable wrt.\ $S$}
338: if for every argument $B$ such that $(B,A) \in x$ there exists an
339: argument $C \in S$ such that $(C,B) \in y$.
340: \end{definition}
341:
342: Based on the notion of acceptability, we can then define a fixpoint
343: semantics for arguments.
344:
345: \begin{definition}
346: Let $x$ and $y$ be notions of attack, and $P$ an extended logic
347: program. The operator
348: $F_{P, x/y}:{\cal P}(\mathit{Args}_P) \rightarrow {\cal P}(\mathit{Args}_P)$
349: is defined as
350: $$F_{P, x/y}(S) = \{ A ~|~ A \mbox{ is $x/y$-acceptable wrt.\ $S$} \}$$
351: We denote the least fixpoint of $F_{P, x/y}$ by $J_{P, x/y}$.
352: If the program $P$ is clear from the context, we omit the subscript $P$.
353: An argument $A$ is called $x/y$-justified if $A \in J_{x/y}$;
354: an argument is called $x/y$-overruled if it is attacked by an
355: $x/y$-justified argument; and an argument is called $x/y$-defensible
356: if it is neither $x/y$-justified nor $x/y$-overruled.
357: \end{definition}
358:
359: For any program $P$, the least fixpoint exists by the Knaster-Tarski fixpoint
360: theorem~\cite{Tar55:Fixpoint,Bir67:LatticeTheory}, because $F_{P,x/y}$
361: is monotone. It can be constructed by transfinite induction as
362: follows:
363: %
364: $$\begin{array}{llll}
365: J^0_{x/y} & \!\!\!=\!\!\! & \emptyset \\
366: J^{\alpha+1}_{x/y} & \!\!\!=\!\!\! & F_{P, x/y}(J^\alpha_{x/y}) &
367: \mbox{for $\alpha \! + \! 1$ a successor ordinal} \\
368: J^\lambda_{x/y} & \!\!\!=\!\!\! & \bigcup_{\alpha < \lambda}J^\alpha_{x/y} &
369: \mbox{for $\lambda$ a limit ordinal} \\
370: \end{array}$$
371: %
372: Then there exists a least ordinal $\lambda_0$ such that
373: $F_{x/y}(J^{\lambda_0}_{x/y}) = J^{\lambda_0}_{x/y} = J_{x/y}$.
374:
375:
376:
377: \section{Relationships of Notions of Justifiability}
378: \label{sec:relationship}
379:
380: This section is devoted to an analysis of the relationship
381: between the different notions of justifiability, leading to
382: a hierarchy of notions of justifiability illustrated in
383: Figure~\ref{fig:hierarchy}.
384:
385:
386: First of all, it is easy to see that the least fixpoint increases if
387: we weaken the attacks, or strengthen the defence.
388:
389: \begin{proposition}
390: \label{prop:subset-just}
391: Let $x' \subseteq x$, $y \subseteq y'$ be notions of attack, then
392: $J_{x/y} \subseteq J_{x'/y'}$.
393: \end{proposition}
394:
395: Theorem~\ref{thm:strong-nonstrong} states that it does not make a
396: difference if we allow only the strong version of the defence. This is
397: because an argument need not defend itself on its own, but it may rely
398: on other arguments to defend it.
399:
400: We only give a formal proof for the first theorem; the proofs for the
401: other theorems are similar, and we provide an intuitive informal
402: explanation instead.
403:
404: \begin{theorem}
405: \label{thm:strong-nonstrong}
406: Let $x$ and $y$ be
407: notions of attack such that \mbox{$x \supseteq \mathit{undercuts}$},
408: and let $sy = y - \mathit{undercuts}^{-1}$. Then
409: $J_{x/y} = J_{x/sy}$.
410: \end{theorem}
411:
412: \begin{proof}
413: Informally, every $x$-attack $B$ to an $x/y$-justified argument $A$ is
414: $y$-defended by some $x/sy$-justified argument $C$ (by induction).
415: Now if $C$ was {\em not} a $sy$-attack, then it is undercut by $B$,
416: and because $x \supseteq \mathit{undercuts}$ and
417: $C$ is justified, there exists a {\em strong} defence
418: for $C$ against $B$, which is also a defence of the original
419: argument $A$ against $C$.\\[2ex]
420: %
421: The formal proof is by transfinite induction.
422: By Proposition~\ref{prop:subset-just}, we have $J_{x/sy} \subseteq J_{x/y}$.
423: We prove the inverse inclusion by showing that
424: for all ordinals $\alpha$:
425: $J_{x/y}^\alpha \subseteq J_{x/sy}^\alpha$,
426: by transfinite induction on $\alpha$.\\[1ex]
427: %
428: {\it Base case} $\alpha=0$:
429: %
430: $J_{x/y} = \emptyset = J_{x/sy}$.\\[1ex]
431: %
432: {\it Successor ordinal } $\alpha \leadsto \alpha+1$:
433: %
434: Let $A \in J_{x/y}^{\alpha+1}$, and $(B,A) \in x$.
435: By definition, there exists $C \in J_{x/y}^\alpha$ such that
436: $(C,B) \in y$. By induction hypothesis, $C \in J_{x/sy}^\alpha$.
437:
438: If $B$ does not undercut $C$, then we are done.
439: If, however, $B$ undercuts $C$, then because
440: $C \in J_{x/sy}^\alpha$, and $\mathit{undercuts} \subseteq x$,
441: there exists
442: $D \in J_{x/sy}^{\alpha_0}(\emptyset) (\alpha_0 < \alpha)$ such that
443: $(D,B) \in sy$. It follows that $A \in J_{x/sy}^{\alpha+1}$.\\[1ex]
444: %
445: {\it Limit ordinal $\lambda$: }
446: %
447: Assume $J_{x/y}^\alpha \subseteq J_{x/sy}^\alpha$ for all $\alpha < \lambda$.
448: Then
449: $J_{x/y}^\lambda = \bigcup_{\alpha<\lambda}J_{x/y}^\alpha \subseteq
450: \bigcup_{\alpha<\lambda}J_{x/sy}^\alpha = J_{x/sy}^\lambda$
451: %
452: \end{proof}
453:
454: In particular, the previous Theorem states that undercut and strong
455: undercut are equivalent as a defence, as are attack and strong attack.
456: This may be useful in an implementation, where we may use the stronger
457: notion of defence without changing the semantics, thereby decreasing
458: the number of arguments to be checked.
459: The following Corollary shows that because defeat lies between attack
460: and strong attack, it is equivalent to both as a defence.
461:
462: \begin{corollary}
463: \label{cor:xa-xsa-just}
464: Let $x$ be a notion of attack such that
465: \mbox{$x \supseteq \mathit{undercuts}$}.
466: Then $J_{x/a} = J_{x/d} = J_{x/sa}$.
467: \end{corollary}
468:
469: \begin{proof}
470: With Proposition~\ref{prop:subset-just} and
471: Theorem~\ref{thm:strong-nonstrong}, we have
472: $J_{x/a} \subseteq J_{x/d} \subseteq J_{x/sa} = J_{x/a}$.
473: \end{proof}
474:
475:
476:
477:
478: \begin{theorem}
479: \label{thm:xu-xa-just}
480: Let $x$ be a notion of attack such that
481: \mbox{$x \supseteq \mbox{\it strongly attacks}$}. Then
482: $J_{x/u} = J_{x/d} = J_{x/a}$.
483: \end{theorem}
484:
485:
486: \begin{proof}
487: Every $x$-attack $B$ to a $x/a$-justified argument $a$
488: is attacked by some
489: $x/u$-justified argument $C$ (by induction).
490: If $C$ is a rebut, but not an
491: undercut, then because $B$ strongly attacks $C$, and because
492: $x \supseteq \mbox{\it strongly attacks}$,
493: there must have been an argument defending $C$ by
494: undercutting $B$, thereby also defending $A$ against $B$.
495:
496: The statement for \textit{defeats} follows in a similar way to
497: Corollary~\ref{cor:xa-xsa-just}.
498:
499: \end{proof}
500:
501:
502: \begin{theorem}
503: \label{thm:sasu-sasa-just}
504: $J_{sa/su} = J_{sa/sa}$
505: \end{theorem}
506:
507:
508:
509: The proof is similar to Theorem~\ref{thm:xu-xa-just}.
510:
511:
512:
513:
514:
515:
516:
517:
518: \begin{theorem}
519: \label{thm:sua-sud-just}
520: $J_{su/a} = J_{su/d}$
521: \end{theorem}
522:
523:
524: \begin{proof}
525: %
526: Every strong undercut $B$ to a $su/a$-justified argument $A$ is attacked
527: by some $su/d$-justified argument $C$ (by induction).
528: If $C$ does not defeat $A$, then there is some argument $D$
529: defending $C$ by defeating $B$, thereby also defending $A$ against $B$.
530: \end{proof}
531:
532:
533: We will now present some example programs which distinguish
534: various notions of justifiability.
535:
536: \begin{figure}
537: \footnotesize
538: \begin{center}
539: \begin{tabular}{l|l|l}
540: $\begin{array}{rcl}
541: \multicolumn{3}{c}{P_1 =} \\
542: p & \gets & not~q \\
543: q & \gets & not~p \\
544: \\
545: \\
546: \\
547: \end{array}$
548: &
549: $\begin{array}{rcl}
550: \multicolumn{3}{c}{P_2 =} \\
551: p & \gets & not~q \\
552: q & \gets & not~p \\
553: \neg p \\
554: \\
555: \\
556: \end{array}$
557: &
558: $\begin{array}{rcl}
559: \multicolumn{3}{c}{P_3 =}\\
560: p & \gets & not~q \\
561: q & \gets & not~r \\
562: r & \gets & not~s \\
563: s & \gets & not~p \\
564: \neg p \\
565: \end{array}$
566: \\\hline
567: $\begin{array}{rcl}
568: \multicolumn{3}{c}{P_4 =} \\
569: p & \gets & not~q \\
570: q & \gets & not~p \\
571: r & \gets & not~p \\
572: \\
573: \end{array}$
574: &
575: $\begin{array}{rcl}
576: \multicolumn{3}{c}{P_5 =} \\
577: p & \gets & not~\neg p \\
578: \neg p \\
579: \\
580: \\
581: \end{array}$
582: &
583: $\begin{array}{rcl}
584: \multicolumn{3}{c}{P_6 =} \\
585: \neg p & \gets & not~q \\
586: \neg q & \gets & not~p \\
587: p \\
588: q \\
589: \end{array}$
590: \end{tabular}
591: \end{center}
592: %
593: \caption{Examples}
594: \label{fig:ex}
595: \end{figure}
596: %
597: %
598: \begin{example}\hspace{0cm}
599: \label{ex:loop}
600: Consider $P_1$ in Figure \ref{fig:ex}.
601: %
602: For any notion of attack $x$, we have
603: $J_{su/x} = J_{sa/x} = \{ [p \gets not~q], [q \gets not~p] \},$
604: because there is no strong undercut or strong attack to any
605: of the arguments.
606: %
607: However,
608: $J_{a/x} = J_{d/x} = J_{u/x} = \emptyset,$
609: because every argument is undercut (and therefore defeated and
610: attacked).
611: \end{example}
612:
613: \begin{example}\hspace{0em}
614: \label{ex:coherence}
615: Consider $P_2$ in Figure \ref{fig:ex}.
616: %
617: Let $x$ be a notion of attack. Then
618: $J_{d/x} = J_{a/x} = \emptyset,$
619: because every argument is defeated (hence attacked).
620: $J_{sa/su} = J_{sa/sa} = \{ [q \gets not~p] \},$
621: because $[q \gets not~p]$ is the only argument which is not
622: strongly attacked, but it does not strongly attack any other
623: argument.
624: $J_{u/su} = J_{u/u} = \{ [\neg p] \},$
625: because there is no undercut to $[\neg p]$, but
626: $[\neg p]$ does not undercut any other argument.
627: $J_{u/a} = \{ [\neg p], [q \gets not~p] \},$
628: because there is no undercut to $[\neg p]$, and the undercut
629: $[p \gets not~p]$ to $[q \gets not~p]$ is attacked by
630: $[\neg p]$. We also have
631: $J_{sa/u} = \{ [\neg p], [q \gets not~p] \},$
632: because $[q \gets not~p]$ is not strongly attacked, and the strong
633: attack $[p \gets not~q]$ on $[\neg p]$ is undercut by
634: $[q \gets not~p]$.
635: \end{example}
636:
637: \begin{example}\hspace{0cm}
638: \label{ex:coherence-big}
639: Consider $P_3$ in Figure \ref{fig:ex}.
640: %
641: Let $x$ be a notion of attack.
642: Then $J_{sa/x} = \emptyset,$
643: because every argument is strongly attacked.
644:
645: $J_{su/u} = J_{su/su} = \{ [\neg p] \},$
646: because all arguments except $[\neg p]$ are
647: strongly undercut, but $[\neg p]$ does not undercut any argument.
648: And
649: $J_{u/a} = J_{su/sa} = J_{su/a} =
650: \{ [\neg p], [q \gets not~r], [s \gets not~p] \}.$
651: \end{example}
652:
653: \begin{example}\hspace{0cm}
654: \label{ex:loop-plus}
655: Consider $P_4$ in Figure \ref{fig:ex}.
656: %
657: Let $x$ be a notion of attack. Then
658: $J_{u/x} = J_{d/x} = J_{a/x} = \emptyset,$
659: because every argument is undercut.
660: $J_{su/su} = J_{su/sa} = J_{sa/su} = J_{sa/sa} =
661: \{ [p \gets not~q], [q \gets not~p] \}$
662: In this case, the strong attacks are precisely the strong undercuts;
663: The argument $[r \gets not~p]$ is not justified, because the
664: strong undercut $[p \gets not~q]$ is undercut, but not strongly
665: undercut, by $[q \gets not~p]$.
666: $J_{su/u} = J_{su/a} = J_{sa/u} = J_{sa/a} =
667: \{ [p \gets not~q], [q \gets not~p], [r \gets not~p] \}$
668: Again, undercuts and attacks, and strong undercuts and strong
669: attacks, coincide; but now $[r \gets not~p]$ is justified,
670: because non-strong undercuts are allowed as defence.
671: \end{example}
672:
673: \begin{example}\hspace{0cm}
674: \label{ex:defeat}
675: Consider $P_5$ in Figure \ref{fig:ex}.
676: %
677: Then $J_{a/x} = \emptyset$, because both arguments attack each
678: other, while $J_{d/x} = \{[\neg p]\}$, because $[\neg p]$ defeats
679: $[p \gets not~\neg p]$, but not vice versa.
680: \end{example}
681:
682: \begin{example}\hspace{0cm}
683: \label{ex:loop-neg}
684: Consider $P_6$ in Figure \ref{fig:ex}.
685: %
686: Let $x$ be a notion of attack. Then
687: $J_{sa/x} = J_{d/x} = J_{a/x} = \emptyset,$
688: because every argument is strongly attacked (hence defeated and attacked),
689: while
690: $J_{u/x} = J_{su/x} = \{ [p], [q] \}.$
691: \end{example}
692:
693:
694:
695:
696:
697: \begin{theorem}
698: \label{thm:hierarchy}
699: The notions of justifiability are ordered (by set inclusion)
700: according to the Hasse diagram in Figure~\ref{fig:hierarchy}.
701: \end{theorem}
702:
703:
704: \begin{figure}[htbp]
705: \begin{center}\footnotesize
706: $\xymatrix@C=-5em@R=3ex{
707: && su/a = su/d \\
708: & su/u \ar@{-}[ru] && su/sa \ar@{-}[lu] \\
709: % \parbox{6em}{\begin{center}sa/u = sa/d = sa/a\end{center}}
710: sa/u = sa/d = sa/a
711: \ar@{-}[ru] &&
712: su/su \ar@{-}[lu] \ar@{-}[ru] &&
713: % \parbox{5em}{\begin{center}u/a = u/d = u/sa\end{center}} \ar@{-}[lu] \\
714: u/a = u/d = u/sa \ar@{-}[lu] \\
715: & sa/su = sa/sa \ar@{-}[lu] \ar@{-}[ru] &&
716: u/su = u/u \ar@{-}[lu] \ar@{-}[ru] \\
717: % && \parbox{6em}{\begin{center}d/su = d/u = d/a = d/d = d/sa\end{center}}
718: && d/su = d/u = d/a = d/d = d/sa
719: \ar@{-}[lu] \ar@{-}[ru] \\
720: % && \parbox{6em}{\begin{center}a/su = a/u = a/a = a/d = a/sa\end{center}}
721: && a/su = a/u = a/a = a/d = a/sa
722: \ar@{-}[u] \\
723: }$
724: \caption{Hierarchy of Notions of Justifiability}
725: \label{fig:hierarchy}
726: \end{center}
727: \end{figure}
728: %
729: By definition, Dung's grounded argumentation semantics~%
730: \cite{Dun93:ArgumentExplicit} is exactly $a/u$-justifiability,
731: while Prakken and Sartor's semantics~\cite{PS97:Argument},
732: if we disregard priorities, amounts to $d/su$-justifiability.
733: As corollaries to Theorem~\ref{thm:hierarchy}, we obtain relationships of
734: these semantics to the other notions of justifiability.
735:
736: \begin{corollary}
737: Let $J_{Dung}$ be the set of justified arguments according to
738: Dung's grounded argumentation semantics~\cite{Dun93:ArgumentExplicit}.
739: Then $J_{Dung}=J_{a/su}=J_{a/u}=J_{a/a}=J_{a/d}=J_{a/sa}$ and
740: $J_{Dung} \subseteq J_{x/y}$ for all notions of attack $x$ and $y$.
741: \end{corollary}
742:
743: \begin{corollary}
744: Let $J_{PS}$ be the set of justified arguments according to
745: Prakken and Sartor's argumentation semantics~\cite{PS97:Argument},
746: where all arguments have the same priority.
747: Then $J_{PS}=J_{d/su}=J_{d/u}=J_{d/a}=J_{d/d}=J_{d/sa}$,
748: $J_{PS} \subseteq J_{x/y}$ for all notions of attack $x \not= a$ and $y$,
749: and $J_{PS} \supseteq J_{a/y}$ for all notions of attack $y$.
750: \end{corollary}
751:
752:
753:
754:
755: \begin{remark}\hspace{0cm}
756: 1. The notions of $a/x$-, $d/x$- and $sa/x$-justifiability are very
757: sceptical in that a {\em fact} $p$ may not be justified, if there
758: is a rule $\neg p \gets B$ (where $not~p \not\in B$) that is not
759: $x$-attacked. On the other hand this is useful in terms of
760: avoiding inconsistency.
761:
762: \noindent
763: 2. $sx/y$-justifiability is very credulous,
764: because it does not take into account non-strong attacks, so e.g.\
765: the program $\{ p \gets not~q, q \gets not~p \}$ has the justified
766: arguments $[p \gets not~q]$ and $[q \gets not~p]$.
767:
768: \end{remark}
769:
770: \begin{remark}
771: One might ask whether any of the semantics in Figure~\ref{fig:hierarchy}
772: are equivalent for {\em non-contradictory} programs, i.e.\ programs for
773: which there is no literal $L$ such that there exist justified
774: arguments for both $L$ and $\neg L$.
775: The answer to this question is no: all the examples above distinguishing
776: different notions of justifiability involve only non-contradictory
777: programs.
778:
779: In particular, even for non-contradictory programs,
780: Dung's and Prakken and Sartor's semantics differ, and
781: both differ from $u/a$-justifiability, which will be shown equivalent to
782: the well-founded semantics WFSX~\cite{PA92:WFSX,AP96:WFSX} in the
783: following section.
784: \end{remark}
785:
786: \section{Well-founded semantics}
787: \label{sec:wfsx}
788:
789: We recollect the definition of the well-founded semantics for
790: extended logic programs, WFSX. We use the definition of~\cite{ADP95:LPsystem},
791: because it is closer to our definition of argumentation semantics than
792: the original definition of~\cite{PA92:WFSX,AP96:WFSX}.
793:
794: \begin{definition}
795: The set of all objective literals of a program $P$ is
796: called the {\em Herbrand base} of $P$ and denoted by $\herbrand(P)$.
797: A {\em pseudo-interpretation} of a program $P$ is a set
798: $T \cup not~F$ where $T$ and $F$ are subsets of $\herbrand(P)$.
799: An {\em interpretation} is a pseudo-interpretation where the sets $T$ and $F$
800: are disjoint. An interpretation is called {\em two-valued} if
801: $T \cup F = \herbrand(P)$.
802: \end{definition}
803:
804:
805: \begin{definition}
806: Let $P$ be an extended logic program, $I$ an interpretation,
807: and let $P'$ (resp.~$I'$) be obtained from $P$ (resp.~$I$) by
808: replacing every literal $\neg A$ by a new atom, say $\neg\_A$.
809: The GL-transformation $\frac{P'}{I'}$ is the program obtained
810: from $P'$ by removing all rules containing a default literal
811: $not~A$ such that $A \in I'$, and then removing all remaining
812: default literals from $P'$, obtaining a definite program $P''$.
813: Let $J$ be the least model of $P''$. $\Gamma_P I$ is obtained from
814: $J$ by replacing the introduced atoms $\neg\_A$ by $\neg A$.
815: \end{definition}
816:
817: \begin{definition}
818: The {\em semi-normal} version of a program $P$ is the program $P_s$
819: obtained from $P$ by replacing every rule $L \gets Body$ in $P$
820: by the rule $L \gets not~\neg L, Body$.
821: \end{definition}
822:
823: If the program $P$ is clear from the context, we write $\Gamma I$ for
824: $\Gamma_P I$ and $\Gamma_s I$ for $\Gamma_{P_s} I$.
825:
826: \begin{definition}
827: Let $P$ be a program whose least fixpoint of $\Gamma \Gamma_s$ is $T$.
828: Then the {\em paraconsistent well-founded model of $P$} is
829: the pseudo-interpretation
830: $WFM_p(P) = T \cup not~(\herbrand(P) - \Gamma_s T)$.
831: If $WFM_p(P)$ is an interpretation, then
832: $P$ is called {\em non-contradictory},
833: and $WFM_p(P)$ is the {\em well-founded model of $P$},
834: denoted by $WFM(P)$.
835: \end{definition}
836: %
837: The paraconsistent well-founded model can by defined iteratively by
838: the transfinite sequence $\{I_\alpha\}$:
839:
840: \begin{tabular}{llll}
841: $I_0$ & = & $\emptyset$ \\
842: $I_{\alpha+1}$ & = & $\Gamma \Gamma_s I_\alpha$ &
843: for successor ordinal $\alpha+1$ \\
844: $I_\lambda$ & = & $\bigcup_{\alpha < \lambda} I_\alpha$ &
845: for limit ordinal $\lambda$ \\
846: \end{tabular}
847:
848: There exists a smallest ordinal $\lambda_0$ such that $I_{\lambda_0}$
849: is the least fixpoint of $\Gamma \Gamma_s$, and
850: $WFM_p(P) = I_{\lambda_0} \cup not~(\herbrand(P) - \Gamma_s I_{\lambda_0})$.
851:
852:
853: \section{Equivalence of argumentation semantics and WFSX}
854: \label{sec:wfsxarg}
855:
856: In this section, we will show that the argumentation semantics $J_{u/a}$ and
857: the well-founded model coincide.
858: That is, the conclusions of justified arguments
859: are exactly the objective literals which are true in the well-founded model;
860: and those objective literals all of whose arguments are overruled are exactly
861: the literals which are false in the well-founded model.
862: The result holds also for contradictory programs under the
863: {\em paraconsistent} well-founded semantics.
864: This is important, because it shows that contradictions in the
865: argumentation semantics are precisely the contradictions under
866: the well-founded semantics, and allows the application of
867: contradiction removal (or avoidance) methods to the argumentation semantics.
868: Because for non-contradictory programs,
869: the well-founded semantics coincides with the paraconsistent
870: well-founded semantics~\cite{ADP95:LPsystem},
871: we obtain as a corollary that argumentation semantics and well-founded
872: semantics coincide for non-contradictory programs.
873:
874: In order to compare the argumentation semantics with the well-founded
875: semantics, we define the set of literals which are a
876: consequence of the argumentation semantics.
877:
878: \begin{definition}
879: $A(P) = T~\cup~not~F$, where \\
880: $T = \{ L ~|$ there is a justified argument for $L \}$ and \\
881: $F = \{ L ~|$ all arguments for $L$ are overruled $\}$.
882: \end{definition}
883:
884:
885: The following Proposition shows a precise connection between arguments and
886: consequences of a program $\frac{P}{I}$.
887: \begin{proposition}
888: \label{prop:model-arg}
889: Let $I$ be a two-valued interpretation.
890: \begin{enumerate}
891: \item \label{prop:model-arg:u}
892: $L \in \Gamma(I)$ iff $\exists$ argument $A$ with conclusion $L$
893: such that $\assm(A) \subseteq I$.
894: \item \label{prop:model-arg:a}
895: $L \in \Gamma_s(I)$ iff $\exists$ argument $A$ with conclusion $L$
896: such that $\assm(A) \subseteq I$ and
897: $\neg\conc(A) \cap I = \emptyset$.
898: \item \label{prop:model-arg:u-neg}
899: $L \not\in \Gamma(I)$ iff $\forall$ arguments $A$ with conclusion $L$,
900: $\assm(A) \cap I \not= \emptyset$.
901: \item \label{prop:model-arg:a-neg}
902: $L \not\in \Gamma_s(I)$ iff $\forall$ arguments $A$ with
903: conclusion $L$, $\assm(A) \cap I \not= \emptyset$
904: or $\neg\conc(A) \cap I \not= \emptyset$.
905: \end{enumerate}
906: \end{proposition}
907: %
908: \begin{proof}
909: See Appendix.
910: \end{proof}
911:
912:
913:
914: \begin{theorem}
915: \label{thm:wfsxarg}
916: Let $P$ be an extended logic program.
917: Then $WFM_p(P) = A(P)$.
918: \end{theorem}
919:
920: \begin{proof}\raggedright
921: First, note that $A$ undercuts $B$ iff
922: $\exists~L$ s.t.\ $not~L \in \assm(A)$ and $L \in \conc(B)$;
923: and $A$ rebuts $B$ iff $\exists~L \in \conc(A) \cap \neg\conc(B)$.\\[2ex]
924: %
925: We show that for all ordinals $\alpha$, $I_\alpha = A_\alpha$,
926: by transfinite induction on $\alpha$.\\[0.5ex]
927: %
928: \textit{Base case $\alpha=0$:}
929: $I_\alpha = \emptyset = A_\alpha$
930: \\[0.5ex]
931: %
932: \textit{Successor ordinal $\alpha \leadsto \alpha+1$}:\\[0.5ex]
933: %
934: $L \in I_{\alpha+1}$ \\
935: \mycenter{iff (Def.\ of $I_{\alpha+1}$)} \\
936: $L \in \Gamma \Gamma_s I_\alpha$ \\
937: \mycenter{iff (Prop.~\ref{prop:model-arg}(\ref{prop:model-arg:u}))} \\
938: $\exists$~argument $A$ for $L$ such that
939: $\assm(A) \subseteq \Gamma_s I_\alpha$ \\
940: \mycenter{iff (Def.\ of $\subseteq$, and $\Gamma_s I_\alpha$
941: is two-valued)} \\
942: $\exists$~argument $A$ for $L$ such that
943: $\forall~not~L \in \assm(A), L \not\in \Gamma_s I_\alpha$ \\
944: \mycenter{iff (Prop.~\ref{prop:model-arg}(\ref{prop:model-arg:a-neg}))} \\
945: $\exists$~argument $A$ for $L$ such that $\forall~not~L \in \assm(A)$,
946: for any argument $B$ for $L$,
947: (~$\exists~not~L' \in \assm(B) ~s.t.\ L' \in I_\alpha$
948: or $\exists~L'' \in \conc(B) ~s.t.\ \neg L'' \in I_\alpha$ ) \\
949: \mycenter{iff (Induction hypothesis)} \\
950: $\exists$~argument $A$ for $L$ such that $\forall~not~L \in \assm(A)$,
951: for any argument $B$ for $L$,
952: (~$\exists~not~L' \in \assm(B) ~s.t.\ \exists$
953: argument $C \in J_\alpha$ for $L'$,
954: or $\exists~L'' \in \conc(B) ~s.t.\ \exists$~
955: argument $C \in J_\alpha$ for $\neg L''$) \\
956: \mycenter{iff (Def.\ of undercut and rebut)} \\
957: $\exists$~argument $A$ for $L$ such that for any undercut $B$ to $A$,
958: (~$\exists$~argument $C \in J_\alpha$ s.t.\
959: $C$ undercuts $B$,
960: or $\exists$~argument $C \in J_\alpha$ s.t.\
961: $C$ rebuts $B$) \\
962: \mycenter{iff} \\
963: $\exists$~argument $A$ for $L$ such that for any undercut $B$ to $A$,
964: $\exists$~argument $C \in J_\alpha$ s.t.\ $C$ attacks $B$ \\
965: \mycenter{iff (Def.\ of $J_{\alpha+1}$)} \\
966: $\exists$~argument $A \in J_{\alpha+1}$ for $L$ \\
967: \mycenter{iff (Def.\ of $A_{\alpha+1}$)} \\
968: $L \in A_{\alpha+1}$\\[0.5ex]
969: %
970: \textit{Limit ordinal $\lambda$:}\\
971: $I_\lambda = \bigcup_{\alpha < \lambda} I_\alpha$ and
972: $A_\lambda = \bigcup_{\alpha < \lambda} A_\alpha$,
973: so by induction hypothesis ($I_\alpha = A_\alpha$ for all $\alpha < \lambda$),
974: $I_\lambda = A_\lambda$.\\[2ex]
975: %
976: Now, we show that a literal $not~L$ is in the well-founded semantics
977: iff every argument for $L$ is overruled.\\[0.5ex]
978: %
979: $not~L \in WFM_p(P)$ \\
980: \mycenter{iff (Def.\ of $WFM_p(P)$)} \\
981: $L \not\in \Gamma_s I$ \\
982: \mycenter{iff (Prop.~\ref{prop:model-arg}(\ref{prop:model-arg:a-neg}))} \\
983: for all arguments $A$ for $L$,
984: (~$\exists~not~L' \in \assm(A) ~s.t.\ L' \in I$, or
985: $\exists~L'' \in \conc(A) ~s.t.\ \neg L'' \in I$ ) \\
986: \mycenter{iff (I=A)} \\
987: for all arguments $A$ for $L$,
988: (~$\exists~not~L' \in \assm(A) ~s.t.\
989: \exists$~argument $B \in J$ for $L'$, or
990: $\exists~L'' \in \conc(A) ~s.t.\
991: \exists$~argument $B \in J$ for $\neg L''$ ) \\
992: \mycenter{iff (Def.\ of undercut and rebut)} \\
993: for all arguments $A$ for $L$,
994: (~$\exists$~argument $B \in J$ s.t.\ $B$ undercuts $A$, or
995: $\exists$~argument $B \in J$ s.t.\ $B$ rebuts $A$ ) \\
996: \mycenter{iff} \\
997: every argument for $L$ is attacked by a justified argument in $J$ \\
998: \mycenter{iff (Def.\ of overruled)} \\
999: every argument for $L$ is overruled \\
1000: \mycenter{iff (Def.\ of $A(P)$)} \\
1001: $not~L \in A(P)$
1002: \end{proof}
1003:
1004: \begin{corollary}
1005: Let $P$ be a non-contradictory program. Then $WFM(P) = A(P)$.
1006: \end{corollary}
1007:
1008: \begin{remark}
1009: In a similar way, one can show that the $\Gamma$ operator corresponds
1010: to undercuts, while the $\Gamma_s$ operator corresponds to attacks, and so
1011: the least fixpoints of $\Gamma\Gamma$, $\Gamma_s\Gamma$, and
1012: $\Gamma_s\Gamma_s$ correspond to $J_{u/u}$, $J_{a/u}$, and $J_{a/a}$,
1013: respectively.
1014: In~\cite{ADP95:LPsystem}, the least fixpoints of these operators are
1015: shown to be ordered as
1016: $lfp(\Gamma_s\Gamma) \subseteq lfp(\Gamma_s\Gamma_s) \subseteq
1017: lfp(\Gamma\Gamma_s)$, and
1018: $lfp(\Gamma_s\Gamma) \subseteq lfp(\Gamma\Gamma) \subseteq
1019: lfp(\Gamma\Gamma_s)$.
1020: Because $J_{a/u} = J_{a/a} \subseteq J_{u/u} \subseteq J_{u/a}$ by
1021: Theorem~\ref{thm:hierarchy}, we can strengthen this statement
1022: to $lfp(\Gamma_s\Gamma) = lfp(\Gamma_s\Gamma_s) \subseteq
1023: lfp(\Gamma\Gamma) \subseteq lfp(\Gamma\Gamma_s)$.
1024: \end{remark}
1025:
1026:
1027: \section{Proof theory}
1028: \label{sec:proof-theory}
1029:
1030: One of the benefits of relating the argumentation semantics $J_{u/a}$ to
1031: WFSX is the existence of an efficient top-down proof procedure for
1032: WFSX~\cite{ADP95:LPsystem},
1033: which we can use to compute justified arguments in $J_{u/a}$.
1034: On the other hand, {\em dialectical} proof theories, based on dialogue trees,
1035: have been defined for a variety of argumentation semantics
1036: \cite{PS97:Argument,JV99:DialecticSemantics,KT99:ComputingArgumentation}.
1037: In this section, we present a sound and complete dialectical proof theory for
1038: the least fixpoint argumentation semantics $J_{x/y}$ for any
1039: notions of attack $x$ and $y$. Our presentation closely
1040: follows~\cite{PS97:Argument}.
1041: As a further consequence, we obtain an equivalence of the proof theory
1042: for WFSX and the dialectical proof theory for arguments.
1043:
1044: \begin{definition}
1045: An {\em $x/y$-dialogue} is a finite nonempty sequence of
1046: moves $move_i = (\mathit{Player}_i,Arg_i) (i > 0)$, such that
1047: \begin{enumerate}
1048: \item $\mathit{Player}_i = P$ iff $i$ is odd; and
1049: $\mathit{Player}_i = O$ iff $i$ is even.
1050: \item If $\mathit{Player}_i = \mathit{Player}_j$ and $i \not= j$,
1051: then $Arg_i \not= Arg_j$.
1052: \item If $\mathit{Player}_i = P$ and $i > 1$, then
1053: $Arg_i$ is a minimal argument such that $(Arg_i,Arg_{i-1}) \in y$.
1054: \item If $\mathit{Player}_i = O$, then $(Arg_i,Arg_{i-1}) \in x$.
1055: \end{enumerate}
1056: \end{definition}
1057:
1058: The first condition states that the players $P$ (Proponent) and
1059: $O$ (Opponent) take turns, and $P$ starts.
1060: The second condition prevents the proponent from repeating a move.
1061: The third and fourth conditions state that both players have to
1062: attack the other player's last move, where the opponent is allowed
1063: to use the notion of attack $x$, while the proponent may use $y$ to
1064: defend its arguments.
1065:
1066: \begin{definition}
1067: An {\em $x/y$-dialogue tree} is a tree of moves such that
1068: every branch is a dialogue, and for all moves $move_i = (P, Arg_i)$,
1069: the children of $move_i$ are all those moves $(O,Arg_j)$ such that
1070: $(Arg_j,Arg_i) \in x$.
1071: \end{definition}
1072:
1073: \begin{definition}
1074: A player {\em wins an $x/y$-dialogue} iff the other player cannot move.
1075: A player {\em wins an $x/y$-dialogue tree} iff it wins all branches
1076: of the tree. An $x/y$-dialogue tree which is won by the proponent
1077: is called a {\em winning $x/y$-dialogue tree}.
1078: An argument $A$ is {\em provably $x/y$-justified} iff there exists a
1079: $x/y$-tree with $A$ as its root, and won by the proponent.
1080: A literal $L$ is a {\em provably justified conclusion} iff
1081: it is a conclusion of a provably $x/y$-justified argument.
1082: The {\em height} of a dialogue tree is $0$ if it consists only of
1083: the root, and otherwise $height(t) = \bigcup height(t_i)+1$ where
1084: $t_i$ are the trees rooted at the grandchildren of $t$.
1085: \end{definition}
1086:
1087: We show that the proof theory of $x/y$-dialogue trees is sound and
1088: complete for any notions of attack $x$ and $y$.
1089:
1090: \begin{theorem}
1091: \label{thm:sound-complete}
1092: An argument is provably $x/y$-justified iff it is $x/y$-justified.
1093: \end{theorem}
1094:
1095: \begin{proof}
1096: ``If''-direction.
1097: We show by transfinite induction: If $A \in J^{\alpha}_{x/y}$, then
1098: there exists a winning $x/y$-dialogue tree of height $< \alpha$
1099: for $A$.\\[1ex]
1100: %
1101: {\em Base case $\alpha=0$:}\\
1102: Then there exists no argument $B$ such that $(B,A) \in x$,
1103: and so $A$ is a winning $x/y$-dialogue tree for $A$ of height $0$.\\[0.5ex]
1104: %
1105: {\em Successor ordinal $\alpha+1$:}\\
1106: If $A \in J_{x/y}^{\alpha+1}$, then for any $B_i$ such that $(B_i,A) \in x$
1107: there exists a $C_i \in J_{x/y}^{\alpha}$ such that $(C_i,B_i) \in y$.
1108: By induction hypothesis, there exist winning $x/y$-dialogue trees
1109: for the $C_i$. Thus, we have a winning tree rooted for $A$,
1110: with children $B_i$, whose children are the winning trees for $C_i$.\\[0.5ex]
1111: %
1112: {\em Limit ordinal $\lambda$:}\\
1113: If $A \in J_{x/y}^{\lambda}$, then there exists an $\alpha < \lambda$
1114: such that $A \in J_{x/y}^{\alpha}$; by induction hypothesis,
1115: there exists a winning $x/y$-dialogue tree of height $\alpha$ for $A$.\\[1ex]
1116: %
1117: ``Only-if''-direction.
1118: We prove by transfinite induction:
1119: If there exists a winning tree of height $\alpha$ for $A$,
1120: then $A \in J_{x/y}^{\alpha}$.\\[1ex]
1121: %
1122: {\em Base case $\alpha=0$:}\\
1123: Then there are no arguments $B$ such that $(B,A) \in x$, and so
1124: $A \in J_{x/y}^0$.\\[0.5ex]
1125: %
1126: {\em Successor ordinal $\alpha+1$:}\\
1127: Let $T$ be a tree with root $A$, whose children are $B_i$,
1128: and the children of $B_i$ are winning trees rooted at $C_i$.
1129: By induction hypothesis, $C_i \in J_{x/y}^{\alpha}$.
1130: Because the $B_i$ are all those arguments such that $(B_i,A) \in x$,
1131: then $A$ is defended against each $B_i$ by $C_i$, and so
1132: $A \in J_{x/y}^{\alpha+1}$.
1133: \end{proof}
1134:
1135: As a corollary, we can relate the proof theory of WFSX and the
1136: $u/a$-proof theory.
1137:
1138: \begin{corollary}
1139: $L$ is a provably $u/a$-justified conclusion iff
1140: there exists a successful T-tree~\cite{AP96:WFSX} for $L$.
1141: \end{corollary}
1142:
1143: \begin{proof}
1144: Follows from the fact that $u/a$-dialogue trees are sound and complete
1145: for $u/a$-justifiability (Theorem~\ref{thm:sound-complete}),
1146: that $T$-trees are sound and complete for WFSX~\cite{AP96:WFSX},
1147: and that $u/a$-justifiability and WFSX are equivalent
1148: (Theorem~\ref{thm:wfsxarg}).
1149: \end{proof}
1150:
1151: \section{Conclusion and Further Work}
1152: \label{sec:conclusion}
1153:
1154: We have identified various notions of attack for extended logic
1155: programs. Based on these notions of attack, we defined notions of
1156: acceptability and least fixpoint semantics. These fixpoint semantics
1157: were related by establishing a lattice of justified arguments, based
1158: on set inclusion. We identified an argumentation semantics $J_{u/a}$
1159: equal to the well-founded semantics for logic programs with explicit
1160: negation, $WFSX$~\cite{AP96:WFSX}, and established that $J_{Dung}
1161: \subseteq J_{PS} \subseteq J_{u/a} = WFSX$, where $J_{Dung}$ and
1162: $J_{PS}$ are the least fixpoint argumentation semantics of
1163: Dung~\cite{Dun93:ArgumentExplicit} and Prakken and
1164: Sartor~\cite{PS97:Argument}. We have defined a dialectical proof
1165: theory for argumentation. For all notions of justified arguments
1166: introduced, we prove that the proof theory is sound and complete
1167: wrt. the corresponding fixpoint argumentation semantics. In
1168: particular, we showthe equivalence of successful T-trees
1169: ~\cite{AP96:WFSX} in WFSX to provably $u/a$ justified arguments.
1170:
1171: Finally, it remains to be seen whether a variation in the notion of
1172: attack yields interesting variations of alternative argumentation
1173: semantics for extended logic programs such as preferred extensions or
1174: stable extensions~\cite{Dun93:ArgumentExplicit}. It is also an open
1175: question how the hierarchy changes when priorities are added as
1176: defined in \cite{PS97:Argument, Vre97:AbstractArgumentationSystems}.
1177:
1178:
1179:
1180: \noindent {\bf Acknowledgement}
1181: This work has been supported by EPSRC grant GRM88433.
1182:
1183: \bibliographystyle{plain}
1184: %\bibliography{nmr}
1185:
1186: \begin{thebibliography}{10}
1187:
1188: \bibitem{ADP95:LPsystem}
1189: J.~J. Alferes, C.~V. Dam\'asio, and L.~M. Pereira.
1190: \newblock A logic programming system for non-monotonic reasoning.
1191: \newblock {\em Journal of Automated Reasoning}, 14(1):93--147, 1995.
1192:
1193: \bibitem{AP96:WFSX}
1194: J.~J. Alferes and L.~M. Pereira.
1195: \newblock {\em Reasoning with Logic Programming}.
1196: \newblock (LNAI 1111), Springer-Verlag, 1996.
1197:
1198: \bibitem{Bir67:LatticeTheory}
1199: Garrett Birkhoff.
1200: \newblock {\em Lattice Theory}.
1201: \newblock American Mathematical Society, 3rd edition, 1967.
1202:
1203: \bibitem{BDKT97:Argument}
1204: A.~Bondarenko, P.M. Dung, R.A. Kowalski, and F.~Toni.
1205: \newblock An abstract, argumentation-theoretic approach to default reasoning.
1206: \newblock {\em Artificial Intelligence}, 93(1-2):63--101, 1997.
1207:
1208: \bibitem{CML00:LogicalModelsOfArgument}
1209: Carlos~Iv\'an Ches{\~n}evar, Ana~Gabriela Maguitman, and Ronald~Prescott Loui.
1210: \newblock Logical models of argument.
1211: \newblock {\em ACM Computing Surveys}, 32(4):337--383, December 2000.
1212:
1213: \bibitem{Dun93:ArgumentExplicit}
1214: P.~M. Dung.
1215: \newblock An argumentation semantics for logic programming with explicit
1216: negation.
1217: \newblock In {\em Proc. of the 10th International Conference on Logic
1218: Programming}, pages 616--630. MIT Press, 1993.
1219:
1220: \bibitem{Dun95:Argument}
1221: P.~M. Dung.
1222: \newblock On the acceptability of arguments and its fundamental role in
1223: nonmonotonic reasoning, logic programming and n-person games.
1224: \newblock {\em Artificial Intelligence}, 77(2):321--357, 1995.
1225:
1226: \bibitem{GRS91:WFS}
1227: Allen~Van Gelder, Kenneth~A. Ross, and John~S. Schlipf.
1228: \newblock The well-founded semantics for general logic programs.
1229: \newblock {\em Journal of the ACM}, 38(3):620--650, July 1991.
1230:
1231: \bibitem{GL88:StableModels}
1232: M.~Gelfond and V.~Lifschitz.
1233: \newblock The stable model semantics for logic programming.
1234: \newblock In R.~A. Kowalski and K.~A. Bowen, editors, {\em 5th International
1235: Conference on Logic Programming}, pages 1070--1080. MIT Press, 1988.
1236:
1237: \bibitem{GL90:ClassicalNegation}
1238: M.~Gelfond and V.~Lifschitz.
1239: \newblock Logic programs with classical negation.
1240: \newblock In {\em Proc. of ICLP90}, pages 579--597. MIT Press, 1990.
1241:
1242: \bibitem{JV99:DialecticSemantics}
1243: H.~Jakobovits and D.~Vermeir.
1244: \newblock Dialectic semantics for argumentation frameworks.
1245: \newblock In {\em Proceedings of the Seventh International Conference on
1246: Artificial Intelligence and Law (ICAIL '99)}, pages 53--62, 1999.
1247:
1248: \bibitem{JV99:RobustSemantics}
1249: H.~Jakobovits and D.~Vermeir.
1250: \newblock Robust semantics for argumentation frameworks.
1251: \newblock {\em Journal of Logic and Computation}, 9(2):215--261, 1999.
1252:
1253: \bibitem{KT99:ComputingArgumentation}
1254: A.C. Kakas and F.~Toni.
1255: \newblock Computing argumentation in logic programming.
1256: \newblock {\em Journal of Logic and Computation}, 9:515--562, 1999.
1257:
1258: \bibitem{KSE98:Argument}
1259: S.~Kraus, K.~Sycara, and A.~Evenchik.
1260: \newblock Reaching agreements through argumentation: a logical model and
1261: implementation.
1262: \newblock {\em Artificial Intelligence}, 104(1-2):1--69, 1998.
1263:
1264: \bibitem{PSJ98:AgentsArguing}
1265: Simon Parsons, Carlos Sierra, and Nick Jennings.
1266: \newblock Agents that reason and negotiate by arguing.
1267: \newblock {\em Journal of Logic and Computation}, 8(3):261--292, 1998.
1268:
1269: \bibitem{PA92:WFSX}
1270: Luis~Moniz Pereira and Jos\'e~J\'ulio Alferes.
1271: \newblock Well founded semantics for logic programs with explicit negation.
1272: \newblock In {\em B. Neumann (Ed.), European Conference on Artificial
1273: Intelligence}, pages 102--106. Wiley, 1992.
1274:
1275: \bibitem{PS97:Argument}
1276: Henry Prakken and Giovanni Sartor.
1277: \newblock Argument-based extended logic programming with defeasible priorities.
1278: \newblock {\em Journal of Applied Non-Classical Logics}, 7(1), 1997.
1279:
1280: \bibitem{Sch99:Argument}
1281: Michael Schroeder.
1282: \newblock An efficient argumentation framework for negotiating autonomous
1283: agents.
1284: \newblock In {\em Proceedings of Modelling Autonomous Agents in a Multi-Agent
1285: World MAAMAW99}. LNAI1647, Springer-Verlag, 1999.
1286:
1287: \bibitem{Tar55:Fixpoint}
1288: A.~Tarski.
1289: \newblock A lattice-theoretical fixpoint theorem and its applications.
1290: \newblock {\em Pacific Journal of Mathematics}, 5:285--309, 1955.
1291:
1292: \bibitem{Vre97:AbstractArgumentationSystems}
1293: Gerard A.~W. Vreeswijk.
1294: \newblock Abstract argumentation systems.
1295: \newblock {\em Artificial Intelligence}, 90(1--2):225--279, 1997.
1296:
1297: \bibitem{wag94a}
1298: Gerd Wagner.
1299: \newblock {\em Vivid Logic -- Knowledge-Based Reasoning with Two Kinds of
1300: Negation}, volume LNAI 764.
1301: \newblock Springer--Verlag, 1994.
1302:
1303: \end{thebibliography}
1304:
1305: \newpage
1306: \appendix
1307:
1308: \section*{Appendix}
1309:
1310: \begin{proof}[Proof of Proposition~\ref{prop:model-arg}]\hspace{0em}
1311: \raggedright
1312: \begin{enumerate}
1313: \item ``If''-direction:
1314: Induction on the length $n$ of the derivation of $L \in \Gamma(I)$.\\[0.5ex]
1315: %
1316: \textit{Base case}: $n = 1$:\\
1317: Then there exists a rule $L \gets not~L_1,\ldots,not~L_n$ in $P$ s.t.\
1318: $L_1,\ldots,L_n \not\in I$,
1319: and $[L \gets not~L_1,\ldots,not~L_n]$ is an argument for $L$
1320: whose assumptions are contained in $I$.\\[0.5ex]
1321: %
1322: \textit{Induction step}: $n \leadsto n+1$:\\
1323: Let $L \in \Gamma^{n+1}(I)$. Then there exists a rule
1324: $r = L \gets L_1,\ldots,L_n,not~L'_1,\ldots,L'_m$ in $P$ s.t.\
1325: $L_i \in \Gamma^n(I)$, and $L'_i \not\in I$.
1326: By induction hypothesis, there exists arguments $A_1,\ldots,A_n$ for
1327: $L_1,\ldots,L_n$ with $\assm(A_i) \subseteq I$.
1328: Then $A = [r] \cdot A_1 \cdots A_n$ is an argument for $L$
1329: such that $\assm(A) \subseteq I$.\\[1ex]
1330: %
1331: ``Only-if'' direction: Induction on the length of the argument.\\[0.5ex]
1332: \textit{Base case}: $n = 1$:\\
1333: Then $A = [L \gets not~L_1,\ldots,not~L_n]$, and
1334: $L_1,\ldots,L_n \not\in I$. Then $L \gets \in \frac{P}{I}$,
1335: and $L \in \Gamma^1(I)$.\\[0.5ex]
1336: %
1337: \textit{Induction step}: $n \leadsto n+1$:\\
1338: Let $A = [L \gets L_1,\ldots,L_n,not~L'_1,\ldots,not~L'_m;r_2,\ldots,r_n]$
1339: be an argument s.t.\ $\assm(A) \subseteq I$.
1340: $A$ contains subarguments $A_1,\ldots,A_n$ for $L_1,\ldots,L_n$,
1341: with $\assm(A_i) \subseteq I$.
1342: Because $L'_1,\ldots,L'_m \not\in I$, then
1343: $L \gets L_1,\ldots,L_n \in \frac{P}{I}$.
1344: By induction hypothesis, $L_i \in \Gamma(I)$.
1345: so also $L \in \Gamma(I)$.
1346: \item ``If''-direction:
1347: Induction on the length $n$ of the derivation of $L \in \Gamma_s(I)$.\\[0.5ex]
1348: %
1349: \textit{Base case}: $n = 1$:\\
1350: Then there exists a rule $L \gets not~L_1,\ldots,not~L_n$ in $P$ s.t.\
1351: $\neg L,L_1,\ldots,L_n \not\in I$,
1352: and $[L \gets not~L_1,\ldots,not~L_n]$ is an argument for $L$
1353: whose assumptions are contained in $I$, and $\neg L \not\in I$.\\[0.5ex]
1354: %
1355: \textit{Induction step}: $n \leadsto n+1$:\\
1356: Let $L \in \Gamma^{n+1}(I)$. Then there exists a rule
1357: $r = L \gets L_1,\ldots,L_n,not~L'_1,\ldots,L'm$ in $P$ s.t.\
1358: $L_i \in \Gamma^n(I)$, $L'_i \not\in I$, and $\neg L \not\in I$.
1359: By induction hypothesis, there exists arguments $A_1,\ldots,A_n$ for
1360: $L_1,\ldots,L_n$ with $\assm(A_i) \subseteq I$ and
1361: $\neg \conc(A_i) \cap I = \emptyset$.
1362: Then $A = [r] \cdot A_1 \cdots A_n$ is an argument for $L$
1363: such that $\assm(A) \subseteq I$, and $\neg \conc(A) \cap I = \emptyset$.\\[1ex]
1364: %
1365: \newpage
1366: ``Only-if'' direction: Induction on the length of the argument.\\[0.5ex]
1367: \textit{Base case}: $n = 1$:\\
1368: Then $A = [L \gets not~L_1,\ldots,not~L_n]$, and
1369: $\neg L,L_1,\ldots,L_n \not\in I$. Then $L \gets \in \frac{P_s}{I}$,
1370: and $L \in \Gamma^1(I)$.\\[0.5ex]
1371: %
1372: \textit{Induction step}: $n \leadsto n+1$:\\
1373: Let~$A = [L \gets L_1,\ldots,L_n,not~L'_1,\ldots,not~L'_m;\ldots]$
1374: be an argument s.t.\ $\assm(A) \subseteq I$, and
1375: $\neg \conc(A) \cap I = \emptyset$.
1376: $A$ contains subarguments $A_1,\ldots,A_n$ for $L_1,\ldots,L_n$,
1377: with $\assm(A_i) \subseteq I$, and $\neg \conc(A_i) \cap I = \emptyset$.
1378: Because $L'_1,\ldots,L'_m \not\in I$, and $\neg L \not\in I$, then
1379: $L \gets L_1,\ldots,L_n \in \frac{P}{I}$.
1380: By induction hypothesis, $L_i \in \Gamma(I)$.
1381: so also $L \in \Gamma(I)$.
1382: \item and 4. follow immediately from \ref{prop:model-arg:u}. and
1383: \ref{prop:model-arg:a}., because $I$ is two-valued.
1384: \end{enumerate}
1385: \end{proof}
1386:
1387: \end{document}
1388: