=Paper=
{{Paper
|id=Vol-2445/paper_6
|storemode=property
|title=Reifying Default Reasons in Justification Logic
|pdfUrl=https://ceur-ws.org/Vol-2445/paper_6.pdf
|volume=Vol-2445
|authors=Stipe Pandžić
|dblpUrl=https://dblp.org/rec/conf/ki/Pandzic19
}}
==Reifying Default Reasons in Justification Logic==
https://ceur-ws.org/Vol-2445/paper_6.pdf
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