Towards Context Graphs for Argumentation Logics Michael Kohlhase Computer Science, FAU Erlangen-Nürnberg Abstract. Decision situations require individuals and organizations to choose between a multitude of options based on facts, opinions, and arguments about the situation at hand or similar ones. Current support systems are mostly fact-based and fail to take into account arguments found on the web or in the literature. In this paper we propose to use modular, theory-graph knowledge repre- sentation formats to model the contexts in multi-agent argumentations: theory graphs naturally provide “little ontologies” (the theories) that can be mutually exclusive and are interconnected by inclusions and views (in OMDoc/MMT). To augment them to full argumentation context graphs we add argumentation relations like attack, rebut, support, and undercut and study their ontological properties. 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 es- sential to systematically weigh arguments for and against an option and to take into account different perspetives and assumptions. Support by information tech- nologies is indispensable for finding relevant facts and arguments and to analyze and aggregate them in a given context – but currently, the requisite technologies are missing. 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 dialogs, generating targeted explanations is indispensable to e.g. make erroneous behavior of a machine understandable or to render predictions of malfunctions comprehensible. 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. The work presented in this paper is situated in the DFG Special Research Action (SPP) 1999 “RATIO: Robust Argumentation Ma- chines” [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 bring order into the zoo of logic-based approaches to common sense reasoning and argumentation, and systematically extend log- ics with features from argumentation frameworks. Section 2 reviews the state of the art, and Section 3 details the knowledge representation framework we use. Section 4 gives the details of “argumentation systems as theory graphs” construction, an Section 5 concludes the paper. 2 State of the Art in Logic-Based Argumentation There is a large set of prior work on the representation of knowledge, inference and computational models for argumentations. We will survey i) logical models for individual reasoning (arguments) and ii) models for the interaction of ar- guments brought forth by multiple agents (argumentation systems) in the next two sections (2.1 and 2.2). We observe that these two aspects are independent of each other, which opens the way to mixing and matching to get adequate target systems for representing real-world argumentations. 2.1 Argumentation Systems The field of argumentation systems (see e.g. [BH08] for a general overview) uses various approaches to representing arguments and their interaction with counter-arguments. The foundational work of Dung [Dun95] introduces abstract argumentation systems (AAS) as directed graphs, in which “arguments” are nodes and edges are “attack relations” between arguments. Dung’s model treats arguments as atomic by abstracting from their inner structure. Extending AASs with an additional support relation yields bipolar argumen- tation frameworks. AASs can also be extended by adding a preference relation on arguments (preference-based argumentation frameworks), which are further refined by value-based argumentation frameworks. [JHHC15] surveys these ex- tensions. Structured argumentation [BH08] gives arguments an internal e.g. deductive structure. This allows to study and catalogue argumentation schemata in texts Abstract Dialectical Frameworks (ADF) are hybrids between abstract and struc- tured argumentation (see [Bre+13]), they are currently the focus of study, as they generalize many of the existing formal models of argumentation. Argument trees can be used to formalize undercuts in an argumentation [BH06]. An edge in such a tree points from an argument concluding ¬P to an argument using P as a premise. 2 Assumption-based argumentation, a form of structured argumentation ex- tended by “defeasible axioms” (i.e. assumptions), lend themselves to being rep- resented as more general graphs [CT16]. Closely related is Hunter’s framework for approximate arguments [Hun07] based on enthymemes, where arguments can have implicite assumptions not necessarily shared between all participating agents. First-Order Argumentation Somewhat surprisingly, there are few systems that consider properties beyond simple propositional logical aspects; a notable excep- tion is Besnard and Hunter’s work on a “first-order argumentation framework” [BH05]. Here, the argument trees presented in [BH06] are extended by first-order quantifiers. 2.2 Robust Representation of Individual Inference In classical logic, the calculus of natural deduction [Gen35] serves as a foundation for single-agent argumenation. For the representation of real-world knowledge and inferences and such given in natural language, “robust” logics integrate infer- ence with insecure knowledge (e.g. probabilistic and fuzzy logics), non-monotonic reasoning (e.g. default logics, abduction and induction) or linguistic phenomena (e.g. discourse logics and modal logics). These logics are usually classified as “philosophical logics” or “non-classical logics”[GG84]; – we prefer to think of them as logics that allow the robust representation of human argumentations. Logics for robust representation of argumentation A plethora of logics have been devised to express various aspects of natural language or logical inference not covered by classical logic. To name only some examples, (multi-)modal logics extend classical logic by (potentially various different) notions of possibility and necessity. Preference logic allows for stating sentences of the form “A is bet- ter than / worse than B”. Relevance logic restricts the classical (i.e. material) implication in such a way as to avoid valid implications between seemingly dis- connected premises and conclusions, which seems false from a colloquial under- standing of “If... then”-sentences. It is one example for paraconsistent logics, which try to deal with inconsistency in a non-fatal manner by systematically avoiding ex falso quodlibet. Temporal logics allow for reasoning about time (e.g. “X is true at time t0 ”), probabilistic logics about probabilities. Dynamic Logics Representations of arguments naturally arise from the interpre- tation/formalization of natural language documents. A paradigmatic language here is Discourse Representation Theory (DRT) [KR93] which introduces “dis- course referents” to treat anaphoric references in statements like “A student is sleeping. He is tired.”. In static logics, the first sentence would be modeled by a formula like ϕ = ∃x.x ∈ Student ∧ sleep(x). However, the “he” in the sec- ond sentence refers to the student in the first sentence, so formalizing the first sentence as ϕ doesn’t work, since the scope of the existential quantifier is re- stricted to that formula. Dynamic logics try to remedy these problems in various 3 ways by changing the behaviour of variables or introducing non-standard quanti- fiers with “non-recursive” scoping behaviour. Discourse referents also account for many other linguistic phenomena including tense, propositional attitudes, dia- logue, and – importantly for argumentation – presuppositions and propositional anaphora. Other dynamic logics include Dynamic Predicate Logic (DPL) [GS91], and their Montague-style higher-order versions [GS90; KKP96]. 2.3 Limitations: Interoperability & Context Management By and large, the robust logics surveyed above have usually been developed with a focus on the particular features and primitives they introduce to remedy a par- ticular shortcoming of classical logics. Efforts for integration of features in more comprehensive logics exist, but are unsystematic and sparse. As a consequence the logics – and the domain developments in them – are insular, duplicate work, and make comparison and benchmarking difficult. What we need for a robust representation of knowledge and argumentation is a system of shallow embeddings1 that make classical and non-classical log- ics practically interoperable and thus creates a uniform meaning space of logic-based representations. To do so, we need a uniform framework in which we can represent logics, their semantics, and their embeddings, so that we can systematically study – and engineer – combinations. In the argumentation theories reviewed above, the context of argumentation is essentially reduced to a set of assumptions. This makes the “management” of (and reasoning about) contexts – which humans routinely do in argumentation – difficult to model. Heterogeneous ontologies can be used as a structured basis for “graphs of argumentation contexts” if additional relations are introduced for overlaps and mutual exclusions of theories to make assumptions and their consequences explicitly representable and thus mechanizable. It seems that the management of argumentation contexts should be independent of the base logic – a service an argumentation framework should offer “on top”. 3 Towards Scalable Argumentation Logics We have identified three shortcomings in the state of the art: i ) a zoo of logical formalisms and frameworks that address various aspects of human inference and argumentation, but are usually incomparable and often even incompatible. ii ) the management of argumentation contexts, and To remedy these, we need to i ) An “Atlas of Argumentation Logics” to bring order into the zoo of argumen- tation logics and frameworks. Such an “atlas” identifies the representational and inferential primitives, a modular development in a (meta)-theory graph, and relates the systems via theory morphisms in the OMDoc/MMT format. 1 i.e. transformations that preserve structure and domain invariants and do not blow up formula sizes 4 ii ) “Context Graphs for Argumentation”, i.e. a logic-independent framework for context management in argumentations based on (domain-level) OM- Doc/MMT theory graphs. We show how these two goals can be obtained on the basis of existing represen- tation formats and knowledge management tools. 3.1 Theory Graphs for Modular Knowledge Representation 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 [RK13]), which increases expressivity, clarifies the representational primitives and formally defines the semantics of this fragment. OMDoc/MMT is designed to be foundation-independent and introduces sev- eral concepts to maximize modularity and to abstract from and mediate be- tween different foundations, to reuse concepts, tools, and formalizations. The OMDoc/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 theo- ries within some logic are all uniformly represented as OMDoc/MMT theories, rendering all of those equally accessible, reusable and extendable. Constants, functions, symbols, theorems, axioms, proof rules etc. are all represented as con- stant declarations, and all terms which are built up from those are represented as objects. 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. All of this naturally gives us the notion of a theory graph, which relates theories (represented as nodes) via vertices representing theory morphisms (as in Figure 1), being right at the design core of the OMDoc/MMT language. 5 It is a central advan- translation m tage of the OMDoc/MMT LF LF + X inclusion system that theory mor- meta-theory m0 phisms “transport axioms, FOL HOL definitions, theorems, . . . ” to new contexts and thus mult induce knowledge that is not explicitly represented Monoid cgroup add Ring in the graph. Therefore it is a central design invariant Fig. 1. A Theory Graph with Meta-Theories 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. Flexiformal Content Recently, OMDoc/MMT has been extended to enable han- dling content of flexible formality [Koh13] in a bid to reach full OMDoc coverage. In a nutshell, Informal parts are modeled as opaque constants, objects or theo- ries [Ian17]. While they can obviously not be formally analyzed with respect to their formal structure, they can still be used in (and be subject to) the various knowledge management services provided by MMT, in particular they can be connected to formal content via theory morphisms. As a result, we believe we can use OMDoc/MMT to represent all kinds of arguments in a unified manner, whether they can be fully formalized in some logic and/or argumentation system or need to be represented informally. 3.2 LATIN: an Atlas of (Classical) Logics The LATIN atlas [Cod+11] is a heterogeneous, highly integrated library of for- malizations of logics and related languages as well as translations between them. It uses OMDoc/MMT as a framework, with LF as a meta-theory for the individ- ual logics. True to the general OMDoc/MMT philosophy, all the integrated theories are built up in a modular way and include propositional, first-order, sorted first- order, common, higher-order, modal, description, and linear logics. Type theo- retical features, which can be freely combined with logical features, include the λ-cube, product and union types, as well as base types like booleans or natural numbers. In many cases alternative formalizations are given (and related to each other via theory morphisms), e.g., Curry- and Church-style typing, or Andrews and Prawitz-style higher-order logic. The logic morphisms include the rela- tivization translations from modal, description, and sorted first-order logic to unsorted first-order logic, the negative translation from classical to intuitionistic logic, and the translation from first to sorted first- and higher-order logic. The left side of Figure 2 shows a fragment of the LATIN atlas, focusing on first-order logic (FOL) being built on top of propositional logic (PL), its transla- tion to HOL and ultimately resulting in the foundations of Mizar, Isabelle/HOL 6 and ZFC, as well as translations between them. The formalization of proposi- tional logic includes its syntax as well as its proof and model theory, as shown on the right of Figure 2. In a nutshell, the LATIN Logic Atlas provides the logic- interoperability framework and seed content (classical, description, and some modal logics) that we called for in Section 2.3 above. Crucially, domain theories can be aligned by theory morphisms, iff there are “meta-morphisms” for them (see Figure 1), therefore LATIN – and an extension for robust logics and ar- gumentation frameworks – also provides an uniform meaning space for logical content and argumentations. LATIN already already contains some of the robust logics surveyed in Sec- tion 2.2, and we are currently working on formalizing more; due to the high level of reuse in LATIN, a logic (and its ND-based proof theory) can usually be added in a matter of one or two days. 4 Context Graphs for Argumentation Logics 4.1 Argumentation Relations in Theory Graphs Argumentation frameworks such as Dung-style frameworks [Dun95], abstract dialectical frameworks [Bre+13] or the first-order argumentation framework by Besnard and Hunter [BH05] introduce their own relations between arguments, such as support, refutation or undercut. Modelling arguments and their prerequisite knowledge and assumptions as theories, we can in P C turn model these relations as arrows between the- ories, giving rise to theory graphs as described in A ¬A Section 3.1 and thus using existing and new tools for theory graphs for applying these frameworks in a formal setting. Figure 3 shows a typical situa- tion for agents P and C, which agree on a common CG ground, expressed as the theory graph CG, but dif- fer on some assumption A, which P accepts and C rejects (see also Figure 4 for a real-world example). Fig. 3. Context Graph Base ∧Mod PL ML SFOL DFOL ¬ ... ∧ ∧Syn DL FOL HOL PL ∧Pf OWL CL Isabelle/HOL ZFC Mizar Fig. 2. A Fragment of the LATIN Atlas (from [KR16]) 7 Essentially, if P and C are “internally consistent”, then they accept only the material below the re- spective dashed line, but any argument that involves A will essentially play out in the top quadrant, which is contested by both – hence the argument. We have marked the tension between A and ¬A via the dotted “antithesis” line in Fig- ure 3. Context graphs are particularly interesting in the context of approximate arguments and enthymemes [Mai16]. This simple example already shows that theory graphs can serve as knowledge- based context models, where many interesting properties can be read off the graph struture. We conjecture that we can model the attack-like relations in ar- gumentation frameworks (e.g. refute and undercut) as paths in suitably granular theory graph which contain a single “antithesis”-like relation and the support- like relations as paths without. Modelling context graphs as theory graphs naturally implies that the rela- tions in these graphs (support, refutation, attack, undercut etc.) become different arrows in a theory graph. The theory graphs used by OMDoc/MMT currently (mostly) assume, that the arrows are various kinds of theory morphisms, meaning they are supposed to map declarations in one theory to corresponding declara- tions in another theory in a truth-preserving manner, and most of the existing services offered by OMDoc/MMT are based on this assumption. While framings (possibly support relations) should be easily representable as theory morphisms, the same is not true for attacks, undercuts and related “negative” relations. We want to extend the OMDoc/MMT format and the MMT system by new kinds of arrows in a theory graph, that can correctly specify the behaviour of these relations. Since OMDoc/MMT is highly extensible by design, we believe that we can handle these negational relations in a similar manner as the already present theory morphisms. In particular, structural features have recently been added to the OMDoc/MMT system (see e.g. [Ian17]), which allow for adding new syntactical constructs that can be elaborated automatically into the symbols used by the abstract OM- Doc/MMT language. In particular, these could induce arrows in a theory graph that do not correspond to the currently implemented theory morphism. Con- sequently, we can probably represent all the relations between arguments and argumentation contexts as structural features in OMDoc/MMT. Representing argumentations as theory graphs has the additional advan- tage, that we can use theory graph operations, such as theory intersections (see [MK15]) or “theory difference” to identify the common ground and refactoring the corresponding theories yielding a theory graph as in Figure 3. 4.2 Framing in Arguments Often, agents do not pick up on arguments of others directly, but via “framing” (see e.g. [SRWB86] for a discussion). In a nutshell, framing means that a concept mapping between argumentation/knowledge contexts (a frame) is established and the facts and assumptions underlying the argument are mapped along the 8 frame. This happens often in counter-arguments by framing the original argu- ment in terms of an obviously wrong argument, as in the following example2 : – The 1973 Roe vs. Wade decision denied fetus’ rights on the basis of personhood. – The 1857 Dred Scott decision denied Black Americans rights on the basis of personhood. – Personhood for Black Americans has been denied purely on the basis of cultural consensus. – Therefore the denial of personhood for fetuses could also be purely on the basis of cultural consensus. Here, the argument that abortion should be legal because of a court decision is reframed in terms of a similar court decision regarding African Americans, and the invalidity of the latter case is used to infer the invalidity of the former. We could express this in terms of a views by the (pseudo-)formalization in Figure 4. Building on a common ground CG that persons do not have rights, the invalidity of Arg2 can be transfered to ϕ(Arg2) = Arg1. ϕ : {DredScott1857 = RoevsWade1973, black = fetus} Arg1 { Arg2 { RoevsWade1973 : Court Decision DredScott1857 : Court Decision P1 : RoevsWade1973 ⇒ ¬ Person(fetus) P1 : DredScott1857 ⇒ ¬ Person(black) Conclusion : ¬ Rights(fetus)} Conclusion : ¬ Rights(black)} CG {P2 : ∀x.¬ Person(x) ⇒ ¬ Rights(x)} Fig. 4. A Theory Graph with a view that encodes the framing of an argument Another example are the terms pro-life and pro-choice, where proponents on both sides of the debate (on abortion) try to frame their positions in a positive light by framing them in terms of a universally desired property (a right to life vs. a right to choose). 5 Conclusion We have presented a novel way of combining commons-sense (robust) logical systems with context management to obtain argumentation frameworks. We combine two facilities of the OMDoc/MMT framework for this: representation of logics in meta-logical frameworks and context management in theory graphs. We have shown that the approach can account for important features like framing in argumentations, and conjecture that other features like analogical 2 Adapted from www.truthmapping.com/map/647/ 9 transfer also works. The next step is to scale and evaluate the approach to more examples. Acknowledgments The author acknowledges financial support from the German Research Foundation (DFG) under grant KO 2428/18 and fruitful discussions with the Dennis Müller. References [AL] ALMANAC: Argumentation Logics Manager & Argument Context Graph. Project Home Page. url: http://kwarc.info/projects/ almanac/ (visited on 06/17/2018). [BH05] Philippe Besnard and Anthony Hunter. “Practical First-order Ar- gumenation”. In: MIT Press, 2005, pp. 590–595. [BH06] Philippe Besnard and Anthony Hunter. “Knowledgebase compila- tion for efficient logical argumentation”. In: KR. Ed. by Patrick Doherty, John Mylopoulos, and Christopher A. Welty. AAAI Press, 2006, pp. 123–133. [BH08] Philippe Besnard and Anthony Hunter. Elements of Argumentation. MIT Press, 2008. [Bre+13] Gerhard Brewka et al. “Abstract Dialectical Frameworks Revis- ited”. In: Proceedings of the Twenty-Third International Joint Con- ference on Artificial Intelligence (IJCAI). Beijing, China: AAAI Press, 2013, pp. 803–809. url: http://dl.acm.org/citation. cfm?id=2540128.2540245. [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. [CT16] Robert Craven and Francesca Toni. “Argument Graphs and Assumption- based Argumentation”. In: Artif. Intell. 233.C (Apr. 2016), pp. 1– 59. doi: 10.1016/j.artint.2015.12.004. [Dun95] P.M. Dung. “On the Acceptability of Arguments and its Funda- mental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games”. In: Artificial Intelligence 77.2 (1995), pp. 321– 358. [Gen35] Gerhard Gentzen. “Untersuchungen über das logische Schließen I & II”. In: Mathematische Zeitschrift 39 (1935), pp. 176–210, 572–595. [GG84] Dov Gabbay and F. Guenthner, eds. Handbook of Philosophical Logic. D. Reidel, 1984. [GS90] Jeroen Groenendijk and Martin Stokhof. “Dynamic Montague Gram- mar”. In: Papers from the Second Symposium on Logic and Lan- guage. Ed. by L. Kálmán and L. Pólos. Akadémiai Kiadó, Budapest, 1990, pp. 3–48. 10 [GS91] Jeroen Groenendijk and Martin Stokhof. “Dynamic Predicate Logic”. In: Linguistics & Philosophy 14 (1991), pp. 39–100. [Hun07] Anthony Hunter. “Real Arguments Are Approximate Arguments”. In: Proceedings of the 22Nd National Conference on Artificial Intel- ligence - Volume 1. AAAI’07. Vancouver, British Columbia, Canada: AAAI Press, 2007, pp. 66–71. url: http://dl.acm.org/citation. cfm?id=1619645.1619657. [Ian17] Mihnea Iancu. “Towards Flexiformal Mathematics”. PhD thesis. Bremen, Germany: Jacobs University, 2017. url: https://opus. jacobs-university.de/frontdoor/index/index/docId/721. [JHHC15] Naeem Khalid Janjua, Omar Khadeer Hussain, Farookh Khadeer Hussain, and Elizabeth Chang. “Philosophical and Logic-Based Argumentation- Driven Reasoning Approaches and their Realization on the WWW: A Survey”. In: The Computer Journal 58.9 (2015), pp. 1967–1999. doi: 10.1093/comjnl/bxu057. eprint: http://comjnl.oxfordjournals. org/content/58/9/1967.full.pdf+html. [KKP96] Michael Kohlhase, Susanna Kuschert, and Manfred Pinkal. “A type- theoretic semantics for λ-DRT”. In: Proceedings of the 10th Ams- terdam Colloquium. Ed. by P. Dekker and M. Stokhof. ILLC. Am- sterdam, 1996, pp. 479–498. url: http://kwarc.info/kohlhase/ papers/amscoll95.pdf. [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. [Koh13] Michael Kohlhase. “The Flexiformalist Manifesto”. In: 14th Inter- national Workshop on Symbolic and Numeric Algorithms for Sci- entific Computing (SYNASC 2012). Ed. by Andrei Voronkov et al. Timisoara, Romania: IEEE Press, 2013, pp. 30–36. url: http:// kwarc.info/kohlhase/papers/synasc13.pdf. [KR16] Michael Kohlhase and Florian Rabe. “QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge”. In: Jour- nal of Formalized Reasoning 9.1 (2016), pp. 201–234. url: http: //jfr.unibo.it/article/download/4570/5733. [KR93] Hans Kamp and Uwe Reyle. From Discourse to Logic: Introduction to Model-Theoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory. Dordrecht: Kluwer, 1993. [Mai16] Jean-Guy Mailly. “Using Enthymemes to Fill the Gap between Logi- cal Argumentation and Revision of Abstract Argumentation Frame- works”. In: CoRR abs/1603.08789 (2016). url: http : / / arxiv . org/abs/1603.08789. [MK15] Dennis Müller and Michael Kohlhase. “Understanding Mathemat- ical Theory Formation via Theory Intersections in MMT”. 2015. url: http : / / cicm - conference . org / 2015 / fm4m / FMM _ 2015 _ paper_2.pdf. 11 [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. [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). [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. [SRWB86] David A. Snow, E. Burke Rochford, Steven K. Worden, and Robert D. Benford. “Frame alignment processes, micromobilization, and movement participation”. In: American Sociological Review 51.4 (1986), pp. 464–481. 12