Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). Reifying Default Reasons in Justification Logic? Stipe Pandžić[0000 0002 6812 1437] Department of Theoretical Philosophy, Faculty of Philosophy & Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, Faculty of Science and Engineering University of Groningen, Groningen, The Netherlands s.pandzic@rug.nl Abstract. The main goal of this paper is to argue that justification logic advances the formal study of default reasons. After introducing a variant of justification logic with default reasons, we first show how the logic can be used to model undercutting attacks and exclusionary reasons. Then we compare this logic to Reiter’s default logic interpreted as an argumentation framework. The comparison is done by analyzing di↵erences in the way in which process trees are built for the two logics. Keywords: Justification logic · Default reasons · Defeaters · Formal argumentation · Reiter’s default logic. 1 Introduction In its most general sense, the notion of “reason” can be understood as a sup- port or justification for a conclusion or an action. In reasoning from incomplete information, reasons are usually not strong enough to eliminate any possibility of conflicting reasons, that is, reasons are often only defeasible. A good example is human reasoning with its dedication to identifying undefeated reasons upon which actions and conclusions are to be based. But what are default reasons formally? One notable logical account of defeasible reasoning is Reiter’s default logic [17, 1] with its rules that enable “jumping” to conclusions. The answer to our question in Reiter’s logic is, however, left ambiguous. This problem is identified by Horty in the following passage about the reification of reasons [9, p. 6]: Suppose, as in our example, that the agent’s background theory contains the default B ! F , an instance for Tweety of the general default that birds fly, together with B, the proposition that Tweety is a bird, so that the default is triggered. In this case, it seems plain that the agent has a reason to conclude that Tweety flies. But how, exactly, should this reason be reified? Should it be identified with the default B ! F itself, or with the proposition B? ? Research supported by Ammodo KNAW project Rational Dynamics and Reasoning 59 Horty’s conclusion is that this question “like many questions concerning reifica- tion, is somewhat artificial” and that “when it comes to reification, the reason relation could be projected in either direction, toward defaults or propositions, and the choice is largely arbitrary”. The goal of this paper is to show that the question of reification is important and that giving an answer to it opens up new paths in formalizing defeasible reasoning. In particular, our focus is on showing benefits of formalizing default reasons with the language of justification logic, which is expressive enough to encode the structure of default inferences within its reason terms. The paper has the following structure. The next section introduces the ba- sics of the logic of default justifications first introduced in [12] and developed in [13] as a theory of structured arguments that generalizes (a large subclass of) Dung’s frameworks [7]. Section 3 elaborates on the conceptual di↵erences between Reiter’s logic interpreted as an argumentation framework and our jus- tification logic argumentation theory. We start by showing how to represent exclusionary reasons and undercutting defeat in process trees for justification logic-based default theories. Then we show how to translate undercut into Rei- ter’s default logic by interpreting its default processes as arguments. We argue that our logic conforms better to the idea of making a default inference without having to anticipate numerous exceptions to the inference. 2 Logic of default reasons The logic of default justifications was first presented in [12]. Here, we can only give an overview of the key definitions, starting with the basic justification logic language.1 2.1 Syntax, axioms and rules of JTCS The basic format of justification assertions is “t : F ”, where a justification term “t” is informally interpreted as a reason or justification for “F ”. The set T m consists of all justification terms, constructed from variables x1 , . . . , xn , . . . and proof constants c1 , . . . , cn , . . . by means of operations ‘·’ and ‘+’. The grammar of justification terms is given by the following Backus-Naur form: t ::= x | c | (t · t) | (t + t) where x is a variable denoting an unspecified justification and c is a proof con- stant, taken as atomic within the system. A set of subterms Sub(t) is defined by induction on the construction of a term t. Formulas of JTCS based on the countable set of propositional atoms P formulas are defined by the following Backus-Naur form: F ::= > | P | (F ! F ) | (F _ F ) | (F ^ F ) | ¬F | t : F 1 Justification logic was first characterized as a logic of arithmetic proofs in [2]. For the basic workings of justification logic operators and the relation between justification logic variants see, e.g., [8]. 60 where P 2 P and t 2 T m. The set F m consists of exactly all formulas. We can now define the logic JTCS , which is the weakest logic with “truth inducing” justifications containing axiom schemes for the two basic operations application ‘·’ and sum ‘+’. Informally, application (axiom A1 below) represents the reification of the modus ponens inference as a reason term, while sum (axiom A2 below) enables merging two reason terms to produce a new reason term. These are the axioms and rules of JTCS : A0 All the instances of propositional logic tautologies from F m A1 t : (F ! G) ! (u : F ! (t · u) : G) (Application) A2 t : F ! (t + u) : F ; u : F ! (t + u) : F (Sum) A3 t : F ! F (Factivity) R0 From F and F ! G infer G (Modus ponens) R1 If F is an instance of A0-A3, cn , cn 1 , . . . , c1 proof constants and cn 1 : · · · : c1 : F 2 CS(cn ), then infer cn : cn 1 : · · · : c1 : F (Iterated axiom necessitation), where the function CS(c) assigns formulas to any constant according to the following two conditions: – Axiomatically appropriate: for each axiom instance A, there is a constant c such that A 2 CS(c) and for each formula cn 1 : · · · : c1 : A 2 CS(cn ) such that n 1, there is a constant cn+1 such that cn : cn 1 : · · · : c1 : A 2 CS(cn+1 ); – Injective: each proof constant c justifies at most one formula. The intuition behind the function CS(c) in R1 is that the basic logical axioms are taken to be justified by proof constants and so are the formulas likewise produced. A set of instances of rule R1 is called Constant Specification (CS) set: Definition 1 (Constant specification) CS = {cn : cn 1 : · · · : c1 : F | F is an instance of A0-A3, cn , cn 1 , . . . , c1 are proof constants and n 2 N} We say that the formula F is JTCS -provable (JTCS ` F ) if F can be derived using the axioms A0-A3 and rules R0 and R1. 2.2 Semantics The semantics for JTCS is an adapted version of the semantics for the logic of proofs (LP) given by [11]. The JTCS logic can be proved to be sound and complete with respect to the semantics below. Definition 2 (JTCS model) A function reason assignment based on CS is de- fined as ⇤(·) : T m ! 2F m , mapping each term to a set of formulas from F m. We assume that it satisfies the following conditions: 1.) If F ! G 2 ⇤(t) and F 2 ⇤(u), then G 2 ⇤(t · u), 2.) ⇤(t) [ ⇤(u) ✓ ⇤(t + u) and 3.) If c : F 2 CS, then F 2 ⇤(c). A truth assignment v : P ! {T rue, F alse} is a function assigning truth values to propositional formulas in P. We define the interpretation I as a pair (v, ⇤). For an interpretation I, |= is a truth relation on the set of formulas of JTCS . We say that, for any formula t : F 2 F m, I |= t : F i↵ F 2 ⇤(t). Truth conditions for atomic propositions, ¬, !, ^ and _ are defined as usual. An interpretation I is reflexive i↵ the truth relation for I fulfills the following condition: 61 – For any term t and any formula F , if F 2 ⇤(t), then I |= F . We define the consequence relation of the logic of factive reasons JTCS on re- flexive interpretations in such a way that, for any set of JTCS formulas ⌃: Definition 3 (JTCS consequence relation) ⌃ |= F i↵ for all reflexive in- terpretations I, if I |= B for all B 2 ⌃, then I |= F . For a set of formulas ✓ F m and the JTCS consequence relation |= defined above, a JTCS closure of is given by T hJTCS ( ) = {F | |= F }. For a closure T hJTCS ( ), it holds that CS ✓ T hJTCS ( ). 2.3 Default theories based on the JTCS language Building on the JTCS syntax, we introduce the definition of the default theory: Definition 4 (Default Theory) A default theory T is defined as a pair (W, D), where the set W is a finite set of JTCS formulas and D is a count- able set of default rules. Each default rule is of the following form: t : F :: (u · t) : G = . (u · t) : G The informal reading of the default is: “If t is a reason justifying F , and it is consistent to assume that (u · t) is a reason justifying G, then (u · t) is a defeasible reason justifying G”. The default rule introduces a unique reason term u, which means that, for a default theory T , the following holds: 1.) For any formula v : H 2 T hJTCS (W ), u 6= v; 2.) For any formula H 2 W , u : (F ! G) is not a subformula of H and 0 0 0 0 ·t ):G0 3.) For any default rule 0 2 D such that 0 = t :F(u::(u 0 ·t0 ):G0 , if F 6= F 0 or G 6= G0 , then u 6= u0 . Every default rule produces a reason term whose structure codifies an ap- plication operation step. Notice that in above, in contrast to axiom A1, we do not require the formula u : (F ! G) to be a part of the knowledge base. Instead, u : (F ! G) is the underlying assumption of on the basis of which we are able to extend an incomplete knowledge base. The propositions of this kind are important in the system since they function as rules allowing for default steps, but they are also specific JTCS formulas. They will be referred to as “war- rants”, because their twofold role mirrors that of Toulmin’s argument warrants [19, p. 91]. Warrants extend the interpretation of the application operation “·” and each warrant is made explicit by means of a function warrant assignment: #(·) : D ! F m. The function maps each default rule to a specific justified con- ditional as follows: #( i ) = u : (F ! G), where i 2 D and i = t:F(u·t):G ::(u·t):G , for some reason term t, a unique reason term u and some formulas F and G. A set of all such underlying warrants of default rules is called Warrant Spec- ification (WS) set. 62 Definition 5 (Warrant specification) For a default theory T = (W, D), jus- tified defeasible conditionals are given by the Warrant Specification set: WS T = #[D] = {un : (F ! G) | #( i ) = un : (F ! G) and i 2 D}. The basis of operational semantics for a default theory T = (W, D) is the pro- cedure of collecting new, reason-based information from the available defaults. A sequence of default rules ⇧ = ( 0 , 1 , . . .) is a possible order in which a list of default rules without multiple occurrences from D is applied (⇧ is possibly empty). Applicability of defaults is determined in the following way: for a set of JTCS -closed formulas we say that a default rule = t:F(u·t):G ::(u·t):G is appli- cable to i↵ t : F 2 and ¬(u · t) : G 2 / . Default consequents are brought together in the set of JTCS formulas that represents the current evidence base: In(⇧) = T hJTCS (W [{cons( ) | occurs in ⇧}). The set In(⇧) collects reason- based information that is yet to be determined as acceptable or unacceptable depending on the acceptability of reasons and counter-reasons for formulas. We need to further specify sequences of defaults that are significant for a the- ory T : default processes.2 For a sequence ⇧, the initial segment of the sequence is denoted as ⇧[k], where k indicates the number of elements contained in that segment of the sequence and a minimal number of defaults for the sequence ⇧. Any segment ⇧[k] is also a sequence. We can now define default processes: Definition 6 (Process) A sequence of default rules ⇧ is a process of a default theory T = (W, D) i↵ every k such that k 2 ⇧ is applicable to the set In(⇧[k]), where ⇧[k] = ( 0 , . . . k 1 ). We will use warrant specification sets WS ⇧ that are relativized to default pro- cesses. The kind of process that we are focusing on here is called closed process. A process ⇧ is taken to be closed i↵ every 2 D that is applicable to In(⇧) is already in ⇧. The possibility to refer to warrants within the language enables us to model undercutting defeaters. They defeat other default reasons, not by contradicting their conclusions as rebutting reasons do, but by denying that their warrant provides support for the conclusion in an undercutting circumstance. Definition 7 (Undercut) A reason u undercuts reason t being a reason for a formula W F in a set of JTCS -closed formulas ✓ In(⇧[k]) i↵ (v)2Sub(t) u : ¬[v : (G ! H)] 2 and v : (G ! H) 2 WS ⇧ . Undercutting brings about revisions of default extensions, as we will show by way of an example in Section 3. For any default theory T = (W, D), an agent always considers potential extension sets of JTCS formulas that meet the following conditions: 1.) W ✓ and 2.) ✓ {W [ cons(⇧) | ⇧ is a process of T }. 2 Our definitions are inspired by Antoniou’s [1] operational semantics for Reiter’s default theories. 63 For any potentially acceptable set we define the notion of acceptability of a justified formula t : F : Definition 8 (Acceptability) For a default theory T = (W, D), a formula t : F 2 cons(⇧) is acceptable w.r.t. a set of JTCS formulas i↵ for each reason u that undercuts t as a reason for F such that u : G 2 In(⇧), T hJTCS ( ) undercuts u as a reason for G. Following [13], we provide formal argumentation semantics for justification as- sertions in terms of multiple extension notions for default theories (formal cor- respondence of JTCS extensions to Dung’s extensions is established in [13]). Definition 9 (JTCS Extensions) For any default theory T = (W, D) based on the JTCS language: JTCS Admissible Extension A potential extension set of JTCS formulas is a JTCS admissible extension of T i↵ T hJTCS ( ) is conflict-free and if each formula t : F 2 is acceptable w.r.t. . JTCS Preferred Extension A JTCS admissible extension , T hJTCS ( ) is a JTCS preferred extension of T i↵ for any other JTCS admissible extension 0 , 6⇢ 0 . JTCS Complete Extension For closed processes ⇧ and ⇧ 0 of T , a set of JTCS for- mulas T hJTCS ( ) ✓ In(⇧) is a JTCS complete extension of T i↵ is a JTCS ad- missible extension of T and each formula t : F 2 cons(⇧ 0 ), if T hJTCS ( ) [ {t : F } is JTCS consistent and t : F is acceptable w.r.t. , then t : F belongs to . JTCS Grounded Extension A JTCS complete extension T hJTCS ( ) is the unique JTCS grounded extension of T if is the smallest potential extension with respect to set inclusion such that T hJTCS ( ) is a JTCS complete extension of T . JTCS Stable Extension For closed processes ⇧ and ⇧ 0 of T , a JTCS stable ex- tension is a JTCS closure of a potential extension ⇢ In(⇧) such that (1) T hJTCS ( ) undercuts all the formulas t : F 2 In(⇧) outside T hJTCS ( ) and (2) for any formula u : G 2 0 such that 0 ⇢ In(⇧ 0 ) and u : G 62 In(⇧), it holds that [ {u : G} is JTCS inconsistent. 3 Undercutting in justification logic and Reiter’s logic In this section, we want to illustrate the advantages of the expressiveness that our logic has in comparison to Reiter’s default logic by means of an example with undercut. Consider an agent reasoning about whether a KLM Boeing 737 aircraft has cleared the take-o↵ protocol or not, given that a source of information says that “the crosswind component at the default runway is at the speed of 35 knots” (C). Knowing that, at this speed of the crosswind component, the Boeing 737 type of aircraft is usually not allowed to proceed with taking o↵, the agent concludes that “the KLM Boeing 737 flight has been delayed” (K), according to the following default rule: r : C :: (s · r) : K 1 = . (s · r) : K The default can be read as follows: “If r is a reason justifying that the crosswind component at the default runway is at 35 knots and it is consistent to assume 64 that (s·r) is a reason justifying that the KLM Boeing 737 flight has been delayed, then (s · r) is a defeasible reason justifying that the KLM Boeing 737 flight has been delayed”. If the agent receives additional information that it is not the case that “the SAS Boeing 737 aircraft has been delayed” (S), then the agent has a reason to assume that “the aircraft can be allocated to an alternative runway” (R). t : ¬S :: (u · t) : R 2 = . (u · t) : R On a runway of a di↵erent orientation, the initial readings of the crosswind may even turn into a favorable headwind component. The information that there is an alternative runway undercuts the initial piece of reasoning codified by s, according to the following default rule: (u · t) : R :: (v · (u · t)) : ¬[s : (C ! K)] 3 = . (v · (u · t)) : ¬[s : (C ! K)] The consequent reads as follows: “(v · (u · t)) is a defeasible reason denying that the reason s justifies that if the crosswind component for the default runway is at the speed of 35 knots, then the KLM Boeing 737 flight has been delayed”. Additionally, the agent has a reason to conclude that the KLM flight has not been delayed, grounded on the reasoning about an alternative runway: (u · t) : R :: (w · (u · t)) : ¬K 4 = . (w · (u · t)) : ¬K Were it the case that the course of the agent’s reasoning follows the proposed order, the agent would have to revise the conclusion supported by the rea- son (s · r). For a default theory T1 = (W, D) with W = {r : C, t : ¬S} and D = { 1 , 2 , 3 , 4 }, the process ( 1 , 2 , 3 ) corresponds to such course of reason- ing with a revised JTCS admissible extension. Figure 1 shows all the possible processes of T . Is there a way to model undercut in Reiter’s default logic, without extending the logic with, say, default priorities, as done in [10] and [5]? To answer this, we need to view default logic from the perspective of formal argumentation. The relation between formal argumentation and Reiter’s default logic is known. It is shown in [7] that Reiter’s default logic extensions can be defined in terms of stable extensions of Dung’s frameworks and [13] shows that a large subclass of Dung’s frameworks is a special case of our logic. But besides finding formal cor- respondences between their extensions, it is interesting to look at the conceptual relation of Reiter’s logic to our justification logic. This relation is not straightfor- ward, because the two logics are based on di↵erent underlying languages. This di↵erence does not cause divergence in the way the two logics model rebuttal. Rebuttal is based on the workings of multiple incompatible extensions: two for- mulas extending some knowledge base rebut each other if they cannot both be included in a same default extension. However, the comparison of the ways in which the two logics deal with the concept of undercut reveals some immediate benefits of reifying default reasons in justification logic. 65 T hJTCS ({r : C, t : ¬S}) 1 2 (s · r) : K (u · t) : R 2 1 3 4 (u · t) : R (s · r) : K (v · (u · t)) : ¬[s : (C ! K)] (w · (u · t)) : ¬K 3 4 3 1 3 (v · (u · t)) : ¬[s : (C ! K)] (w · (u · t)) : ¬K (v · (u · t)) : ¬[s : (C ! K)] (s · r) : K (v · (u · t)) : ¬[s : (C ! K)] Fig. 1. Each node of the process tree of T is labeled with an In-set after a default rule (edges) has been applied. Visually, we display only the formulas that are added to In-sets as a result of applying the available defaults. The general form of a default rule in Reiter’s logic is ': 1, . . . , m , for some predicate logic formulas ', 1 , . . . , m and . An operational seman- tics similar to ours is given for Reiter’s logic in [1]. Besides closure, [1] in- troduces an additional condition on the extension-producing processes of Re- iter’s default theories: success. A process is successful if each of the justifica- tions 1 , . . . , m is consistent with the consequents added to an In-set after other defaults have been applied. To capture this formally, we define the set Out(⇧) = {¬ | 2 just( ) for some 2 ⇧}, for some justification just( ) of a rule in a process ⇧ of Reiter’s theory = (W, D). None of the formulas from an Out-set should become a part of an In-set for the same process. For a set of first-order formulas E = In(⇧), E is an extension in Reiter’s logic if and only if ⇧ is both closed and successful. In our logic, it is possible to consider consequents of defaults as arguments based on their underlying warrants. This enables representing conflicts simply by opposing reasons. In Reiter’s logic, reasons are not reified and their conflicts cannot be reflected in the logical language. It is, however, possible to take the perspective of formal argumentation on Reiter’s logic. To take such perspective, we follow [16, p. 52] in defining arguments in terms of finite processes of Reiter’s theory and their mutual attacks through conflicts of In-sets with Out-sets. We start from defining attacks in terms of finite processes of a theory = (W, D): – ⇧ attacks ⇧ 0 if ' 2 In(⇧) for some ' 2 Out(⇧ 0 ), 66 where ⇧ and ⇧ 0 are some finite processes of . We can develop further on this definition to specify di↵erent kinds of attack: – If all the default rules from ⇧ and ⇧ 0 could possibly form a finite process ⇧ 00 of (in any possible order of the sequence), then the attack between ⇧ and ⇧ 0 is undercut. Otherwise, it is a rebuttal between ⇧ and ⇧ 0 . The idea behind the refinement of the attack definition is that in Reiter’s logic, non-normal default rules can be seen as a way to introduce “exclusionary rea- sons” [10] and undercut in Reiter’s theory. Consider the following two Reiter’s default rules: 0 35Knots(crosswind ) : ¬alternative(runway) = , delayed (KLM ) saying that “if the crosswind component at the default runway is at 35 knots, and it is consistent to assume that the aircraft cannot be allocated to an alternative runway, then the KLM Boeing 737 flight has been delayed” and 00 35Knots(crosswind ) ^ ¬delayed (SAS ) : alternative(runway) = , alternative(runway) saying that “if the crosswind component at the default runway is at 35 knots and the SAS Boeing 737 flight has not been delayed, and it is consistent to assume that the flight can be allocated to an alternative runway, then the flight can be allocated to an alternative runway”. Moreover, the following default is available to the agent: 000alternative(runway) : ¬delayed (KLM ) = . ¬delayed (KLM ) Take = (W, D) to be a Reiter’s default theory with W = {35Knots(crosswind ), ¬delayed (SAS )} and D = { 0 , 00 , 000 }. The process tree for the Reiter’s theory is found in Figure 3. The idea of undercut can be illustrated by the way in which ⇧ 0 = ( 00 ) attacks ⇧ = ( 0 ) via affirming the circumstance in which the conclusion of ⇧ would not be reasonable any more, but it does not affirm the negation of that conclusion. This corresponds to the idea of undercut. Notice that, in contrast to 1 above, Reiter’s rule 0 needs to include the negation of the exclusionary circumstance alternative(runway) in conveying the idea of undercut. Notice that the mechanism whereby ⇧ 0 attacks ⇧ is also responsible for the problem of process “destruction” [1, p. 63]. An example of process destruction occurs in the unsuccessful process ⇧ 00 = ( 0 , 00 ), where, after 00 has been ap- plied, ⇧ 00 becomes closed and unsuccessful. As it can be seen from the process tree of T , justification logic-based default theories are able to model interaction among default rules and undercut without having to resort to the use of process destruction. This is mainly due to the fact that the rule 3 , which is “missing” in the Reiter’s logic rendition of the example, brings forth the undercut of the default reason from 1 as a part of the example description. 67 T h({c, ¬s}) ; 0 00 Fig. 2. The process tree of T h({c, ¬s, k}) {r} T h({c, ¬s, r}) {¬r} Reiter’s default theory . Un- 00 000 dercut is modelled by the failed process branch. T h({c, ¬s, k, r}) {r, ¬r} T h({c, ¬s, r, ¬k}) {¬r, k} failed closed & successful Several remarks are at hand by comparing the structures of the process trees of T and . Although the theories model the same phenomenon, Reiter’s logic noticeably simplifies the example. While some ways of simplifying are desirable, there are several reasons to prefer the representation of undercut in justification logic. One of them is that failed processes disable reinstatement of reasons that could, in principle, be reinstated by undercutting their undercutters. In our ex- ample above, even if the SAS flight has not been delayed, it might be the case that the current demand for the runway reassignment exceeds the operational capacities of the alternative runway. This, in turn, provides a reason to reinstate the initial reason in support of the claim that the KLM flight is delayed. Justi- fication logic is able to represent such reason reinstatement and processes that are, in principle, infinitely extendable. As can be seen from the definitions of JTCS extensions, only JTCS admis- sible extensions can be identified by looking at a single branch of the process tree of T . To determine the status of other JTCS extensions, all reasons need to be taken into account.3 In contrast, Reiter’s default processes are self-contained with respect to the extensions status. Therefore, JTCS extensions have more in common with the notion of Reiter’s logic consequence relation (credulous and skeptical ). For instance, JTCS grounded extensions correspond to the skeptical notion of validity, which amounts to the intersection of all Reiter’s extensions. It is only in taking the argumentation perspective on Reiter’s processes that we need to look at the dependencies of di↵erent process tree branches. Conceptually, the most important advantage of representing defeasible rea- soning in justification logic is that neither for reaching a defeasible conclu- sion nor for undercutting that reason, agents do not need to anticipate exclu- sionary reasons. In an important sense, anticipating exclusionary reasons with ¬alternative(runway) in the Reiter’s rule 0 above goes against the idea of de- fault reasoning. Namely, in the sense that the number of these conditions may be infinite. The need to anticipate exclusionary reasons brings us back to the initial problem: we want to find out how to avoid anticipating numerous exceptions before an agent is able to reach a conclusion. It is an advantage of our theory to be able to model exceptions to rules via undercut, but without the drawback of guessing all the conditions of undercut within a default theory. 3 This could be further amended by considering “anytime reasoning” methods as, for example, those proposed in [6] for Reiter’s logic. 68 Finally, notice that by using Reiter’s non-normal defaults, we are not only able to define undercut, but also to define theories such as ⇤ = (W ⇤ , D⇤ ), where W ⇤ = {;} and D⇤ = { 0000 = ;:¬A A }. The rule ;:¬A A invalidates its own applicability. Using the above defined translation to argument frameworks, it is possible to build a single-argument attack cycle in terms of the argument ⇧ = ( 0000 ). This kind of attack is well-known from Dung’s abstract argumentation frameworks [7]. In [13], it is proved that defining single-argument attack cycles is not possible once arguments’ warrants have been included as underlying rules for each default. This shows that although 0000 sanctions “jumping” to the conclusion A, this does not mean that the type of inference it instantiates counts a reasoned defeasible step. 4 Related work and conclusion Some existing extensions of default theories that can deal with the problem of exclusionary reasons come close to our intention of reifying default reasons. Most notably, approaches that are based on reasoning about default rule priorities such as [5, 9, 10] include a variant of reasoning about other reasons, namely, by reasoning about the relative weights of defaults. Strictly speaking, reasoning about default priorities reifies default rules, not default reasons, by extending the underlying language of default logic with default names and a predicate symbol that represents priorities among defaults. In such default theories, agents may arrive to conclusions about which ordering of defaults is a preferred one and to, thereby, consider higher priority as a source of defeat. Priority weighing in the style of [5] can be represented in process trees, as done in [1, pp. 97-98]. It can be noticed that one of the difficulties with such reasoning is that before applying a default, an agent needs to consider all other applicable defaults. As in Reiter’s logic, processes are possibly failed, where failure is now due to making application choices that are inconsistent with a valid ordering among defaults. Horty [10, p. 124] defines “exclusionary default theories” where he explicitly includes undercutters, but his undercut is logically only a predicate saying that a rule has been excluded. A more elaborate study of the di↵erent ways to defeat reasons is carried out in argumentation theory, from the classical account of undercut and rebuttal in [14] to some later formal argumentation frameworks such as, e.g., [15, 4, 20]. These frameworks are not based on default logic nor do they base their formalism on a language with formulas that feature reason terms. Hence, as for our current discussion on the problem of reification, such systems do not provide explicit answers. Among justification logic systems, some of them [3, 18] combine belief revision and dynamic epistemic logic techniques to model defeat, which is closest in its kind to undermining. However, none of them is able to model undercut or to encode defeasibility in the structure of reason terms. Finally, our answer to the problem of reification is that both a prerequisite of a default rule and the rule itself are involved in reifying default reasons. This is reflected in the way in which default application codifies default steps from 69 warrants and prerequisites of defaults to their consequents. An immediate ad- vantage of reification is that, by referring to such reason-producing steps within the object language, we can provide a fine-grained logical account of defeat. References 1. Antoniou, G.: Nonmonotonic Reasoning. Cambridge, MA: MIT Press (1997) 2. Artemov, S.N.: Explicit provability and constructive semantics. Bulletin of Sym- bolic Logic pp. 1–36 (2001) 3. Baltag, A., Renne, B., Smets, S.: The logic of justified belief, explicit knowledge, and conclusive evidence. Annals of Pure and Applied Logic 165(1), 49–81 (2014) 4. Besnard, P., Hunter, A.: A logic-based theory of deductive arguments. Artificial Intelligence 128(1-2), 203–235 (2001) 5. Brewka, G.: Reasoning about priorities in default logic. In: Proceedings of the Twelfth National Conference on Artificial Intelligence, AAAI’94. vol. 2, pp. 940– 945. AAAI Press/The MIT Press (1994) 6. Cadoli, M., Schaerf, M.: Approximate inference in default logic and circumscrip- tion. Fundamenta Informaticae 21(1, 2), 103–112 (1994) 7. Dung, P.M.: On the acceptability of arguments and its fundamental role in non- monotonic reasoning, logic programming and n-person games. Artificial Intelligence 77(2), 321–357 (1995) 8. Fitting, M.: Justification logics, logics of knowledge, and conservativity. Annals of Mathematics and Artificial Intelligence 53(1-4), 153–167 (2008) 9. Horty, J.F.: Reasons as defaults. Philosopher’s Imprint 7(3), 1–28 (2007) 10. Horty, J.F.: Reasons as Defaults. Oxford University Press (2012) 11. Mkrtychev, A.: Models for the logic of proofs. In: Adian, S., Nerode, A. (eds.) Logical Foundations of Computer Science, 4th International Symposium, LFCS ’97. vol. 1234 of LNCS, pp. 266–275. Springer-Verlag (1997) 12. Pandžić, S.: A logic of default justifications. In: Fermé, E., Villata, S. (eds.) 17th International Workshop on Nonmonotonic Reasoning, NMR 2018. pp. 126–135 (2018) 13. Pandžić, S.: Justification logic as a theory of structured arguments. Unpublished manuscript (2019) 14. Pollock, J.L.: Defeasible reasoning. Cognitive Science 11(4), 481–518 (1987) 15. Prakken, H.: An abstract framework for argumentation with structured arguments. Argument and Computation 1(2), 93–124 (2010) 16. Prakken, H.: Commonsense Reasoning and Argumentation. Utrecht University (2018), course reader 17. Reiter, R.: A logic for default reasoning. Artificial Intelligence 13(1-2), 81–132 (1980) 18. Renne, B.: Multi-agent justification logic: Communication and evidence elimina- tion. Synthese 185(1), 43–82 (2012) 19. Toulmin, S.E.: The Uses of Argument. Cambridge University Press (2003) 20. Verheij, B.: Correct grounded reasoning with presumptive arguments. In: Loizos, M., Kakas, A. (eds.) European Conference on Logics in Artificial Intelligence, JELIA 2016. pp. 481–496. Springer (2016) 70