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 representation 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.
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 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 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 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. 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 bring order into the zoo of logic-based approaches to common sense reasoning and argumentation, and systematically extend logics 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
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 arguments 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
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 argumentation 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 extensions.
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 structured 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.
Assumption-based argumentation, a form of structured argumentation extended by “defeasible axioms” (i.e. assumptions), lend themselves to being represented 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 exception 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
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 inference 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 better than / worse than B”. Relevance logic restricts the classical (i.e. material) implication in such a way as to avoid valid implications between seemingly disconnected premises and conclusions, which seems false from a colloquial understanding 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 interpretation/formalization of natural language documents. A paradigmatic language here is Discourse Representation Theory (DRT) [KR93] which introduces “discourse 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 second 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 restricted to that formula. Dynamic logics try to remedy these problems in various ways by changing the behaviour of variables or introducing non-standard quantifiers with “non-recursive” scoping behaviour. Discourse referents also account for many other linguistic phenomena including tense, propositional attitudes, dialogue, 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
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 particular 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 logics 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
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 argumentation 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 ii ) “Context Graphs for Argumentation”, i.e. a logic-independent framework for context management in argumentations based on (domain-level) OMDoc/MMT theory graphs.
We show how these two goals can be obtained on the basis of existing representation formats and knowledge management tools. 3.1
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 [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 several concepts to maximize modularity and to abstract from and mediate between 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 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 OMDoc/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.
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 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.
It is a central advan- translation m tage of the OMDoc/MMT LF LF + X system that theory mor- inclusion phisms “transport axioms, meta-theory FOL m0 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 handling 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 theories [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
The LATIN atlas [Cod+11] is a heterogeneous, highly integrated library of formalizations 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 individual 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 firstorder, common, higher-order, modal, description, and linear logics. Type theoretical 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 relativization 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 translation to HOL and ultimately resulting in the foundations of Mizar, Isabelle/HOL and ZFC, as well as translations between them. The formalization of propositional 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 logicinteroperability 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 argumentation frameworks – also provides an uniform meaning space for logical content and argumentations.
LATIN already already contains some of the robust logics surveyed in Section 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 4.1
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 theories, giving rise to theory graphs as described in Section 3.1 and thus using existing and new tools A ¬A for theory graphs for applying these frameworks in a formal setting. Figure 3 shows a typical situation for agents P and C, which agree on a common CG ground, expressed as the theory graph CG, but differ on some assumption A, which P accepts and C rejects (see also Figure 4 for a real-world example). Fig. 3. Context Graph DL
ML OWL Isabelle/HOL
PL FOL CL
SFOL HOL ZFC
Base ¬ . . .
∧ PL ∧
Syn ∧
Mod ∧
Pf DFOL Mizar
Fig. 2. A Fragment of the LATIN Atlas (from [KR16]) Essentially, if P and C are “internally consistent”, then they accept only the material below the respective 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 Figure 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 knowledgebased context models, where many interesting properties can be read off the graph struture. We conjecture that we can model the attack-like relations in argumentation frameworks (e.g. refute and undercut) as paths in suitably granular theory graph which contain a single “antithesis”-like relation and the supportlike relations as paths without.
Modelling context graphs as theory graphs naturally implies that the relations 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 declarations 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 OMDoc/MMT language. In particular, these could induce arrows in a theory graph that do not correspond to the currently implemented theory morphism. Consequently, 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 advantage, 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
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 frame. This happens often in counter-arguments by framing the original argument 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 {
RoevsWade1973 : Court Decision P1 : RoevsWade1973 ⇒ ¬ Person(fetus) Conclusion : ¬ Rights(fetus)} Arg2 { DredScott1857 : Court Decision P1 : DredScott1857 ⇒ ¬ Person(black)
Conclusion : ¬ Rights(black)}
CG {P2 : ∀x.¬ Person(x) ⇒ ¬ Rights(x)} 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
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/ 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 Mu¨ller. [BH05] [BH06] [BH08] [Bre+13] [Cod+11] [CT16] [Dun95] [Gen35] [GG84] [GS90] [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 Intelligence - 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 ArgumentationDriven 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 typetheoretic semantics for λ-DRT”. In: Proceedings of the 10th Amsterdam Colloquium. Ed. by P. Dekker and M. Stokhof. ILLC. Amsterdam, 1996, pp. 479–498. url: http://kwarc.info/kohlhase/ papers/amscoll95.pdf. [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. [Koh13] Michael Kohlhase. “The Flexiformalist Manifesto”. In: 14th International Workshop on Symbolic and Numeric Algorithms for Scientific 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: Journal 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 Logical Argumentation and Revision of Abstract Argumentation Frameworks”. In: CoRR abs/1603.08789 (2016). url: http : / / arxiv . org/abs/1603.08789. [MK15] Dennis Mu¨ller and Michael Kohlhase. “Understanding Mathematical Theory Formation via Theory Intersections in MMT”. 2015. url: http : / / cicm - conference . org / 2015 / fm4m / FMM _ 2015 _ paper_2.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. [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.