=Paper=
{{Paper
|id=Vol-2454/paper_63
|storemode=property
|title=Context Graphs for Argumentation Logics
|pdfUrl=https://ceur-ws.org/Vol-2454/paper_63.pdf
|volume=Vol-2454
|authors=Michael Kohlhase,Max Rapp
|dblpUrl=https://dblp.org/rec/conf/lwa/KohlhaseR19
}}
==Context Graphs for Argumentation Logics==
https://ceur-ws.org/Vol-2454/paper_63.pdf
Context Graphs for Argumentation Logics
Michael Kohlhase, Max Rapp
Computer Science, FAU Erlangen-Nürnberg
Abstract. Representing human reasoning and argumentation requires
robust formalisms that go beyond classical, deductive logics in dealing
with aspects of human reasoning such as inconsistency or defeasibility.
The field of Formal Argumentation comprises a plethora of formalisms
that address a subset of these problem while occupying intersecting re-
gions of the space parametrised by the factors implementation, formality
and expressivity. This multiplicity complicates the compatibility, com-
parability and reuse of argument formalisms and argumentative content.
The modular approach to knowledge representation is designed to ad-
dress these problems. This paper proposes that modularity is best achieved
by refactoring argumentation formalisms into a representation language
and an on-top graph structure – the context graph. We claim that
argumentativeness arises from conflict- and support-relations between
internally consistent contexts and conjecture that every argumentation
formalism is isomorphic to some combination of a classical logic and a
context graph.
1 Introduction
In complex decision situations, individuals and organizations face a multitude
of options and alternatives. To reach a well-balanced and justified decision, it
is essential to systematically weigh arguments for and against an option and to
take into account different perspetives and assumptions. Support by informa-
tion technologies is indispensable for finding relevant facts and arguments and
to analyze and aggregate them in a given context – but currently, the requi-
site technologies are still in their infancy [CV18a]. Search engines and decision-
supporting information systems like e.g. IBM Watson operate on single facts
as information unit. They can extract large collections of facts from documents
but cannot consolidate them into arguments, much less contextualize or validate
arguments. Without an embedding into an argumentative frame, isolated facts
cannot yield deeper insights or justifications, so mere big-data-style correlation
analyses do not suffice for decision support in complex situations. To just name
one example: in the context of human/machine dialogues, generating targeted
explanations is indispensable to e.g. make erroneous behavior of a machine un-
derstandable [TM07].
Copyright ©2019 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
Meeting this challenge requires a mix of technologies: i) information re-
trieval and computational linguistics to extract facts, arguments, and contexts,
ii) knowledge representation technology to model arguments and their contexts,
iii) inference techniques to analyze, aggregate, and plausibilize them, and finally
iv) human/computer interaction technologies to make the ensuing information
systems amenable to humans. In recent years these challenges have inspired an
increasing amount of research: argumentation mining [CV18b] seeks to extract
argument(ation)s from text; argumentation theories [EV18] attempt to (empir-
ically or normatively) model human argumentative reasoning; dialogue systems
[Pra06] address the interactive aspect of argumentation. The speed of develop-
ment in this area is exemplified by the recent emergence of IBM’s Project Debater
[Pro] as the first system that implements the full argumentation pipeline – as
demonstrated in its much publicized debate with professional debater Harish
Natarajan.
The work presented in this paper is situated in the DFG Special Research
Action (SPP) 1999 “RATIO: Robust Argumentation Machines” [RATIO]; con-
cretely the ALMANAC (Argumentation Logics Manager & Argument Context
Graph) [AL] project in RATIO. It makes a contribution to the two middle as-
pects: knowledge representation and reasoning.
Concretely, we show how to systematically and modularly extend classical
logics by on-top graph structures yielding full-blown argumentation frameworks
in a knowledge representation system (MMT) that allows for rapid prototyping
and high intercompability of frameworks.
To this end in Section 2 we review previous attempts to unify and modularize
the plethora of argumentation formalisms and compare them to our approach. In
Section 3 we summarize the MMT system and language. In Section 4 we present
context graphs in MMT and how they can be used to capture argumentation
formalisms. We conjecture that context graphs enable us to characterize all of
the existing argumentation formalisms. Section 5 provides a first example of
how classical logics can be rendered argumentative though context graphs and
Section 6 carries out a first test of our conjecture. Concluding, in Section 7 we
summarize our findings and outline our future research plans.
2 State of the Art in Modularizing Formal Argumentation
Argumentation formalisms, for our purposes, include those frameworks that in-
clude an automated reasoning component. In particular, we don’t consider here:
– argument structure theories [Ree+17; Tou03] that investigate empiri-
cally which components make up (good) arguments;
– argument schemes [MWR17] that provide a taxonomy of argument-types
that frequently occur “in the wild”;
– representational frameworks [Che+06] that aim at maximal coverage of
argumentative content;
– dialogue systems [Pra06] that focus on the dynamics of argumentation
and the associated computational problems.
2
This does not mean that these fields do not pose interesting research questions
in our setting: especially argument schemes and argument dynamics are highly
interesting from an MMT perspective. However, we leave it to future work to
investigate these issues properly.
For a full review of the existing argumentation formalisms we defer to [Koh18]
and the excellent survey provided by [Pra17]. Here will only summarize the pre-
vious attempts to introduce greater unity and modularity to the zoo of existing
argumentation formalisms.
Logic-Based Argumentation The logic-based approach (LBA) [BH18] constitutes
the paradigm that is most closely related to our work. In logic-based argumenta-
tion a base logic is extended by definitions of arguments, counterarguments (that
is, attack between arguments) and argument graphs (composed from arguments
and counterarguments). An argument is a pair of premises Γ and a conclusion α
such that α can be derived from Γ in the proof theory of the base logic. One or
several counterargument relations are usually defined depending on the choice
of base logic. Usually these relate the claim of an argument to the premises
(undercut, defeat) or the claim of another (rebuttal). Argument graphs can be
created either through modelling of a given natural language argumentation or
through automatic generation from a given knowledge base in the base logic.
ASPIC+ On a high level, the structure of ASPIC+ [MP18] frameworks is similar
to LBA in that it consists of a base logic (called the logical language) and an
argumentative superstructure (called an argumentation system). However there
are three crucial differences: firstly, in ASPIC+ the proof theory is part of the su-
perstructure and may include defeasible rules. Secondly, knowledge-bases may
not only include fixed knowledge (axioms) but also defeasible content (ordinary
premises). Thirdly, the notions of argument, counterargument and argument
graphs are not freely definable but fixed with respect to the argumentation sys-
tem and the knowledge base.
As such ASPIC+ and LBA not only intersect in terms of expressivity but also
have functional differences: LBA is best viewed as a manual on how to extend
a given classical logic to an argumentative one. In contrast, ASPIC+ is a fixed
framework that can be instantiated by some combination of a logical language,
proof calculus and knowledge base but does not allow the modification of the
constituents of the framework itself.
Assumption-Based Argumentation Assumption-based Argumentation (ABA) [Cyr+17]
occupies a middle position between LBA and ASPIC+. Namely, it shares the basic
structure of a base logic with an argumentative superstructure with the former
two. In ABA the superstructure consists of sets of assumptions and a notion of
contrariness for sentences of the language. Like in LBA the base logic is usually
classical – that is there are no defeasible inference rules. On the other hand
there is only one version of attack between sets of assumptions which is defined
in terms of derivability and contrariness.
3
Historically, ABA is closely tied to the analysis of non-monotonic logics in
terms of abstract argumentation. In essence, by choosing the correct classical
base logic and a suitable notion of contrariness ABA allows the characterization
of many non-monotonic logics and their semantics. In spite of this similarity to
the LBA approach, ABA is not merely the fragment of LBA that deals with non-
monotonic logics: there is no equivalent to the notion of contrariness in LBA.
Neither is it a superset of ASPIC+ as it does not admit preference relations 1
over arguments (however the fragment of ASPIC+ without preferences can be
translated into ABA [Dun16]).
Summarizing, our approach differs from the existing modular frameworks in
several ways:
– Instead of defining counterarguments ad-hoc with respect to the given base
logic as in LBA or fixing their definitions as in ASPIC+ and ABA, we seek
to define them as logic- and even foundation-independently as possible. This
enables greater modularity and is achieved by constructing them from very
primitive notions such as theory-morphisms.
– Instead of being a mere superstructure on the base logic, context graphs en-
able the embedding of argumentative content into a powerful knowledge rep-
resentation framework (OMDoc/MMT). OMDoc/MMT provides much more
extensive ontology and context management capabilities than implementa-
tions of argumentation frameworks usually do. For example, content and in
principle also arguments can travel across the context graph through theory
morphisms and there is a priori no reason that different contexts could not
have different representation languages.
– Instead of developing frameworks on paper we implement them from the start
in the OMDoc/MMT knowledge representation system enabling features such
as proof checking, semantic computation and visualization.
– Finally, instead of fixing the semantics of arguments in terms of deductions
in the base logic, arguments in our approach can in principle take almost
arbitrary form; we do not exercise this here, but leave it to future work.
We therefore conjecture that classical logics plus context graphs subsume
ASPIC+, LBA, and ABA in terms of expressibility while at the same time be-
ing superior from a design perspective. In terms of expressibility we submit the
ALMANAC-conjecture (see Section 4) that any argumentation formalism can be
captured by a combination of a classical representation language and a context
graph. From a design perspective our modular approach enables reuse, compara-
bility and compatibility of formalisms and argumentative content in a powerful
knowledge representation framework. This allows the rapid prototyping of new
argumentation frameworks at a high level of implementation including capabil-
ities such as automated proof checking, argumentation semantic computation
and argument graph visualization.
1
However ABA extensions with preferences exist, see e.g. [Wak17]
4
3 Modular Knowledge Representation in the
OMDoc/MMT system
OMDoc [Koh06] is a wide-coverage representation language for mathematical
knowledge (formal) and documents (informal/narrative). In the last decade de-
velopment has focused on the formal aspect leading to the OMDoc/MMT in-
stance (Meta-Meta-Theories or Meta-Meta-Tool [RK13], henceforth simply MMT),
which increases expressivity, clarifies the representational primitives and for-
mally defines the semantics of this fragment.
MMT is designed to be foundation-independent and introduces several concepts
to maximize modularity and to abstract from and mediate between different
foundations. This enables the reuse of concepts, tools, and formalizations. The
MMT language integrates successful representational paradigms
– the logics-as-theories representation from logical frameworks,
– theories and the reuse along theory morphisms from the heterogeneous method,
– the Curry-Howard correspondence from type theoretical foundations,
– URIs as globally unique logical identifiers from OpenMath,
– the standardized XML-based interchange syntax of OMDoc,
and makes them available in a single, coherent representational system for the
first time. The combination of these features is based on a small set of care-
fully chosen, orthogonal primitives in order to obtain a simple and extensible
language design. Using these primitives, logical frameworks, logics and theories
within some logic are all uniformly represented as MMT theories, rendering all of
those equally accessible, reusable and extendable. Constants, functions, symbols,
theorems, axioms, proof rules etc. are all represented as constant declarations,
and all terms which are built up from those are represented as objects.
Theories are named groups of declarations at the top-level of MMT’s surface
syntax. A theory in MMT is declared as in Fig. 1. A theory usually declares a
metatheory that provides the language to be used in the theory’s declarations.
In Fig. 1 this is first-order logic (FOL). The body of the theory can include
other theories (in this case FOL natural deduction). In addtion this is where new
constants are declared.
Theory morphisms represent truth-preserving maps between theories. Exam-
ples include theory inclusions, translations/isomorphisms between (sub-)theories
and models/instantiations (by mapping axioms to theorems that hold within a
model), as well as a particular theory inclusion called meta-theory, that relates
a theory on some meta level to a theory on a higher level on which it depends.
This includes the relation between some low level theory (such as the theory of
groups) to its underlying foundation (such as first-order logic), and the latter’s
relation to the logical framework used to define it – e.g. LF; see [Pfe01] for an
overview.
5
All of this naturally theory background_knowledge : found:?Logic =
gives us the notion of a include found:?NaturalDeduction ❙
theory graph, which re- Tweety : type ❙
lates theories (represented bird : type ⟶ prop ❙
as nodes) via vertices repre- axiom: ⊦ bird Tweety ❙
senting theory morphisms ❚
(as in Fig. 2), being right at
the design core of the OM-
Doc/MMT language. Fig. 1. The head of the theory declaration contains
the theory’s name and metalanguage (an MMT FOL
It is a central advantage
implementation) and is delimited by “=”. The proof
of the OMDoc/MMT sys- theory for FOL is included in the first line of the body.
tem that theory morphisms The other lines are constant declarations: read “Tweety
“transport axioms, defini- is a bird”.
tions, theorems, …” to new
contexts and thus induce
knowledge that is not explicitly represented in the graph. Therefore it is a central
design invariant of the system that we can name all induced objects with canon-
ical URIs, the MMT URIs, which contain enough information to reconstruct the
induced objects themselves – given the graph.
3.1 Derived Modules
Modules are the top-level
declarations of the MMT translation m
language. The primitive LF LF + X
modules are theories and inclusion
theory morphisms (mainly meta-theory m′
FOL HOL
views and structures). They
have dedicated correspond- mult
ing data structures in MMT’s
abstract syntax that are Monoid cgroup add Ring
known to other MMT com-
ponents such as MMT’s Fig. 2. A Theory Graph with Meta-Theories
type checker. In the MMT
surface syntax a module declaration starts with a keyword and takes an op-
tional definiens in terms of other modules. This is followed by the body of the
module containing its declarations and a concluding module delimiter. Besides
primitive modules, MMT offers users the ability to define derived modules.
Derived modules elaborate into some combination of more primitive modules.
This allows for the definition of a great variety of theory- or morphism-like mod-
ules while at the same time maintaining MMT features like proof-checking.
The conceptual advantage of derived declarations and modules in MMT is
that they allow to combine the advantages of deep and shallow encodings –
here from argumentation theories into MMT. Generally, an encoding models the
meaning of (structures of) the source language using structures of the target
language. We call an encoding shallow if the encoding preserves the structure
6
of the source language, otherwise deep. Derived modules allow us to give shal-
low embeddings by extending the “syntax” of MMT theory graphs with theory
relations that structurally resemble the argumentation logics, while their elabo-
ration generates the deep embedding into MMT primitives that can be managed
and type-checked.
4 Context Graphs and the ALMANAC-Conjecture
The idea first put forward in [Koh18] is to enrich theory graphs with argumen-
tative relations to capture existing argumentation theories and offer increased
context management capabilities. In this paper this idea is elaborated in terms
of derived theory relations. In context graphs, theories are interpreted as po-
tentially mutually exclusive yet internally consistent contexts. The intuition is
that an argument is a locally valid “deduction” in that it holds with respect to
its context – a set of assumptions, axioms, inference rules or even global theories
that can be interpreted, for example, as the persuasions of an agent, the tenets
of a certain field or the contents of a knowledge base.
We argue that argumentation theories are particular instances of such context
graphs where the base logic and the admissible theory relations are fixed. MMT
already comprises an immense archive of possible base logics: the LATIN Logic
Altas [Cod+11; LATIN]. In this paper we use derived relations to enrich it with
argumentative theory relations. Generally we submit
Conjecture 1 (ALMANAC Conjecture). Each argumentation formalism A can
be captured by a classical object-language L and a context graph scheme G such
that A is isomorphic to hL, Gi.
Due to the prominence of argumentation in human thought, if true, the AL-
MANAC-conjecture would imply that much of human dialectical capability can
be constructed from classical logics plus extremely simple ingredients such as
theory morphisms. This reduction of an important human faculty to simple in-
gredients would constitue a first step towards a grammar of thought that would
identify the basic components of human reasoning and the rules of their compo-
sition.
5 Example 1: Inconsistency Graphs
The simplest way to extend a classical logic with argumentative capabilities is
to make use of the logic’s built-in inconsistency symbol ⊥ . ⊥ is either part of
the language or can be defined in almost all classical logics. An inconsistency
relation based on ⊥ is thus of special interest as classical logics – in particular
first-order logic and higher order logics – traditionally form the metatheories used
to approximate natural mathematical language. Therefore any theory relation
defined only in terms of ⊥ could be used in almost arbitrary mathematical
domains via MMT’s inheritance mechanisms.
7
We shall develop the intended joint-inconsistency relation in the context of
propositional logic. As such we require that all theories in an inconsistency graph
have a common meta-theory that includes at least propositional logic. Then we
define inconsistency graphs as follows:
Definition 1 (Inconsistency Relation). Let {T1 , . . . , Tn } be a set of theories,
C a conflict theory declaring only ` ⊥ and M a theory that includes proposi-
tional logic and is a meta-theory for all Ti and∪C. Then {T1 , . . . , Tn } are jointly
n
inconsistent iff there exists a total view C 7→ i=1 Ti .
In other words a collection of theories is jointly inconsistent iff there exists
a homomorphism from the inconsistent theory into their union. Procedurally,
MMT requires the user to declare an inconsistency relation by specifying the
conflict theory C and an assignment for ` ⊥ either in the∪form of a declaration
n
of the target theory or in the form of a proof ϕ that ∪n i=1 Ti ` ⊥. It then
elaborates the declaration by implicitly
∪n constructing i=1 Ti through the use
of includes and a view
∪n from C to i=1 T i that maps ` ⊥ to ϕ. Next it checks
whether ϕ is a valid i=1 Ti proof.
Inconsistency graphs are then defined like so:
Definition 2 (Inconsistency Graph). Let G be a theory graph with vertices
V and edges E. G is an inconsistency graph if
– V is a set of theories;
– E = V iews ∪ M etas ∪ Includes ∪ Inconsistencies where V iews, M etas,
Includes are the theory morphisms described earlier and Inconsistencies is
an inconsistency relation
– there is a meta-theory M ∈ V that includes at least propositional logic such
that (M, T ) ∈ M etas for all T ∈ V
Figure 3 displays an example of such an inconsistency graph. Here the meta-
theory is first-order logic and the theories declare an assortment of facts involving
some common ground. The theory “Common Ground” corresponds to the theory
declaration in Fig. 1. Two jointly inconsistent extensions of “Common Ground”
arise on the question whether Tweety can fly or not. The double-arrow denoting
joint inconsistency is elaborated by MMT into the part of the graph color-coded
in red. The view φ maps d to a proof of ⊥ using conjunction introduction (CI)
and falsum introduction (F I).
6 Example 2: ABA and Asymmetric Conflict Relations
As we have noted in Section 2 ABA is one of the major unifying frameworks
in argumentation and non-monotonic logic. We will carry out a first test of
the ALMANAC-hypothesis by characterzing ABA in terms of a context graph.
Before we tackle this problem we need to formally define ABA-frameworks in the
following section.
8
Metatheory
Conflict Theory
First Order Logic
d:`⊥
`, ∀, ∧, ∃, ...
φ : d 7→ F I CI(b c)
Joint Inconsistency
a
b, c a, c
a, b
Tweety can fly Tweety cannot fly
a a
b : ` F ly(T weety) c : ` ¬F ly(T weety)
a a
Common Ground
a : ` bird(T weety)
Fig. 3. A context graph scheme characterizing the binary joint inconsistency relation.
6.1 Assumption-Based Argumentation
ABA presupposes a classical base logic together with a proof calculus:2
Definition 3 (Deductive System). A deductive system is a pair hL, Ri where
L is any classical logic that contains at least the falsum symbol ⊥ and R is a proof
calculus on L that has at least the falsum introduction rule ` α, ` ¬α −→` ⊥.
Such classical deductive systems are then rendered argumentative through
the addition of set of assumptions and a contrary-operator:
Definition 4. (Assumption-Based Framework) An Assumption-Based Frame-
work with respect to a deductive system hL, Ri is a triple hT, ABox, ¯ i where
T, ABox ⊆ L are a Tbox and a set of assumptions respectively. ¯ is a function
L −→ L
The contrary operator ¯ is freely definable together with the base logic deter-
mines the the characterized non-monotonic logic. Such characterization results
exist among other logics for logic programming, default logic and autoepistemic
logic and non-monotonic modal logic [Bon+97].
While the notion of argument is not explicitly defined in ABA, their role
is essentially played by derivations. A formula α over L is derivable from a
set of formulas T (put T ` α) if there exists a sequence of formulas β1 , . . . , βn
2
Our exposition here follows [Bon+97].
9
s.t. βn = α and for each i = 1, . . . , n, βi ∈ T or there is α1 , .., αm ` βi with
aj ∈ {β1 , . . . , βi−1 } for all j=1,…,m.
Attacks between sets of formulas are then defined as follows:
Definition 5. (Attack) A set of formulas F attacks another one F ′ iff there is
f ∈ F ′ s.t. F ` f . If F ′ = {f } we say that F attacks f .
The key difference to the notion of inconsistency discussed in Section 5 is
that attack may be asymmetric. Consider the following example:
Example 1. Consider the assumption-based framework defined as follows:
– hL, Ri = Propositional Language and Calculus.
– T = {a → b}
– ABox = Arg1 ∪ Arg2
– Arg1 = {¬c}
– Arg2 = {a, b → c}
– φ = ¬φ
Clearly, Arg2 attacks Arg1 as we can derive c (the contrary of ¬c using
Modus Ponens twice. However, there is no attack from Arg1 to Arg2 as Arg1 ∪ T
is already logically closed and C ∈
/ Arg1 .
6.2 Assumption-Based Attack Graphs
The challenge in characterizing ABA in terms of a context graph is to capture
the asymmetric attack relation in terms of theory morphisms.
Towards this goal we modify the metalogic in which we are working. In-
stead of propositional logic we now allow for any logic with propositional let-
ters, a proof calculus and an unary contrariness operator ¯ . Such a contrari-
ness operator could be classical negation but we also allow for any other notion
of contrariness. In oder to define assumptions, we extend this metalanguage
slightly: in addition to a contrary operator we equip it with an assumption-
hood operator |∼ and a rule assumptionhood implies derivability (aid) that states
|∼α −→` α for any well-formed formula α. We call the resulting language an
assumption-enriched logic.
The assumptionhood operator is used to distinguish declarations that are
assumptions from “ordinary” declarations. Contrary to an ordinary declaration,
an assumption can become the target of an attack. In this way it introduces the
asymmetry we are after:
Definition 6 (Assumption-Based Attack Relation). Let T , T1 , T2 , C, C1 , C2
be theories that share a common meta-theory M that includes an assumption-
enriched logic such that
– T1 includes T ,
– T2 includes T ,
– C declares only a constant c,
10
– C1 includes C and declares only |∼c,
– C2 includes C and declares only ` c.
Then T1 attacks T2 iff
– there exists a total view δ : C 7→ T such that ϕ(c) = t for some expression t
of T (the kernel of the attack),
– there exists a total view ϕ : C1 7→ T1 such that ϕ(|∼c) = |∼t (the assumption
wing of the attack),
– there exists a total view ψ : C1 7→ T2 such that ϕ(` c) = π where π is a proof
of t (the derived wing of the attack).
The kernel of the attack pinpoints the conflict and enforces that the decla-
rations from the wings are mapped to mutual contraries of the same expression.
The derived wing designates the origin of the attack arrow whereas the assump-
tion wing demarcates its target.
Analogously to the joint inconsistency case, given a declaration of an attack
relation by the user, MMT will implicitly construct and proof-check the conflict
theories and views. In this case the user has to provide three view declarations
in the body of the attack module.
Definition 7 (Assumption-based Attack Graph). Let G be a theory graph
with vertices V and edges E. G is an Assumption-based Attack graph if
– V is a set of theories;
– E = V iews ∪ M etas ∪ Includes ∪ Attacks where V iews, M etas, Includes
are the theory morphisms described earlier and Attacks is an attack relation;
– there is an assumption-enriched meta-theory M ∈ V such that (M, T ) ∈
M etas for all T ∈ V
Example 1 (continued). Consider again our earlier example only that now
T = T , Arg1 = T1 and Arg2 = T2 . The metalanguage is propositional logic
where contrary is just plain negation. It is extended by the assumptionhood
operator |∼ and aid. We then need to construct the kernel and wings of th attack
from the canonical theories C, C1 , C2 . Fig. 4 showcases this in detail. The kernel
δ : C 7→ T maps w to c thereby ensuring that both of the wings have to map
to the same formula c (and its contrary c respectively). The assumption wing
ϕ requires an assumption as its target, the derived wing ψ a derivation. We
achieve this by setting the codomain of ϕ to Arg1 , mapping |∼w to |∼¬c, and
the codomain of ψ to Arg2 , mapping ` w to a derivation c. The derivation
uses negation introduction and twice modus ponens to derive ¬¬c which is the
contrary of ¬c. Note that we cannot reverse the wings and map |∼c to |∼¬c in
Arg1 as |∼¬c is not declared in Arg1 .
Example 1 showcases the major result of this section: assumption-based at-
tack graphs subsume assumption-based frameworks. We simply translate the
assumption-based framework’s contrary to our meta-language’s contrary, each
subset of assumptions to a theory with assumptions as |∼-declarations and in-
stantiate every attack as an assumption-based attack.
11
Contrary
contrary = ¬ # ¯· Meta (Propositional Logic)
a : prop → type # |∼ 1 prop, `, ∧, ∨, ¬, M P, N I, ...
aid : {x : prop} |∼ x −→` x
C
w : prop
δ : w 7→ c
C1 C2
con1 : |∼w con2 : ` w̄
ϕ : con1 7→ a1 ψ : con2 7→ π
Arg 2
Arg 1
a2 : |∼a
a1 : |∼¬c
a3 : |∼b → c
T
a : prop
b : prop
c : prop π = N I(M P (M P ((aid a2 )ax1 ))a3 )
ax1 : ` a → b
Fig. 4. ABA Example
7 Conclusion
We have shown how to render classical logics argumentative through context
graphs using the examples of inconsistency graphs and asumption-based attack
graphs. In this process we have confirmed the ALMANAC conjecture for the case
of Assumption-Based Argumentation Frameworks – one of the major paradigms
in formal argumentation. In future work we will demonstrate how this modular
approach to argumentation formalism design enables the rapid prototyping of
full-blown argumentation systems including proof-checking, semantic computa-
tion and visualization. In addition we want to investigate additional elaborations
for attack and other argumentation relations. A first idea to be investigated for
ABA would be an alternative way to facilitate non-symmetric attacks by insist-
ing that the view φ in Figure 4 – i.e. the view into the target of the attack – be
simple, i.e. maps constants to constants. Furthermore, we note that the elabora-
tions have a distinct flavor of categorical constructions. This suggests that there
is a connection of our work in institution theory. We want to extend [Rab08] to
study this in more detail.
12
References
[AL] ALMANAC: Argumentation Logics Manager & Argument Context
Graph. Project Home Page. url: http://kwarc.info/projects/
almanac/ (visited on 06/17/2018).
[Bar+18] Pietro Baroni, Dov Gabbay, Massimiliano Giacomin, and Leendert
van der Torre, eds. Handbook of Formal Argumentation. College Pub-
lications, 2018.
[BH18] Philipp Besnard and Anthony Hunter. “A Review of Argumentation
based on Deductive Arguments”. In: (2018). Ed. by Pietro Baroni,
Dov Gabbay, Massimiliano Giacomin, and Leendert van der Torre,
pp. 437–484.
[Bon+97] A. Bondarenko, P.M. Dung, R.A. Kowalski, and F. Toni. “An ab-
stract, argumentation-theoretic approach to default reasoning”. In:
Artificial Intelligence 93.1 (1997), pp. 63 –101. doi: https://doi.
org/10.1016/S0004-3702(97)00015-5.
[Che+06] Carlos Chesñevar et al. “Towards an Argument Interchange Format”.
In: The Knowledge Engineering Review 21.04 (Dec. 2006), p. 293.
doi: 10.1017/s0269888906001044.
[Cod+11] Mihai Codescu et al. “Project Abstract: Logic Atlas and Integra-
tor (LATIN)”. In: Intelligent Computer Mathematics. Ed. by James
Davenport, William Farmer, Florian Rabe, and Josef Urban. LNAI
6824. Springer Verlag, 2011, pp. 289–291. url: https : / / kwarc .
info/people/frabe/Research/CHKMR_latinabs_11.pdf.
[CV18a] Elena Cabrio and Serena Villata. “Five Years of Argument Mining:
a Data-driven Analysis”. In: Proceedings of the Twenty-Seventh In-
ternational Joint Conference on Artificial Intelligence, IJCAI-18.
International Joint Conferences on Artificial Intelligence Organiza-
tion, July 2018, pp. 5427–5433. doi: 10.24963/ijcai.2018/766.
[CV18b] Elena Cabrio and Serena Villata. “Five Years of Argument Mining:
a Data-driven Analysis”. In: Proceedings of the Twenty-Seventh In-
ternational Joint Conference on Artificial Intelligence, IJCAI-18.
International Joint Conferences on Artificial Intelligence Organiza-
tion, July 2018, pp. 5427–5433. doi: 10.24963/ijcai.2018/766.
[Cyr+17] Kristijonas Cyras, Xiuyi Fan, Claudia Schulz, and Francesca Toni.
“Assumption-based argumentation: Disputes, explanations, prefer-
ences”. In: IFCoLog Journal of Logics and Their Applications 4.8
(2017), pp. 2407–2456.
[Dun16] Phan Minh Dung. “An Axiomatic Analysis of Structured Argumen-
tation with Priorities”. In: Artif. Intell. 231.C (Feb. 2016), pp. 107–
150. doi: 10.1016/j.artint.2015.10.005.
[EV18] Frans H van Eemeren and Bart Verheij. “Argumentation Theory in
Formal and Computational Perspective”. In: (2018). Ed. by Pietro
Baroni, Dov Gabbay, Massimiliano Giacomin, and Leendert van der
Torre, pp. 3–73.
13
[Koh06] Michael Kohlhase. OMDoc – An open markup format for mathe-
matical documents [Version 1.2]. LNAI 4180. Springer Verlag, Aug.
2006. url: http://omdoc.org/pubs/omdoc1.2.pdf.
[Koh18] Michael Kohlhase. “Towards Context Graphs for Argumentation
Logics”. In: ed. by Rainer Gemulla et al. Vol. 2191. CEUR Work-
shop Proceedings. CEUR-WS.org, 2018, pp. 203–214. url: http :
//ceur-ws.org/Vol-2191/paper25.pdf.
[LATIN] The LATIN Logic Atlas. url: https://gl.mathhub.info/MMT/
LATIN (visited on 06/02/2017).
[MP18] Sanjay Modgil and Henry Prakken. “Abstract Rule-Based Argumen-
tation”. In: (2018). Ed. by Pietro Baroni, Dov Gabbay, Massimiliano
Giacomin, and Leendert van der Torre, pp. 287–408.
[MWR17] Fabrizio Macagno, Douglas Walton, and Chris Reed. “Argumenta-
tion Schemes. History, Classifications, and Computational Applica-
tions”. In: IFCoLog Journal of Logics and Their Applications 4.8
(2017). url: http : / / dougwalton . ca / papersinpdf / 17IFColog
SCHEMES.pdf.
[Pfe01] Frank Pfenning. “Logical Frameworks”. In: Handbook of Automated
Reasoning. Ed. by Alan Robinson and Andrei Voronkov. Vol. I and
II. Elsevier Science and MIT Press, 2001.
[Pra06] Henry Prakken. “Formal systems for persuasion dialogue”. In: The
Knowledge Engineering Review 21.2 (June 2006), pp. 163–188. doi:
10.1017/s0269888906000865.
[Pra17] Henry Prakken. “Historical Overview of Formal Argumentation”.
In: IFCoLog Journal of Logics and Their Applications 4.8 (2017),
pp. 2183–2262. url: http://www.cs.uu.nl/groups/IS/archive/
henry/history.pdf.
[Pro] Project Debater - How does it work? Accessed: 2019-24-06. url:
https : / / www . research . ibm . com / artificial - intelligence /
project-debater/how-it-works/.
[Rab08] Florian Rabe. “Representing Logics and Logic Translations”. PhD
thesis. Jacobs University Bremen, 2008. url: http://kwarc.info/
frabe/Research/phdthesis.pdf.
[RATIO] RATIO: Robust Argumentation Machines. Home Page of the DFG
Special Research Action (SPP) 1999. url: http://spp-ratio.de
(visited on 06/17/2018).
[Ree+17] Chris Reed et al. “The Argument Web: an Online Ecosystem of
Tools, Systems and Services for Argumentation”. In: Philosophy &
Technology 30.2 (May 2017), pp. 137–160. doi: 10.1007/s13347-
017-0260-8.
[RK13] Florian Rabe and Michael Kohlhase. “A Scalable Module System”.
In: Information & Computation 0.230 (2013), pp. 1–54. url: http:
//kwarc.info/frabe/Research/mmt.pdf.
[TM07] Nava Tintarev and Judith Masthoff. “A Survey of Explanations in
Recommender Systems”. English. In: Data Engineering Workshop.
14
Ed. by G. Uchyigit. IEEE Computer Society, Dec. 2007, pp. 801–
810. doi: 10.1109/ICDEW.2007.4401070.
[Tou03] Stephen E Toulmin. The uses of argument. Cambridge university
press, 2003.
[Wak17] Toshiko Wakaki. “Assumption-Based Argumentation Equipped with
Preferences and its Application to Decision Making, Practical Rea-
soning, and Epistemic Reasoning”. In: Computational Intelligence
33.4 (2017), pp. 706–736. doi: 10.1111/coin.12111. eprint: https:
//onlinelibrary.wiley.com/doi/pdf/10.1111/coin.12111.
15