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.
In its most general sense, the notion of “reason” can be understood as a support 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
[
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
basics of the logic of default justifications first introduced in [
The logic of default justifications was first presented in [
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 constant, 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 [
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
The semantics for JTCS is an adapted version of the semantics for the logic
of proofs (LP) given by [
Definition 2 (JTCS model) A function reason assignment based on CS is defined 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: – 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 reflexive interpretations in such a way that, for any set of JTCS formulas ⌃ : Definition 3 (JTCS consequence relation) ⌃ |= F i↵ for all reflexive interpretations I, if I |= B for all B 2 ⌃ , then I |= F .
For a set of formulas ✓ F m and the J TCS 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
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 countable 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 3.) For any default rule 0 2 D such that 0 = t0:F(u0:0:·(tu00)·:tG0)0: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 application 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 “warrants”, 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 conditional as follows: #( i) = u : (F ! G), where i 2 D and i = t:F ::(u·t):G , for (u·t):G 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 Specification (WS) set. Definition 5 (Warrant specification) For a default theory T = (W, D), justified defeasible conditionals are given by the Warrant Specification set:
WST = #[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 procedure 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::·(tu)·:tG):G is applicable 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 reasonbased 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 theory 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 processes. 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 F in a set of JTCS-closed formulas ✓ In(⇧ [k]) i↵ W(v)2 Sub(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 [
we define the notion of acceptability of a justified formula t : F : undercuts u as a reason for G.
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
u that undercuts t as a reason for F such that u : G 2 In(⇧ ), T hJTCS ( )
i↵ for each reason
Following [
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, 0.
JTCS Complete Extension For closed processes ⇧ and ⇧ 0 of T , a set of JTCS formulas T hJTCS ( ) is JTCS consistent and t : F is acceptable w.r.t. , then t : F belongs to missible extension of T and each formula t : F 2 cons(⇧ 0), if T hJTCS ( ) [ { t : F } JTCS Grounded Extension A JTCS complete extension T hJTCS ( ) is the unique ✓ In(⇧ ) is a JTCS complete extension of T i↵ is a JTCS adto 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 extension 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: 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 1 = r : C :: (s · r) : K 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). 2 = t : ¬S :: (u · t) : R (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 reason (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 reasoning 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 [
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),
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
reasons” [
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 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: 000 = alternative(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 arming the circumstance in which the conclusion of ⇧ would not be reasonable any more, but it does not arm 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 applied, ⇧ 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. T h({c, ¬s, k}) {r}
T h({c, ¬s, r}) {¬r} 00
000 T h({c, ¬s, fkai,lerd}) {r, ¬r}
T h({c, ¬s, r, ¬k}) closed & successful{¬r, k}
Fig. 2. The process tree of Reiter’s default theory . Undercut is modelled by the failed process branch.
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 example 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. Justification 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 admissible 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
reasoning in justification logic is that neither for reaching a defeasible
conclusion nor for undercutting that reason, agents do not need to anticipate
exclusionary reasons. In an important sense, anticipating exclusionary reasons with
¬alternative(runway ) in the Reiter’s rule 0 above goes against the idea of
default 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 [
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 [
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 [
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 [
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