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 regions of the space parametrised by the factors implementation, formality and expressivity. This multiplicity complicates the compatibility, comparability and reuse of argument formalisms and argumentative content. The modular approach to knowledge representation is designed to address 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.
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 diferent perspetives and assumptions. Support by information technologies is indispensable for finding relevant facts and arguments and to analyze and aggregate them in a given context – but currently, the requisite technologies are still in their infancy [CV18a]. Search engines and decisionsupporting 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 understandable [TM07].
Meeting this challenge requires a mix of technologies: i) information retrieval 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 (empirically or normatively) model human argumentative reasoning; dialogue systems [Pra06] address the interactive aspect of argumentation. The speed of development 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]; concretely the ALMANAC (Argumentation Logics Manager & Argument Context Graph) [AL] project in RATIO. It makes a contribution to the two middle aspects: 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
Argumentation formalisms, for our purposes, include those frameworks that include an automated reasoning component. In particular, we don’t consider here: – argument structure theories [Ree+17; Tou03] that investigate empirically 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.
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 previous 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 argumentation 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 diferences: firstly, in ASPIC+ the proof theory is part of the superstructure 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 system and the knowledge base.
As such ASPIC+ and LBA not only intersect in terms of expressivity but also have functional diferences: 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.
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 nonmonotonic 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 difers 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 enable the embedding of argumentative content into a powerful knowledge representation framework (OMDoc/MMT). OMDoc/MMT provides much more extensive ontology and context management capabilities than implementations 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 diferent contexts could not have diferent 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 being 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, comparability 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 capabilities such as automated proof checking, argumentation semantic computation and argument graph visualization. 1 However ABA extensions with preferences exist, see e.g. [Wak17]
OMDoc/MMT system OMDoc [Koh06] is a wide-coverage representation language for mathematical knowledge (formal) and documents (informal/narrative). In the last decade development has focused on the formal aspect leading to the OMDoc/MMT instance (Meta-Meta-Theories or Meta-Meta-Tool [RK13], henceforth simply MMT), which increases expressivity, clarifies the representational primitives and formally 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 diferent 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 ifrst time. The combination of these features is based on a small set of carefully 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. Examples 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.
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 OMDoc/MMT language. Fig. 1. The head of the theory declaration contains
It is a central advantage the theory’s name and metalanguage (an MMT FOL of the OMDoc/MMT sys- itmhepolreymfeonrtaFtOioLni)s ainncdluidseddeilnimtihtee dfirstbylin“e=o”f. tThheebopdroy.of 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 canonical URIs, the MMT URIs, which contain enough information to reconstruct the induced objects themselves – given the graph. 3.1
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 FOL m′ 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 components 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 optional 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 ofers 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 modules 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 of the source language, otherwise deep. Derived modules allow us to give shallow embeddings by extending the “syntax” of MMT theory graphs with theory relations that structurally resemble the argumentation logics, while their elaboration generates the deep embedding into MMT primitives that can be managed and type-checked. 4
The idea first put forward in [ Koh18] is to enrich theory graphs with argumentative relations to capture existing argumentation theories and ofer increased context management capabilities. In this paper this idea is elaborated in terms of derived theory relations. In context graphs, theories are interpreted as potentially 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 ALMANAC-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 ingredients would constitue a first step towards a grammar of thought that would identify the basic components of human reasoning and the rules of their composition. 5
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 ifrst-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.
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 fT1, . . . , Tng be a set of theories, C a conflict theory declaring only ` ? and M a theory that includes propositional logic and is a meta-theory for all Ti and C. Then fT1, . . . , Tng are jointly inconsistent if there exists a total view C 7! ∪in=1 Ti.
In other words a collection of theories is jointly inconsistent if 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 of the target theory or in the form of a proof ϕ that ∪n . It then elaborates the declaration by implicitly constructing ∪n i=1 Ti ` ? i=1 Ti through the use of includes and a view from C to ∪in=1 Ti that maps ` ? to ϕ. Next it checks whether ϕ is a valid ∪n
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 2 V that includes at least propositional logic such that (M, T ) 2 M etas for all T 2 V 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.
First Order Logic `, 8, ^, 9, ...
a b : ` F ly(T weety) a, b a φ : d 7! F I CI(b c)
d : ` ?
a b, c
a : ` bird(T weety) a, c
a c : ` :F ly(T weety) a 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 Framework 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 determines 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]. s.t. βn = α and for each i = 1, . . . , n, βi 2 T or there is α1, .., αm ` βi with aj 2 fβ1, . . . , βi−1g 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 ′ if there is f 2 F ′ s.t. F ` f . If F ′ = ff g we say that F attacks f .
The key diference to the notion of inconsistency discussed in that attack may be asymmetric. Consider the following example: Section 5 is Example 1. Consider the assumption-based framework defined as follows: – hL, Ri = Propositional Language and Calculus. – T = fa ! bg – ABox = Arg1 [ Arg2 – Arg1 = f:cg – Arg2 = fa, b ! cg – φ = :φ
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 2/ Arg1. 6.2
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. Instead of propositional logic we now allow for any logic with propositional letters, a proof calculus and an unary contrariness operator ¯ . Such a contrariness 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 assumptionhood operator j and a rule assumptionhood implies derivability (aid) that states j α !` α 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 assumptionenriched logic such that – T1 includes T , – T2 includes T , – C declares only a constant c, – C1 includes C and declares only j c, – C2 includes C and declares only ` c.
Then T1 attacks T2 if – 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 ϕ(j c) = j 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 declarations from the wings are mapped to mutual contraries of the same expression. The derived wing designates the origin of the attack arrow whereas the assumption 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 2 V such that (M, T ) 2
M etas for all T 2 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 j 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 j w to j :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 j c to j :c in Arg1 as j :c is not declared in Arg1.
Example 1 showcases the major result of this section: assumption-based attack 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 j -declarations and instantiate every attack as an assumption-based attack. Contrary contrary = : # ¯ a : prop ! type # j 1 aid : fx : propg j x !` x
C1 con1 : j w Arg 1 a1 : j :c ϕ : con1 7! a1
C w : prop
δ : w 7! c T a : prop b : prop c : prop ax1 : ` a ! b Fig. 4. ABA Example
Meta (Propositional Logic) prop, `, ^, _, :, M P, N I, ...
C2 con2 : ` w¯
ψ : con2 7! π Arg 2 a2 : j a a3 : j b ! c π = N I(M P (M P ((aid a2)ax1))a3) 7
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 computation 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 insisting 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 elaborations 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. [Koh06] Michael Kohlhase. OMDoc – An open markup format for mathematical 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 Workshop 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 Argumentation”. 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. “Argumentation Schemes. History, Classifications, and Computational Applications”. 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/s13347017-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 Masthof. “A Survey of Explanations in Recommender Systems”. English. In: Data Engineering Workshop. [Wak17]