56 Rapp et al. / Context Graphs for Legal Reasoning and Argumentation Context Graphs for Legal Reasoning and Argumentation Max RAPP a , Axel ADRIAN a and Michael KOHLHASE a a FAU Erlangen-Nürnberg Abstract. We propose a new, structured, logic-based framework for legal reason- ing and argumentation: Instead of using a single, unstructured meaning space, the- ory graphs organize knowledge and inference into collections of modular meaning spaces organized by inheritance and interpretation. Context graphs extend theory graphs by attack relations and interpret theories as knowledge contexts of agents in argumentation. We introduce the context graph paradigm by modeling the well- studied case Popov v. Hayashi, concentrating on the role of analogical reasoning in context graphs. Keywords. Legal Argumentation, Theory Graphs, Reasoning with Legal Cases 1. Introduction There is a huge literature in legal theory regarding the methods of jurisprudence; see e.g. [Ash17,Blu03,Har12,Mac78]. But there is no consensus on how legal thinking actually works or should work in detail. One area of dissent is between rule-based and analogical reasoning when discussing precedent in case law systems [Ste18]. However, it seems all approaches structurally combine the legal rule of a case – especially of a leading case – and the legally important facts of the present case [Adr09, p. 879]. This structural combination of laws and facts can be represented in formal systems as a logical syllogism: for each case to be decided it has to be checked in detail whether the legally relevant facts can be “subsumed” under the conditions of an applicable legal rule. See e.g. [Mac78, p. 19ff, 229ff], [Har12, p. 124ff], or [Adr09, p. 777ff] for a discussion. This is sometimes [Eng97, p.23ff] seen as establishing the analogical equivalence of the present case and a legally relevant precedent. Contribution We propose to capture these analogical modes of reasoning in a new, structured, logic-based framework for legal reasoning and argumentation: context graphs. These structure legal and world knowledge into theories, which are organized into a strongly interconnected graph by inheritance, interpretation, and argumentation relations. This graph structure drives knowledge processing and argumentation. Overview Section 2 reviews the relevant state of the art in legal reasoning. Section 3 introduces the context graphs framework and applies it to the Popov v. Hayashi case. Section 4 shows rule and precedence case application in the case and Section 5 discusses the fine points of analogical transfer in these applications. Section 6 concludes the paper. Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). Rapp et al. / Context Graphs for Legal Reasoning and Argumentation 57 Acknowledgements The work presented in this paper was supported by the DFG SPP 1999 RATIO (Rational Argumentation Machines) under Grant KO 2428/18. 2. State of the Art in Modelling Legal Reasoning with Cases Capturing and automating how law practitioners reason with cases has been a major focus in legal AI since the HYPO [Ash90] and CATO [Ale97] systems of the late 80s and early 90s. There are two main approaches in modelling legal reasoning with cases: rule-based and analogy-based reasoning [Ste18,ABC19]. In analogical approach the similarity of cases is assessed based on aspects. That is, dimensions of cases that range from maximally pro-defendant to maximally pro-plaintiff and boolean factors that pertain either to the defendant or to the plaintiff. Conflicting arguments for different possible precedent applications are then constructed based on the degree to which cases resemble each other in terms of their aspects [BC12,ABC19]. The main implementations of the analogical approach are the HYPO [Ash90] and CATO systems [Ale97]. In the rule-based approach, precedents are taken to extend the existing body of law by their respective “rule of the case” which is encoded as a defeasible in- ference rule in the object language of some logic (e.g. [Pra12]). Defeasibility is estab- lished through attacks (undercuts, rebuttals) and preference ordering over rules. The most important systems include ASPIC+ [PM14,Pra12] and abstract dialectical frameworks (ADFs) in conjunction with the ANGELIC methodology [AA16]. In recent years, rule-based approaches have proven to be easier to operationalize: they mostly require checking correctness of rule application. Another advantage of rule- based approaches is that they allow to systematically treat the burden of proof and differ- ent proof standards by using default reasoning and prioritisation of rules, respectively. However, [Ste18] argues that the analogy-account for legal reasoning is preferable as it better accounts for judicial discretion and as a heuristic to find applicable precedents or reasons to distinguish a case – especially for novel cases. [ABC19] concur with this analysis but conclude that computational models for analogical reasoning are unlikely: they would require huge ontologies marred by the problem of subjectivity and the im- possibility to choose between competing ontologies of the same set of facts. They do however see potential for analogy-based tools for training law-students through ex-post analysis and assisting law-practitioners in constructing ontologies for novel cases piece- meal (see e.g. [Ash09]). Thus we believe that checking the internal coherence of analogi- cal reasoning, automating some of its aspects and guiding practitioners through heuristic detection of analogy candidates is feasible. See Sections 4 and 5 for a discussion. 3. Formalizing the Law in Context Graphs In the rule-based approach legal reasoning is represented as inference in logical calculi. To this end classical logical calculi are extended by defeasible inference rules or default assumptions in various rule-based or assumption-based argumentation frameworks – e.g. ASPIC+ [PM14]or ABA [ČFST17]. In this paper, we adopt this practice, but introduce an important novel feature: in- stead of using a single, unstructured meaning space, we organize the knowledge, infer- 58 Rapp et al. / Context Graphs for Legal Reasoning and Argumentation ence and argumentation into collections of meaning spaces we call theories or contexts when taking argumentation into account. Importantly, theories are not independent, but are connected by inheritance and interpretation morphisms, forming theory graphs. This enables us to combine rule-based and analogical reasoning through theory morphisms. For argumentation, these morphisms can be used to define conflict relations like attack. Theory/Context Graphs in MMT For concrete representation of the theory graphs we use the MMT (Meta Meta Theories) format [RK13].It models formal objects and state- ments using logical frameworks, in particular the judgments-as-types paradigm. Formally, theories are sets of object declarations and definitions as well as state- ments (axioms and theorems). Theory graphs are diagrams in the categories of theories and morphisms. The former allows for fine-grained specifications of the semantics of individual objects, and the latter allows for inducing and translating knowledge across theories. The possible morphisms in MMT are inclusions, which import all declarations from the domain to the co-domain, structures, which are like includes but copy and trans- late all declarations, views, which are semantics-preserving translations from domain to codomain, and the meta-theory-relation, which behaves like an include for most pur- poses. We refer the reader to [RK13] for the general theory of theory graphs and [KR19] for the idea of context graphs; we will introduce the features that are relevant to legal reasoning using the examples as we go along. The meta-theory re- Gray’s Rule Default Rule McCarthy’s Rule lation links a logical Gray-Rule Default-Rule McCarthy-Rule framework to the logics defined in it, thus for- malizing the “logics-as- Gray-Cond Default-Cond McCarthy-Cond theories” approach, which allows us to represent log- KvC-Lexicon MvS-Lexicon ics and (legal) inference World systems together with the Knowledge domains in the MMT sys- KvC-Aspects + MvS-Aspects tem. This is an integral Legal part of the utility of the Foundation KvC-Rule MvS-Rule MMT system for our ap- proach, but we will gloss PvH-Lexicon PvH-Facts over this aspect in this pa- per, concentrating on the Figure 1.: Popov v. Hayashi as a Context Graph domain-level structure of legal reasoning and argu- mentation. The OMDoc/MMT language is implemented in the MMT system (Meta Meta Toolset; see [MMT]), which provides an API for the language constructs at all levels and provides both logical services such as type reconstruction and rewriting and knowledge management services such as IDE and HTML presentation and browsing of libraries. Running Example: Popov vs. Hayashi We will use the seminal case “Popov vs. Hayashi”[Atk12] – reduced to the salient argumentative backbone – as a running exam- ple in this paper. The full MMT formalization of the example is available at [PvH20]. Rapp et al. / Context Graphs for Legal Reasoning and Argumentation 59 The black part in Figure 1 shows a theory graph of legal knowledge. In the center we have a background “theory” of general legal and world knowledge, which we pre- suppose here. (In reality, this is – of course – a large, modular theory graph, which is shared and selectively imported by particular formalizations.) Clustered around this are formalizations of particular legal knowledge: various precedents and legal rules, which are theory graphs on their own (see Figure 3) and inherit from the background theory via inclusion morphisms ( in the diagrams in this paper). Let us now consider the advantages of a modular theory graph over a representation as an (unstructured) collection of formulae: The first division we can encode concerns the sources from which the text draws. In Fig. 1 the sources are represented in a context graph. Typically the distinction is threefold in case law applications: • Precedents: A collection of already decided cases. Their opinions give concrete descriptions of the aspects that contributed to the ratio of the decision. A rule es- tablished by a precedent x is called a rule of x. Fig. 1 contains two precedents cited in Popov v. Hayashi grouped in green/blue: Keron v. Cashman and Metropolitan Life Insurance Company v. San Francisco Bank. • Rules: Some rules are laid down in an abstract form, for example in legal com- mentary. In Fig. 1 the rule subgraph (grouped in red) contains Gray’s rule which Judge McCarthy adopted; a default rule (cf. Section 5); and the rule of Popov v. Hayashi fashioned by Judge McCarthy himself. • Facts: These are the facts of the case at hand. In Fig. 1 they are grouped in cyan. We assume the facts to be settled. The problem of evidence valuation could potentially be addressed with similar methods as we propose here - however we leave this to future work. Note that all of these include the world/legal background, and thus the various groups overlap in that. The shared background makes the formalizations coherent. In formalization practice this means that all shared or shareable knowledge needs to move into the background. The subsumption task the court faces is to establish that the Popov v. Hayashi facts instantiate the aspects of Keron v. Cashman allowing the application of its rule. To this end, the facts of Popov v. Hayashi have to be shown to be analogous to the legally relevant aspects of Keron v. Cashman with the help of information from the other subgraphs. Objects, Statements, and Proofs in MMT Before we can take a look at the contents of the theories shown above, we have to discuss the representation of objects and statements. In MMT we can formalize then as dec- larations of the form name : type = definiens where name is the object name, (optionally) type its type, Figure 2.: An MMT Theory and (again optionally) definiens can be used to define the object. Figure 2 shows a snippet of our formalization in MMT surface syntax – we will use a slightly simplified version of that in the theory graph diagrams below. The theory PvH- Lexicon contains an inclusion of the theory background – the ? is the syntactic indicator 60 Rapp et al. / Context Graphs for Legal Reasoning and Argumentation for theory names – and three object declarations: the key contributors to our example case. The coloured rectangles are MMT delimiters of various levels. In the judgments-as-types paradigm MMT employs, we can formalize statements in the same way. The main trick is to introduce a type constructor `, which – given a proposition ϕ – constructs the type ` ϕ of all proofs of ϕ. If ` ϕ is non-empty, then ϕ has a proof, and thus ϕ is a theorem. Thus a declaration c : ` ϕ which declares a constant c of type ` ϕ entails that ` ϕ is non-empty, and can be seen as an axiom. Note that this trick also allows us to formalize inference rules in a calculus, e.g. the conjunction elimination ∧E rule of the natural deduction calculus as a function ` ϕ ∧ ψ → ` ϕ → ` ψ. With such rules (and axioms like c above) proofs become terms MMT and theorems become declarations, e.g. pf :` ϕ = ∧E c c which defines a constant pf of type ` ϕ by the proof ∧E c c from the axiom c : ` ϕ discussed above (used twice). We will use a meta-theory FOLND formalizing first-order logic and its natural de- duction calculus which introduces the constants →, `, ∧, ¬, ∀, etc. in the rest of the paper. All the theory/context graph diagrams should include a node for this theory with a meta link to all other theories, but we omit these for simplicity. In Section 5 we will discuss context graphs for argumentation. There we graduate to graphs that include argumentation relations as special morphisms and a meta-theory for defeasible aspects of legal reasoning. Formalizing Precedents, Rules and Facts Rules map sets of legal conditions to sets of legal consequences. One could capture this characteristic of rules at the object-language level as is done in rule based argumentation approaches. However to enable analogical reasoning we opt for a theory-graph-based approach to rules. We regard the legal condi- tions and consequences as separate theories connected by a theory morphism. Given a meta-theory, for a formalization of a rule we thus need 1. a legal lexicon of constants specifying the concepts in the rule; 2. a theory of legal conditions specifying when the norm applies; 3. a theory of legal consequences specifying what follows from the rule application. Figure 3 shows a rule formalization in three theories for the three concerns listed above. General concepts such as the types “lperson” and “thing” are inherited from the background knowledge. The lexicon contains the concepts that are to be defined in the rule. In this case, the predicates “takes steps”, “is interrupted” and their conjunction “stint”. Condition theories declare a set of conditions necessary for the application of the rule. E.g. McCarthy’s rule as depicted in Fig. 3 requires an actor and an object and has the condition-axiom cond stint requiring that the actor takes steps to take possession of the object and is interrupted. Note that this is similar to approaches using abstract dialectical frameworks [AA16]. We leave an exploration this connection to future work. Finally, the theory “McCart-Rule” contains three declarations: a proposition to which the rule pertains; an object language version of the rule itself; and finally the legal consequences of the rule application. While the rule is declared axiomatically, the legal consequences come with a derivation from the condition axioms and the rule axiom. In Section 4 we will see how this enables us to “inject” an instantiation of the rule as well as a proof of the legal consequences into the present case where it can then be shared and translated across theories. Formalization of precedents is very similar to formalization of rules. The main dif- ference is that in precedent graphs conditions are replaced by aspects – not all of which may be necessary conditions for application of the rules that the precedent establishes. Rapp et al. / Context Graphs for Legal Reasoning and Argumentation 61 McCart-Lexicon takes steps: lperson → thing → bool is interrupted : lperson → bool stint : lperson → thing → bool McCart-Conditions = [x,y] x takes steps y is interrupted x actor : lperson object : thing cond stint : ` actor stint object McCart-Rule McCart proposition = actor has claim object McCart rule : ` actor stint object ⇒ actor has claim object McCart cons : ` actor has claim object = MP McCart rule cond stint Figure 3. A rule graph for the rule judge McCarthy introduces in his opinion. Finally, in the present case, it is not apparent yet which facts of the case will be legally relevant and become aspects. Thus in a present case graph the legal conditions theory is replaced with a theory describing the case’s facts. 4. Precedent/Rule Application via Views and Pushouts We have seen the basic “object-oriented” infrastructure of theory graphs above and how legal knowledge representation can profit from modularity. But for legal reasoning we utilize an advanced feature of MMT: views and pushouts. In this section we use them to combine modularity and inference to model analogical reasoning. Gray-Cond PvH-Facts McCart-Cond Gray-Rule Default-Cond PvH-Asp-Gray Fig. 7 McCart-Rule Default-Rule PvH-Asp-McCart PvH-Asp-Default KvC-Aspects MvS-Aspects Fig. 8 Fig. 6 KvC-Rule PvH-Ruling PvH-Alt MvS-Rule Figure 4. Generating McCarthy’s and an alternative Ruling from Legal Theories (see Figure 4). The Running Example continued Fig. 4 depicts an extension of the formalization of Popov v. Hayashi from Fig. 1 using analogical reasoning. The black part is that of Fig. 1, but the blue part is generated via pushouts (rectangular subgraphs identified by the pushout marker ) that correspond to rule/precedent application (see Fig. 5 and the discussion there). Fig. 4 contains the backbone of the argumentation of the Popov v. Hayashi ruling – leaving out many details that go beyond introducing the context graph paradigm and thus the scope of this paper. It starts with the established facts (in the theory PvH-Facts) and applies Gray’s rule to establish that Popov did not obtain possession of the baseball 62 Rapp et al. / Context Graphs for Legal Reasoning and Argumentation (and Hayashi did) in PvH-Aspects-Gray. From there, McCarthy would have to apply the “default rule”: unless there is a “proof” that Popov has possession of the ball we have to assume that he does not. Subsequently the precedent Metropolitan Life Insurance Company v. San Francisco Bank (theories MvS-*)applies to obtain the ruling that Popov has no claim to the ball (PvH-Alt; we abstract away from the discussion of “conversion”). However he distinguishes the case and instead, introduces a new rule (cf. Fig. 3) which applied to PvH-Aspects-Gray allows him to derive the required proof that Popov has a (qualified) right to possess the ball (theory PvH-Asp-McCart). Finally, this enables him to apply the precedent Keron v. Cashman (KvC-*) ruling that ownership of the ball is to be split between Popov and Hayashi (theory PvH-Ruling). Note that Judge McCarthy’s ruling PvH-Ruling contradicts and defeats the default ruling PvH-Alt as indicated by the red attack relations. The three rectangular patterns marked by “ Fig. n” in Fig. 4 warrant a closer look, we will discuss them in detail below, after we introduce the general principles of views and pushouts in MMT. ϕ Views Given theories S and T , a view S T states that T is more specific than S after applying the translation ϕ from all symbols of S to T -expressions. Views have a range of intuitive readings: In mathematics, where the notion originates, views are used to formalize examples, interpretation, and even the model relation. In computer science we can use views to formalize specification refinements and the implementation relations. In this paper we use it for analogy: S and T are instances of the same (possibly unknown) theory G and ϕ an analogy between S and T . Pushouts The category T of theories and theory morphisms admits colimits and thus pushouts – a special colimit: Given a theory A with two morphisms A B and ψ : A C, the pushout of A and B (along ψ) is the “minimal” theory P that combines B and C identifying material from A. Precedent Application can be viewed Rule Conditions Rule Consequences as an instance of analogical reasoning in case law and can thus be formal- Application ized as a pushout. The precedent and the present case are construed as instances of Present Case Facts Ruling the same abstract rule established by the precedent. Applying a precedent Prec to Figure 5.: Application of a rule a present case Pres corresponds to con- structing a view ϕ from the legal conditions of a rule established in Prec to the facts of Pres. In essence, pushouts can be interpreted as a meta-language Modus Ponens rule: we can apply the “rule” A B to C if C can be interpreted (i.e. connected with a view) as more specific than A. The pushout P is the result of the “rule application”. Figure 5 on the right shows the general pattern; it underlies all of the pushouts in Fig. 4 – with refinements that we discuss below. Crucially, the MMT system can compute pushouts: the information in A, B, C, and ϕ fully determines all declarations in P [CMR17]; in particular, all names can be generated. This is the basis for the generated (blue) theories in Figure Fig. 4. A detailed example is provided by Fig. 6: here the theory PvH-Aspects-Default is subsumed under the rule established by Metropolitan Life Insurance Company v. San Francisco Bank through the Rapp et al. / Context Graphs for Legal Reasoning and Argumentation 63 view precedent application. The pushout corresponds to the rule application and creates the ruling: ` ¬Popov has claim ball). 5. Operationalizing Analogical Reasoning in Context Graphs In the pushout model of rule-application in the last section, views operationalize “ana- logical transfer”, but the legal literature has identified some additional requirements. In this section we show how these can be modeled. Analogical Reasoning [Ste18] establishes a list of critical questions to analogical rea- soning and [ABC19] remarks on the difficulty of operationalizing them for a computa- tional model. Table 1 shows our proposed operationalization of each of these questions. We will discuss the first three using the Popov v. Hayashi example. We conjecture that A4 can be handled by considering values (as is done e.g. in [BCS03]) in addition to rules and prececents but we leave this to future work. A1 Are A and B similar in a legally relevant Is there a partial view ϕ from the present case A to way? a suitable formalization of the precedent B? A2 Can a successful mapping be made to an Does ϕ’s image in B include all the conditions for aspect of the present-case for every aspect the application of a/the rule of B of the precedent-case that the opinion high- lights enough to indicate that it is part of the ratio in the opinion? A3 Does the surrounding law allow present-case Is there any unjustified default in the interpretation and precedent-case to be mapped success- of the present case? Does another precedent attack fully? and defeat the currently considered precedent? A4 Are there no legally relevant differences be- Is ϕ −1 onto A? If not, is there an A-declaration a tween A and B? outside ϕ −1 (ϕ(B)) such that a is viewed by an im- portant legal principle. Table 1. Analogical Reasoning according to the Literature A1: Identifying legally relevant similarities The first problem in constructing a prece- dent application consists in identifying which aspects (if any) of the precedent are legally relevant to the present case. This can be done by viewing the precedent from the perspec- tive of the present case [Ste18]. We can understand this process in a conservative and constructive way. Under the conservative interpretation, it corresponds to the fact that views map to expressions. In this way, views expose new (derivable) aspects of an already given formalization of the precedent that have not been explicitly declared. Here, a little logical clarification is in order: consider the precedent application view ϕ in Fig. 6. By the theory morphism property, it has to map every constant without definition to an expression in PvH-Asp-Default. The interesting case is the last: in MvS- Aspects Aspect is an axiom of type ` A1 ∧ A2 ∧ A3, so it must be mapped to an (proof)- expression of type ` notitle ∧ noright ∧ nopos, we call this a proof obligation of ϕ. This obligation is fulfilled by the proof term ϕ(Aspect) = Π. Under the constructive interpretation, the precedent’s formalization itself is to be guided by the present case. This can be done through a special definitorial variant of a view – called structure in MMT – where we import, rename and define content from 64 Rapp et al. / Context Graphs for Legal Reasoning and Argumentation PvH-Asp-Default Popov : lperson MvS-Aspects ball : thing notitle = ¬ Popov has title ball relevance-Reduct noright = ¬ Popov has right ball InsCorp: lperson nopos = ¬ Popov posess ball relevance money : thing notitle df : p∼ notitle A1 = ¬ InsCorp has title money noright df : p∼ noright A2 = ¬ InsCorp has right money nopos thm: : ` nopos ϕ: precedent application A3 = ¬ InsCorp posess money = MP gray rule (∧Er Fact2)  Aspect : ` A1 ∧ A2 ∧ A3 Π =∧I (aid notitle df)  InsCorp 7→ Popov include ?relevance-Reduct (aid noright df) nopos thm ϕ= money 7→ ball  Aspect 7→ Π check : thing Hayashi : lperson bank : lperson Fact1 : ` Hayashi has control ball ∧ Hayashi has intent ball PvH-Alt MvS-Rule proposition = Popov has claim ball proposition = InsCorp has claim money rule = ` notitle ∧ noright ∧ nopos ⇒ ¬ proposition rule : Aspect ⇒ ¬ proposition ruling : ` ¬ proposition = MP rule Π ruling : ` ¬ proposition = MP rule Aspect Figure 6. Identifying legally relevant aspects of Metropolitan Life Insurance Company v. San Francisco Bank. the present case. This then serves as the starting point for a full formalization of the precedent. Here we will focus on the conservative interpretation. In both cases, formally we have to ensure that there is a (partial) view from the present case’s facts to the precedent case’s aspects. As we are usually only interested in capturing part of the present case, this view will usually not be total. E.g. deciding whether Popov has a claim to the ball or not as in Fig. 6 does not require us to map facts pertaining to Hayashi. Fig. 6 shows how the precedent Metropolitan Life Insurance Company v. San Fran- cisco Bank which Judge McCarthy used to assess whether Popov can sue for conver- sion is viewed (conservatively) in light of the facts of Popov v. Hayashi. In Metropolitan Life Insurance Company v. San Francisco Bank an insurance company sued a bank over the “conversion” of checks issued to non-existing persons by a fraudulent employee and money that had been paid out on receipt of these checks. The court ruled that the money could not have been converted based on the precedent that depositors have no claim to specific assets in a bank. In becoming a leading case, the “rule of the case” abstracted from this is that “someone who has no title, possession or right to possession of an object cannot sue for conversion of that object”[Atk12, p.6]. Judge McCarthy is interested in applying this rule to Popov’s situation. Under the default assumption (cf. Section 5) that Popov has no right to possession of the ball, the mapping is onto the application condi- tions of the rule established by Metropolitan Life Insurance Company v. San Francisco Bank. In this way the mapping separates the presently legally relevant aspects from the irrelevant ones (everything concerning the checks, the relationship between the money and the checks, the differences between money and baseballs, etc.). A2: Totality of Precedent Application Next we need to check whether the precedent is applicable. This is the case if the reduct of the precedent induced by the present case meets all the application conditions of a rule of the precedent case - as obtains in Fig. 6. There the partial view relevance carves out a reduct of Metropolitan Life Insurance Com- pany v. San Francisco Bank that suffices to apply the case’s rule. This implies that by Rapp et al. / Context Graphs for Legal Reasoning and Argumentation 65 inverting relevance we get a total view precedent application that allows to map the rule conditions to the present case - thereby enabling rule application via pushout. However, even partial views from precedents may be useful in the act of distinguish- ing and with theory construction in “hard” cases. The greater the proportion of the prece- dent that can be mapped, the higher should it be regarded as a candidate for a theory con- struction starting point. In addition, partial views can serve as heuristics to find complete ones. MMT is already equipped with a view finder system that can find simple total and partial views. This may help practitioners in finding precedent candidates quickly. A3: Defaults and Defeasibility A precedent application is binding if ϕ covers all “legally relevant” aspects of B. Else the court may be justified to distinguish B from A, that is defeat the application of A to B either by finding a better precedent A0 or by setting a precedent itself by adopting a new rule (or, as we see in the next example, both). Thus analogical precedent application – just as the application of legal rules – is defeasible. On the other hand some rules apply by default if the burden of proof of no other applica- ble rule can be met. The paradigmatic example is the principle “innocent unless proven guilty”. Defaults and defeasibility can be implemented in context graphs through MMT’s derived modules. For example, in [KR19] we implemented ABA in this way. Here we combine this approach with analogical reasoning. Default Reasoning Default reasoning is one of the most important defeasible modes of inference in legal reasoning. The defeasibility of defaults arises from two circumstances: the proof search may not have been exhaustive or new information or rules may have been added to the knowledge base that render formerly unprovable statements provable. Both situations arise in the law: the first corresponds to a relevant rule from the surrounding law having been ignored; the second arises when new evidence comes to light or a court decides to fashion a new rule. The latter is what happened in Popov v. Hayashi. Following our approach in [KR19] we model the default reasoning in Popov v. Hayashi by instantiating ABA. To this end we enrich our metalanguage with an assump- tion operator p∼: bool −→ type and a strict inference rule aid : {x : bool} p∼ x −→` x. Default-Cond Prop 7→ Popov has right ball PvH-Asp-Gray Prop : bool ... PvH-Facts Default-Rule PvH-Asp-Default proposition = Prop noright df : p∼ ¬ Popov has right ball default : p∼ ¬ Prop ... Figure 7. Inference by default: If Popov’s right to possession cannot be proven, it is assumed that he has none. Fig. 7 shows the situation in which Judge McCarthy finds himself after having in- ferred via Gray’s rule that Popov does not have possession of the ball. Since he obvi- ously does not have a title (this default is left implicit in the opinion), it remains to check whether he has a right to possession. In the absence of an applicable rule establishing a right to possession for Popov, it remains to apply the default rule to infer that he has no such right. Note that the default rule’s only condition is that the input variable be a proposition and it creates an assumption indicated by p∼. Hence anything can be assumed 66 Rapp et al. / Context Graphs for Legal Reasoning and Argumentation by default and together with the rule aid we may get inconsistent theories. However, this is unproblematic as such theories are self-attacking (cf. Fig. 8). Defeasibility In Popov v. Hayashi Judge McCarthy was unhappy with this default out- come and instead decided to fashion a new rule. McCarthy’s rule views PvH-Asp-Gray and via pushout establishes Popov’s claim to the ball based on his interrupted efforts to catch it. This new situation now matches the precedent Keron v. Cashman which he ap- plies. However, his ruling is now in conflict with the default ruling. How can this conflict be resolved? PvH-Aspects-McCart PvH-Aspects-Default Popov right : ` Popov has right ball df-noright : p∼ ¬ Popov has right ball = MP McCarthy-Rule (∧Er Fact2) ... ... Def. Defeater Kernel Assumption Proof : ` Prop Prop: bool Ass : p∼ ¬ Prop PvH-Alt PvH-Ruling PvH proposition = Popov has claim Ball PvH proposition = Popov has claim Ball PvH rule: ` notitle ∧ noright ∧ nopos ⇒ PvH rule = Popov has right Ball ⇒ ¬ PvH proposition Popov has claim Ball PvH ruling: ` ¬ Popov has claim Ball PvH ruling: ` PvH proposition = MP PvH rule (∧I aid title-df aid = MP Ruling Popov Right right-df nopos-ax) Figure 8. Inheriting an Attack Relation Fig. 8 shows how McCarthy’s rule allows to prove the negation – technically, the ABA contrary – of the default assumption df-noright. In theory graphs, attack can be defined by elaboration into a subgraph(for details see [KR19]). In Fig. 8, the light blue diagram is the elaboration of the red attack arrows: Prop is mapped to PvH proposition in the (ommitted in Fig. 8), Proof to Popov right and Ass to df-noright. This corresponds to the ABA definition of attack according to which a set of assumptions A attacks a set of assumptions B if A allows to derive the contrary (here: negation) of an assumption in B. If we apply one of the usual labelings (admissible grounded, preferred, ideal, . . . ) to the resulting attack graph, PvH Aspects Default is defeated and hence the precedent Metropolitan Life Insurance Company v. San Francisco Bank is distinguished as its con- ditions cannot be mapped into PvH Aspects McCart. 6. Conclusion and Outlook We have modeled the well-known case Popov v. Hayashi in theory/context graphs, a new, structured, logic-based framework for legal reasoning and argumentation. We have shown that the mechanism of pushouts is well-suited to model precedent and rule appli- cation and the views involved can adequately capture the analogical transfer in applica- tion. Crucially, given user-specified views, pushout-based reasoning can be automated. Moreover, the modular structure of theory graphs nicely captures the intuitive structure of world and legal knowledge. In essence, our approach lifts legal reasoning and argu- mentation to the theory level and the graph structure can be used to drive the process. Rapp et al. / Context Graphs for Legal Reasoning and Argumentation 67 This can be used to foster human understanding of complex legal arguments via the theory graph diagrams and can ultimately support legalTech services like subsumption checking, precedence case finding, and even educational applications in the long run. References [AA16] Latifa Mohammed Al-Abdulkarim. A methodology for designing systems to reason with legal cases using abstract dialectical frameworks. Artificial Intelligence and Law, 24(1):1–49, 2016. [ABC19] Katie Atkinson and Trevor Bench-Capon. Reasoning with legal cases: Analogy or rule applica- tion? In Proceedings of the Seventeenth International Conference on Artificial Intelligence and Law, ICAIL ’19, page 12–21, New York, NY, USA, 2019. Association for Computing Machinery. [Adr09] Axel Adrian. Grundprobleme einer juristischen (gemeinschaftsrechtlichen) Methodenlehre. Duncker & Humblot Berlin, 1 edition, 2009. [Ale97] Vincent A. W. M. M. Aleven. Teaching Case-Based Argumentation through a Model and Exam- ples. PhD thesis, University of Pittsburgh, USA, 1997. [Ash90] Kevin D. Ashley. Modeling Legal Argument. Reasoning with Cases and Hypotheticals. Artificial intelligence and legal reasoning. MIT Press, 1990. [Ash09] Kevin Ashley. Ontological requirements for analogical, teleological, and hypothetical legal rea- soning. In Proceedings of the International Conference on Artificial Intelligence and Law, pages 1–10, 01 2009. [Ash17] Kevin Ashley. Artificial Intelligence and legal Analytics. Cambrige University Press, 2017. [Atk12] Katie Atkinson. Introduction to special issue on modelling popov v. hayashi. Artificial Intelligence Law, 20(1):1–14, March 2012. [BC12] Trevor Bench-Capon. Representing popov v hayashi with dimensions and factors. Artificial Intel- ligence and Law, 20(1):15–35, 2012. [BCS03] Trevor Bench-Capon and Giovanni Sartor. A model of legal reasoning with cases incorporating theories and values. Artificial Intelligence, 150(1):97 – 143, 2003. AI and Law. [Blu03] Dieter Blumenwitz. Einführung in das anglo-amerikanische Recht. C.H.Beck, 7 edition, 2003. [ČFST17] Kristijonas Čyras, Xiuyi Fan, Claudia Schulz, and Francesca Toni. Assumption-based argumen- tation: Disputes, explanations, preferences. IFCoLog Journal of Logics and Their Applications, 4(8):2407–2456, 2017. [CMR17] Mihai Codescu, Till Mossakowski, and Florian Rabe. Canonical Selection of Colimits. In Phillip James and Markus Roggenbach, editors, Recent Trends in Algebraic Development Techniques, pages 170–188. Springer, 2017. [Eng97] Karl Engisch. Einführung in das juristische Denken. Kohlhammer, Stuttgart, 9 edition, 1997. [Har12] Herbert Lionel Adolphus Hart. The Concept of Law. Oxford University Press, 3 edition, 2012. [KR19] Michael Kohlhase and Max Rapp. Context graphs for argumentation logics. In Robert Jäschke and Matthias Weidlich, editors, Proceedings of the Conference ”Lernen, Wissen, Daten, Analysen”, LWDA, volume 2454 of CEUR Workshop Proceedings, pages 265–279. CEUR-WS.org, 2019. [Mac78] Neil MacCormick. Legal Reasoning and Legal Theory. Oxford University Press, 1978. [MMT] MMT – language and system for the uniform representation of knowledge. Project web site at https://uniformal.github.io/. [PM14] Henry Prakken and Sanjay Modgil. The ASPIC+ framework for structured argumentation: a tuto- rial. Argument and Computation, 5(1):31–62, 2014. [Pra12] Henry Prakken. Reconstructing Popov v. Hayashi in a framework for argumentation with struc- tured arguments and Dungean semantics. Artificial Intelligence and Law, 20(1):57–82, 2012. [PvH20] Popov v. Hayashi as a context graph. https://gl.mathhub.info/jlogic/pvh, 2020. [RK13] Florian Rabe and Michael Kohlhase. A scalable module system. Information & Computation, 0(230):1–54, 2013. [Ste18] Katharina Stevens. Reasoning by precedent – between rules and analogies. Legal Theory, 24(3):216–254, 2018.