=Paper= {{Paper |id=Vol-3739/paper-3 |storemode=property |title=Defeasible Justification for KML-Style Logic |pdfUrl=https://ceur-ws.org/Vol-3739/paper-3.pdf |volume=Vol-3739 |authors=Victoria Chama,Steve Wang,Thomas Meyer,Giovanni Casini |dblpUrl=https://dblp.org/rec/conf/dlog/ChamaWMC24 }} ==Defeasible Justification for KML-Style Logic== https://ceur-ws.org/Vol-3739/paper-3.pdf

Defeasible Justification for KLM-Style Logic
Victoria Chama1,2 , Steve Wang1,2 , Thomas Meyer1,2,3 and Giovanni Casini3,1,2
1
University of Cape Town, South Africa
2
CAIR, South Africa
3
CNR-ISTI, Italy

Abstract
Research in description logics (DLs) and formal ontologies has dedicated quite an effort to the investigation of the
notion of explanation for DL reasoning, for example relying on the notion of justification [1]. There has also been
some effort dedicated to the definition of defeasible reasoning for DLs that, contrary to the classical monotonic
reasoning, is appropriate for dealing with incomplete/uncertain information. In the present paper, we extend the
notion of justification to the framework of defeasible reasoning for DLs; specifically, we consider rational closure
[2], an entailment relation that is of particular importance in the area of defeasible reasoning. Here we present
the main theoretical results for the DL 𝒜ℒ𝒞, and an implementation of our solution, at the moment developed
for propositional logic.

Keywords
Defeasible entailment, rational closure, justification-based explanations

1. Introduction
Knowledge Representation and Reasoning (KRR) is an essential aspect of Artificial Intelligence (AI).
Logics such as Propositional Logic (PL) and Description Logic (DL) provide a way to formulate and
represent knowledge in a structured manner. Reasoning with such formalised knowledge representations
allows us to deduce new information from explicit knowledge. In monotonic (classical) reasoning
adding new knowledge cannot cause the retraction of previously drawn deductions. This characteristic
of monotonic reasoning is not appropriate for reasoning with rules and generalisations that admit
exceptions.
Consider the classic ‘penguin example’: “penguins are birds”, “penguins cannot fly” and “birds can
fly”. Monotonic reasoning concludes that there are no instances of penguins because birds can both fly
and not fly. However, penguins legitimately are birds that cannot fly. Non-monotonic reasoning can
overcome such restriction, in particular the approach to non-monotonicity that is known as defeasible
reasoning. We use a non-monotonic extension of the DL 𝒜ℒ𝒞 to perform defeasible reasoning, for
which software tools already exist [3].
Conclusions produced by reasoning tools are often difficult to understand due to the volume and
complexity of the statements, and there is a need for algorithms and tools that provide explanations
for conclusions. In recent years, research has been done to provide explanations for conclusions in
monotonic reasoning [1, 4]. Consequently, various algorithms to compute explanations and implemen-
tations of these algorithms for DL are available as plugins in Protégé [1]. However, little research has
gone into providing explanations for defeasible reasoning systems. Defeasible reasoning introduces
well-defined and systematic approaches to reasoning with incomplete information and rules that admit
exceptions [5]. Some popular defeasible reasoning systems are based on the semantics developed by
Kraus, Lehmann, and Magidor (KLM) [6]. We focus here on rational closure, originally defined for PL
[7], but has also been lifted to the case for DLs [2, 8, 9]. In this paper we introduce an algorithm that

DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway
$ vchama@cs.uct.ac.za (V. Chama); wngshu003@myuct.ac.za (S. Wang); tmeyer@cs.uct.ac.za (T. Meyer);
giovanni.casini@isti.cnr.it (G. Casini)
https://github.com/SteveWang7596 (S. Wang)
0000-0003-3641-4849 (V. Chama); 0000-0002-8741-2213 (S. Wang); 0000-0003-2204-6969 (T. Meyer); 0002-4267-4447
(G. Casini)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
computes explanations for conclusions drawn using rational closure. The logic we use for this algorithm
is a KLM extension to DL 𝒜ℒ𝒞. We also present an implementation of the algorithm in PL.
The rest of the paper is structured as follows. The next section introduces the necessary preliminaries.
In Section 3, we use the concepts provided in Section 2 to construct a defeasible justification algorithm.
Then, we present an implementation of the defeasible justification algorithm for the propositional case
in Section 4. Lastly, we conclude the paper in Section 5.

2. Preliminaries
In this section, we introduce the foundational notions and concepts required to build an algorithm that
computes explanations for conclusions produced by reasoning services. After a brief introduction to the
DL 𝒜ℒ𝒞, we present the notion of justification defined by Horridge which serves as an explanation for
classical reasoning services. Then we introduce the defeasible logic that we are going to use throughout
the paper. Lastly, we provide details on the form of defeasible reasoning known as rational closure.

2.1. Description Logic 𝒜ℒ𝒞
Description logics (DLs) are a family of logical formalisms that can represent conceptual knowledge in a
structured and formally well-understood way. 𝒜ℒ𝒞 is a basic formalism of DL and stands for Attributive
(Concept) Language with Complements [10]. It includes concept names, concept intersection, concept
union, complement, existential and universal qualifiers. This section provides the syntax and semantics
of 𝒜ℒ𝒞 that will be used in the rest of this paper.

Definition 1 (Syntax). The language of 𝒜ℒ𝒞 is built from a finite set of atomic concept names, 𝐴, and a
finite set of atomic role names, 𝑅. Complex concepts are denoted with 𝐶 and are built inductively according
to the following rule:

𝐶 ::= ⊤|⊥|𝑎|¬𝐶|𝐶 ⊓ 𝐶|𝐶 ⊔ 𝐶|∃𝑟.𝐶|∀𝑟.𝐶

where ⊤ is the universal concept, ⊥ is the bottom concept, ¬ is the unary negation operation, ⊓ is the
binary intersection operation, ⊔ is the binary union operation, ∃ is the existential qualifier, ∀ is the universal
qualifier, 𝑎 ∈ 𝐴 and 𝑟 ∈ 𝑅 [11].

We use ℒ to denote the language of all 𝒜ℒ𝒞 concepts. The semantics of ℒ is given by the notion of
interpretation.

Definition 2 (Semantics). An interpretation is a structure ℐ = ⟨∆ℐ , ·ℐ ⟩, where ∆ℐ is a non-empty set
called the domain, and ·ℐ is an interpretation function. For every 𝑐 ∈ 𝐶, 𝑐ℐ ⊆ ∆ℐ , ⊤ℐ = ∆ℐ , ⊥ℐ = ∅
and for every 𝑟 ∈ 𝑅, 𝑟ℐ ⊆ ∆ℐ × ∆ℐ . For some complex concepts 𝐶 and 𝐷 ∈ ℒ, the interpretation function
·ℐ extends to interpret all complex concepts of ℒ in the following way:

(¬𝐶)ℐ = ∆ℐ /𝐶 ℐ , (𝐶 ⊓ 𝐷)ℐ = 𝐶 ℐ ∩ 𝐷ℐ , (𝐶 ⊔ 𝐷)ℐ = 𝐶 ℐ ∪ 𝐷ℐ ,
(∀𝑟.𝐶)ℐ = {𝑥|𝑦 ∈ 𝐶 ℐ for every 𝑦 s.t (𝑥, 𝑦) ∈ 𝑟ℐ }, (∃𝑟.𝐶)ℐ = {𝑥|(𝑥, 𝑦) ∈ 𝑟ℐ for some 𝑦 ∈ 𝐶 ℐ }

Given 𝐶, 𝐷 ∈ ℒ, 𝐶 ⊑ 𝐷 is called a subsumption statement (or a statement). Concept equivalence,
denoted 𝐶 ≡ 𝐷, is the abbreviation for 𝐶 ⊑ 𝐷 and 𝐷 ⊑ 𝐶. An 𝒜ℒ𝒞 TBox 𝒯 is a finite set of
statements. We refer to such statements in 𝒯 as axioms. We use 𝛼, 𝛽, ... to denote statements in 𝒯 . An
interpretation ℐ satisfies a statement, 𝐶 ⊑ 𝐷, denoted ℐ ⊩ 𝐶 ⊑ 𝐷, if 𝐶 ℐ ⊆ 𝐷ℐ . An interpretation ℐ is
a model of TBox 𝒯 if ℐ satisfies every statement in 𝒯 . Given a TBox 𝒯 and a statement 𝛼, 𝒯 entails 𝛼,
denoted 𝒯 |= 𝛼, if and only if for every interpretation ℐ such that ℐ ⊩ 𝒯 , it also holds that ℐ ⊩ 𝛼. In
this paper, we are not interested in the ABox 𝒜 which is a finite set of concept assertions (instantiation
of concepts) and role assertions (instantiation of roles).
2.2. Justifications
Given an entailment, 𝒯 |= 𝛼, an explanation for 𝒯 |= 𝛼 is a subset of 𝒯 such that it entails 𝛼. Intuitively,
we want to identify the axioms in the 𝒯 that contributed towards the entailment. There are several
approaches to computing explanations for entailments [1, 12]. In this paper, we base the explanation
for entailment on the notion of justification defined by Horridge [1]. Horridge defines justification for
an entailment as the minimal subsets of the knowledge base that entails the query.

Definition 3 (Justification). Let 𝒯 be a TBox and 𝛼 be a statement. 𝒥 is a justification for 𝒯 |= 𝛼 if
𝒥 ⊆ 𝒯 , 𝒥 |= 𝛼 and, for all 𝒥 ′ ⊂𝒥 , it holds that 𝒥 ′ ̸|= 𝛼.

Example 1. Let us consider the penguin example that we mentioned in the introduction. We can formalise
it in a classical TBox, 𝒯 , about birds, penguins and a special penguin that has flying capabilities.
⎧ ⎫
⎪
⎪ Bird ⊑ Fly, ⎪
⎪
⎪
⎪
⎪
⎪ Bird ⊑ Wings, ⎪
⎪
⎪
⎪
Penguin ⊑ ¬Fly,
⎪
⎪ ⎪
⎪
⎨ ⎬
𝒯 = SpecialPenguin ⊑ Fly,
Penguin ⊑ Bird,
⎪
⎪ ⎪
⎪
⎪
⎪ ⎪
⎪
SpecialPenguin ⊑ Penguin,
⎪
⎪ ⎪
⎪
⎪
⎪ ⎪
⎪
Robin ⊑ Bird
⎩ ⎭

Such a TBox entails that special penguins fly (𝒯 ⊨ SpecialPenguin ⊑ Fly). We can identify two
justifications for such a conclusion, that is, two minimal subsets of 𝒯 that allow the derivation of
SpecialPenguin ⊑ Fly:

𝒥1 = {SpecialPenguin ⊑ Fly}
𝒥2 = {SpecialPenguin ⊑ Penguin, Penguin ⊑ Bird, Bird ⊑ Fly}

𝒥1 is a valid justification because the query, SpecialPenguin ⊑ Fly, is an axiom in 𝒯 , and 𝒥2 is also
valid according to Definition 3.
Horridge presents an implementation for computing justifications in Protégé [1, Algorithm 4.1]. In
what follows we will refer to it as Algorithm ComputeAllJustifications (Algorithm 4.1), that, given a
TBox 𝒯 and a statement 𝐶 ⊑ 𝐷 entailed by 𝒯 , returns all associated justifications.

2.3. Defeasible Reasoning
In this section, we discuss how defeasible reasoning has been implemented in DLs. Defeasible logic
enables us to reason with rules and generalisations that model typical scenarios that admit exceptions.
For example, birds typically fly but penguins are atypical birds that do not fly.
There is existing work for extending description logics with defeasible reasoning [2, 3, 8, 9, 13, 14,
15, 16, 17, 18]. As mentioned in the introduction our work is based on the so-called KLM approach to
defeasible reasoning [6], and in particular on a specific entailment relation, rational closure [7]. We focus
on rational closure since it is a particularly significant entailment relation in defeasible reasoning: other
relevant entailment relations are based on it [19, 20, 21], it has already been redefined for description
logics [2, 8, 9, 22], moreover it can be implemented just using a relatively simple procedure on top
of some classical DL reasoner [3]. We introduce our explanations for defeasible reasoning using a
well-known extension of the DL 𝒜ℒ𝒞 to model defeasible reasoning [2]. Such an extension allows for
an additional type of subsumption statement: ‘𝐶 ⊏ ∼ 𝐷’ is a defeasible statement which is read “Typically,
𝐶’s are 𝐷’s, as opposed to “all 𝐶’s are 𝐷’s” for the classical subsumptions ‘𝐶 ⊑ 𝐷’.

Definition 4. (Defeasible Inclusion) For 𝐶, 𝐷 ∈ ℒ, a defeasible inclusion is a statement of the form 𝐶 ⊏
∼ 𝐷.
A defeasible statement 𝐶 ⊏ ∼ 𝐷 can be read as “usually, an instance of the class 𝐶 is also an instance
of the class 𝐷”. A statement like “birds typically fly”, formally represented by Bird ⊏ ∼ Fly in defeasible
𝒜ℒ𝒞, indicates that if something is a bird then it is reasonable to infer that it flies, if we are not informed
of the contrary. ‘ ⊏
∼ ’ is meant to be the defeasible counterpart of the classical subsumption ⊑ [2]. We
define a DBox 𝒟 as a finite set of defeasible statements, and a defeasible knowledge base 𝒦 = 𝒯 ∪ 𝒟 as
consisting of a TBox and DBox. We refer to statements stated in 𝒦 as axioms. The statements that have
a defeasible form are those that can have exceptions to the statements: since most birds fly, but there
are exceptions such as penguins and ostriches, we use Bird ⊏ ∼ Fly instead of Bird ⊑ Fly.

Example 2. Consider the following defeasible version of TBox 𝒯 shown in Example 1.
⎧ ⎫
⎨ Penguin ⊑ Bird, ⎬
𝒯 = Robin ⊑ Bird
SpecialPenguin ⊑ Penguin
⎩ ⎭
Bird ⊏
⎧ ⎫
⎪ ∼ Fly, ⎪
Bird ⊏
⎪ ⎪
Wings,
⎨ ⎬
𝒟= ∼
⎪
⎪ Penguin ⊏ ∼ ¬Fly ⎪ ⎪
SpecialPenguin ⊏ Fly
⎩ ⎭
∼

2.3.1. Rational Closure
As mentioned, we focus our attention on rational closure, a specific form of defeasible entailment. For
the full description, the semantics, and the motivation for the use of rational closure in 𝒜ℒ𝒞, the
reader is directed to the work of Britz et al. [2], while here we focus only on the description of the
algorithmic procedure to decide rational closure. In essence, given a knowledge base 𝒦 = 𝒯 ∪ 𝒟,
the algorithm produces a ranking of the defeasible axioms in 𝒟, all of which are then converted to
classical axioms, from which defeasible entailment (rational closure) can then be computed by a series
of classical entailment checks. The ranking of axioms is based on their exceptionality. Intuitively, in case
of potential conflicts exceptionality arranges axioms in the knowledge base according to specificity: if
we have conflictual information, (e.g., birds fly, penguins are birds, and penguins do not fly), the axioms
that are considered less specific than others will be discarded first (e.g., ‘birds fly’ is discarded in favour
of ‘penguins do not fly’ since information about penguins is more specific than information about birds
in general).
In [2, Sect. 5.2] the procedure Exceptional is aimed at deciding which defeasible axioms are more
exceptional w.r.t. a knowledge base. Exceptionality is based on the specificity among classes in case
we have a conflict: for example ‘penguins usually do not fly’ (Penguin ⊏ ∼ ¬Fly) is more exceptional
than ‘birds usually fly’ (Bird ∼ Fly), since there is a potential conflict and the antecedent of the former
⊏
(Penguin) is a subclass (more specific) than the antecedent of the latter (Bird). We do not provide the
procedure Exceptional here, referring the reader to [2, Sect. 5.2]. On top of procedure Exceptional we
build Algorithm 1, that takes as input a knowledge base 𝒦 = 𝒯 ∪ 𝒟 and returns a ranking of the axioms
in 𝒟 according to exceptionality: from rank 0, with ℰ0 containing all the defeasible axioms in 𝒟, to
some rank 𝑛, with ℰ𝑛 , containing the most exceptional axioms in 𝒟. Algorithm 1 is taken from [23,
Sect. 5.2]. We again refer the reader to this paper for proper explanations and analysis. Here we present
the algorithm and go through an example to give a sense of how the algorithm works.

Example 3. For the defeasible knowledge base 𝒦 from Example 2, ComputeRanking will be executed as
follows.1

1. The algorithm takes as input 𝒦 and creates a hierarchy of defeasible axioms w.r.t their exceptionality.
First it considers the entire set 𝒟, associating it with ℰ0 (line 6):
1
Note that the algorithm also introduces a knowledge base 𝒦* = 𝒯 * ∪ 𝒟* . 𝒦* is a reformulation of the input 𝒦 that is
needed for knowledge bases with a particular form, which is not the case for our example. Here the reader can just assume
that 𝒦* = 𝒦 and, again, we refer to [2] for an explanation.
Algorithm 1: ComputeRanking(𝒦)
Input: 𝒦 = 𝒯 ∪ 𝒟
Output: 𝒦* = 𝒯 * ∪ 𝒟* , an exceptionality sequence ℰ0 , . . . , ℰ𝑛 and a partitioning
𝑅 = {𝒟0 , . . . , 𝒟𝑛 } for 𝒟*
*
1 𝒯 ←𝒯
2 𝒟* ← 𝒟
3 𝑅←∅
4 repeat
5 𝑖←0
6 ℰ0 ← 𝒟 *
7 ℰ1 ← Exceptional(𝒯 * , ℰ0 )
8 while ℰ𝑖+1 ̸= ℰ𝑖 do
9 𝑖←𝑖+1
10 ℰ𝑖+1 ← Exceptional(𝒯 * , ℰ𝑖 )
11 𝒟∞* ←ℰ
𝑖
12 𝒯 ← 𝒯 * ∪ {𝐶 ⊑ 𝐷 | 𝐶 ⊏
* *
∼ 𝐷 ∈ 𝒟∞ }
13 𝒟 * ← 𝒟 * ∖ 𝒟∞*
*
14 until 𝒟∞ = ∅
15 for 𝑗 ← 1 to 𝑖 do
16 𝒟𝑗−1 ← ℰ𝑗−1 ∖ ℰ𝑗
17 𝑅 ← 𝑅 ∪ {𝒟𝑗−1 }
18 ℰ ← (ℰ0 , ..., ℰ𝑖−1 )
19 return 𝒦* = 𝒯 * ∪ 𝒟 * , ℰ, 𝑅

ℰ0 = {Bird ⊏ ⊏ ⊏ ⊏
∼ Fly, Bird ∼ Wings, Penguin ∼ ¬Fly, SpecialPenguin ∼ Fly}
2. Then it applies the algorithm Exceptional to it (line 7). Exceptional identifies all the potential conflicts
in 𝒯 , that in our case are two: (1) birds fly, but penguins, that are birds, do not; (2) penguins do not
fly, but special penguins, that are penguins, do. From such two conflicts, the algorithm Exceptional
identifies the most specific pieces of defeasible information that play a role in it: penguins do not fly
for (1) and special penguins fly for (2). Such axioms are associated with the first level of exceptionality:

ℰ1 = {Penguin ⊏ ⊏
∼ ¬Fly, SpecialPenguin ∼ Fly}.
3. Now, since ℰ1 ̸= ℰ0 , we apply the Exceptional algorithm iteratively until we reach a fixed point
(lines 9-12). More in detail, we apply it to 𝒯 , ℰ1 , and Exceptional identifies a potential conflict
corresponding to case (2) above: (2) penguins do not fly, but special penguins, that are penguins, do.
Again, the algorithm identifies the most specific defeasible axioms playing a role in the potential
conflicts (in this case, special penguins fly), and associates them with a new exceptionality level ℰ2
(line 11):

ℰ2 = {SpecialPenguin ⊏
∼ Fly}.
4. Since ℰ2 ̸= ℰ1 (line 9) we again apply the Exceptional algorithm to 𝒯 , ℰ2 , and Exceptional checks
that there are no more potential conflicts, and ℰ3 = ∅. (line 11). The empty set is trivially a fixed
point of our procedure. Now we have the exceptionality sequence {ℰ0 , ℰ1 , ℰ2 }. The algorithm uses
this sequence to assign a ranking value to each axiom in 𝒟 (line 18): all the axioms that are not
exceptional go into rank 0:

𝒟0 = ℰ0 ∖ ℰ1 = Bird ⊏ ⊏
∼ Fly, Bird ∼ Wings.
The axioms that are exceptional only w.r.t. ℰ0 go into rank 1 (𝒟1 ), and so on:

𝒟1 = ℰ1 ∖ ℰ2 = Penguin ⊏
∼ ¬Fly.
𝒟2 = ℰ2 ∖ ℰ3 = ℰ2 = SpecialPenguin ⊏
∼ Fly.

Now we move to Algorithm 2, that, given a knowledge base 𝒦 and a query 𝐶 ⊏ ∼ 𝐷, decides whether
𝒦 entails 𝐶 ⊏∼ 𝐷 under rational closure. The original algorithm is in [2, Sect. 5.2], and once again we
refer the reader to this publication for proper explanations and analysis. Here we simply go through
our guiding example, while pointing out the following about Algorithm 2:

• The symbol ℰ𝑖 indicates the materialisation of a set of defeasible axioms: given a set 𝒟 =
{𝐶1 ⊏∼ 𝐷1 , . . . , 𝐶𝑛 ∼ 𝐷𝑛 }, the set 𝒟 = {¬𝐶1 ⊔ 𝐷1 , . . . , ¬𝐶𝑛 ⊔ 𝐷𝑛 } is the set of concepts
⊏
expressing the implications that correspond to the defeasible subsumptions.
• Algorithm 2 is slightly different w.r.t. the Function RationalClosure in [2], since it returns not
only the answer to the query, but also a value 𝑖 that provides the exceptionality ranking of the
query. This information is needed for the creation of the justifications (see Section 2.3).

Example 4. Consider the rankings obtained in Example 3 with the query SpecialPenguin ⊏ ∼ Fly. The
rational closure algorithm starts with ℰ0 (line 2), and checks whether the antecedent in the query is in a
conflict w.r.t. ℰ0 . That is the case since (line 3):

l
𝒯 |= {¬Bird ⊔ Fly, ¬Bird ⊔ Wings, ¬Penguin ⊔ ¬Fly, ¬SpecialPenguin ⊔ Fly} ⊓ SpecialPenguin ⊑ ⊥

The algorithms goes on checking for increasing values of ℰ𝑖 (lines 3-4), until it finds an exceptionality
level s.t. SpecialPenguin is not part of any conflict. That is the case fo ℰ2 , since

𝒯 ̸|= (¬SpecialPenguin ⊔ Fly) ⊓ SpecialPenguin ⊑ ⊥
Now the algorithm associates the information in ℰ2 with the query, and checks whether the query is
implied using materialisation and classical DL reasoning (line 6). That is the case since

𝒯 |= (¬SpecialPenguin ⊔ Fly) ⊓ SpecialPenguin ⊑ Fly.
The algorithm returns true and the value 2 (the exceptionality level associated with the query).

Algorithm 2: RationalClosureForJustifications(𝒦, 𝛼)
Input: 𝒦 = 𝒯 ∪ 𝒟 and a query 𝛼 = 𝐶 ⊏ ∼ 𝐷.
Output: true if 𝐶 ⊏∼ 𝐷 is in the rat. clos. of 𝒦, false otherwise; and a rank value i
* * *
1 (𝒦 = 𝒯 ∪ 𝒟 , ℰ𝑠𝑒𝑞𝑢𝑒𝑛𝑐𝑒 = (ℰ0 , . . . , ℰ𝑛 )) ← ComputeRanking(𝒦)
2 𝑖←0
3 while 𝒯 * |=
d
ℰ𝑖 ⊓ 𝐶 ⊑ ⊥ and 𝑖 ≤ 𝑛 do
4 𝑖←𝑖+1
5 if 𝑖 ≤ 𝑛 then
return 𝒯 * |= ℰ 𝑖⊓𝐶 ⊑𝐷,i
d
6

7 else
8 return 𝒯 * |= 𝐶 ⊑ 𝐷, i
3. Defeasible Justification
We now define a procedure that calculates justifications for defeasible entailment:
ComputeDefeasibleJustifications. It is obtained by using RationalClosureForJustifications and
ComputeAllJustifications* as sub-procedures. ComputeAllJustifications* is a simple modification of
ComputeAllJustifications [1, Algorithm 4.1]. We will not present it here. It is sufficient to know that,
given 𝒦 = 𝒯 ∪ 𝒟 and a defeasible inclusion 𝐶 ⊏ ∼ 𝐷, dComputeAllJustifications* (𝒦, 𝐶 ⊏ ∼ 𝐷) returns
every minimal set 𝒥 = 𝒯 ∪ 𝒟 s.t. 𝒥 ⊆ 𝒦 and 𝒯 |= 𝒟 ⊓ 𝐶 ⊑ 𝐷.
′ ′ ′ ′

The algorithm first determines whether a particular query is in the rational closure of the knowledge
base (line 1), and only if it is the case, does it proceed to calculate the justifications (lines 3-15). From
RationalClosureForJustifications we know the rank 𝑖 that is associated to the query (line 6), and we
consider only the information in ℰ𝑖 to calculate the justifications using RationalClosureForJustifications
(lines 8 or 15, depending on the value of the rank 𝑖).

Example 5. Consider the defeasible knowledge base 𝒦 = 𝒯 ∪ 𝒟 from Example 2. In Example 4 we have
seen that SpecialPenguin ⊏
∼ Fly is defeasibly entailed by 𝒦. We see now how Algorithm 3 explains why
⊏
SpecialPenguin ∼ Fly is defeasibly entailed by 𝒦:

1. Line 1 checks whether SpecialPenguin ⊏ ∼ Fly is in the rational closure of 𝒦. From Example 4 we
know that it is the case, and the algorithm moves to line 3.
2. We initialise a variable i to 0 (line 4) and a set 𝒥𝑟𝑒𝑠𝑢𝑙𝑡 to an empty set (line 5). In line 6 we obtain
the value 𝑟𝑎𝑛𝑘 = 2, since, as we have seen in Example 4, SpecialPenguin is associated to ℰ2 . Due
to that, the If-statement block on lines 7-9 is skipped since 𝑟𝑎𝑛𝑘 > 0.
3. Once we obtain the ranking 𝑅 from ComputeRanking (line 11), the while-loop in lines 12-14 removes
axioms contained in 𝒟0 and 𝒟1 . Therefore, we can only use only axioms in 𝒟2 and in the TBox 𝒯 to
compute the justifications.
4. On line 15 we compute all the justifications for the query SpecialPenguin ⊏ ∼ Fly w.r.t 𝒯 ∪ 𝒟2 . The
only justification in 𝒥𝑟𝑒𝑠𝑢𝑙𝑡 is 𝒥1 = {SpecialPenguin ⊏ ∼ Fly}.

Algorithm 3: ComputeDefeasibleJustifications(𝒦, 𝜂)
Input: 𝒦 = 𝒯 ∪ 𝒟 and a query 𝜂 = 𝐶 ⊏ ∼ 𝐷.
Output: RationalClosureForJustifications(𝒦, 𝜂); the set of justifications 𝒥
1 if RationalClosureForJustifications(𝒦, 𝜂) = false then
2 return RationalClosureForJustifications(𝒦, 𝜂)
3 else
4 𝑖←0
5 𝒥𝑟𝑒𝑠𝑢𝑙𝑡 ← ∅
6 𝑟𝑎𝑛𝑘 ← value 𝑖 from RationalClosureForJustifications(𝒦, 𝜂)
7 if 𝑟𝑎𝑛𝑘 = 0 then
8 𝒥𝑟𝑒𝑠𝑢𝑙𝑡 ← ComputeAllJustifications* (𝒦, 𝜂)
9 return RationalClosureForJustifications(𝒦, 𝜂), 𝒥𝑟𝑒𝑠𝑢𝑙𝑡
10 else
11 𝑅 = {𝒟0 , . . .} ← 𝑅 from ComputeRanking(𝒦)
12 while 𝑖 < 𝑟𝑎𝑛𝑘 do
13 𝒦𝑛𝑒𝑤 ← 𝒦𝑛𝑒𝑤 ∖ 𝒟𝑖
14 𝑖←𝑖+1
15 𝒥𝑟𝑒𝑠𝑢𝑙𝑡 ← ComputeAllJustifications* (𝒦𝑛𝑒𝑤 , 𝜂)
16 return RationalClosureForJustifications(𝒦, 𝜂), 𝒥𝑟𝑒𝑠𝑢𝑙𝑡
We return to Example 1 given in Section 2.2. Recall that using the knowledge base in Example 1 there
are two justifications that support the query SpecialPenguin ⊑ Fly: 𝒥1 = { SpecialPenguin ⊑ Fly } and
𝒥2 = { SpecialPenguin ⊑ Penguin, Penguin ⊑ Bird, Bird ⊑ Fly }. Once converted the knowledge base to
the defeasible formalism (Example 2), the corresponding justification sets are 𝒥1 = { SpecialPenguin ⊏ ∼ Fly
} and 𝒥2 = { SpecialPenguin ⊑ Penguin, Penguin ⊑ Bird, Bird ⊏ ∼ Fly }. However, our algorithm eliminates
from the potential justifications all the axioms that have rank lower than 2, hence eliminating Bird ⊏ ∼ Fly,
that is required for 𝒥2 . Eventually, only justification 𝒥1 is eligible.
Everett et al. [24] extended the principle of justifications for both Relevant and Lexicographic Closure.

4. Implementation
In this section we present an implementation of Algorithm 3, but at the moment just for Propositional
Logic (PL)[25]. The original formulation of rational closure was for PL [7], and was developed in
the formal framework introduced by Kraus, Lehmann and Magidor (KLM) [6]. They use defeasible
conditionals 𝛼 |∼ 𝛽, where 𝛼 and 𝛽 are propositional formulas, and that are read as “if 𝛼, usually
𝛽”. A knowledge base in this framework is a finite set of defeasible implications and propositional
formulas. Since any propositional formula can be rewritten as a classical implication of the form 𝛼 → 𝛽
(trivially, 𝛼 can be rewritten as ⊤ → 𝛼 or ¬𝛼 → ⊥), a knowledge base in the KLM Framework can
be seen as a finite set of classical implications and defeasible implications. The correspondence with
our defeasible knowledge base in 𝒜ℒ𝒞, which is a finite set of classical subsumption statements and
defeasible subsumption statements, is quite immediate.

Example 6. The knowledge base below is the PL version of the knowledge base presented in Example 2.

𝒦 = {Penguin → Bird, Robin → Bird, SpecialPenguin → Bird, Bird |∼ Fly,
Bird |∼ Wings, Penguin |∼ ¬Fly, SpecialPenguin |∼ Fly}

The notion of defeasible entailment used in the previous sections in this paper fully corresponds
to rational closure in the propositional case, as shown by Britz et al. [23]. In other words, rational
closure in the propositional case is a simplified version of rational closure in the DL 𝒜ℒ𝒞 case. Similarly,
the defeasible justification algorithm in the propositional case (Algorithm 4) is a simplified version of
Algorithm 3. 𝒦→ and (𝛼 |∼ 𝛽)→ are obtained substituting every instance of a defeasible conditional
𝛼 |∼ 𝛽 with 𝛼 → 𝛽.

Algorithm 4: ComputePropositionalDefeasibleJustifications(𝒦, 𝛼 |∼ 𝛽)
Input: Defeasible knowledge base 𝒦 and query 𝛼 |∼ 𝛽
Output: the set of justifications 𝒥
1 𝑖←0
2 𝒥𝑟𝑒𝑠𝑢𝑙𝑡 ← ∅
3 𝑟𝑎𝑛𝑘 ← value 𝑖 from RationalClosureForJustifications(𝒦, 𝛼 |∼ 𝛽)
4 if 𝑟𝑎𝑛𝑘 = 0 then
5 𝒥 = ComputeAllJustifications(𝒦→ , (𝛼 |∼ 𝛽)→ )
6 return 𝒥
7 𝑅 = {𝒟0 , . . .} ← 𝑅 from ComputeRanking(𝒦)
8 while 𝑖 < 𝑟𝑎𝑛𝑘 do
9 𝒦𝑛𝑒𝑤 ← 𝒦𝑛𝑒𝑤 ∖ 𝒟𝑖
10 𝑖=𝑖+1
→ , (𝛼 |∼ 𝛽)→ )
11 𝒥 = ComputeAllJustifications(𝒦𝑛𝑒𝑤
12 return 𝒥
Example 7. If we run the algorithm with the knowledge base 𝒦 from Example 6 and the query
SpecialPenguin |∼ Fly, we obtain the result that corresponds to the one of Example 5, that is, the only justifi-
cation is {SpecialPenguin |∼ Fly}, while the potential justification {Penguin → Bird, SpecialPenguin →
Bird, Bird |∼ Fly} is not considered since the rank of Bird |∼ Fly is too low w.r.t. the query.

Wang et al. [25] provide more detailed examples of defeasible justification in the propositional case.
The software that implements the defeasible justification algorithm for the KLM frame-
work is coded in Java. We refer to the software tool as KLMDefeasibleJustificationTool. The
KLMDefeasibleJustificationTool follows the Model View Controller (MVC) software architecture pattern
and is composed of objects, a graphical user interface (GUI) and algorithm implementations. The GUI is
constructed using Java Swing packages. The KLMDefeasibleJustificationTool takes two input parameters:
a text file that consists of a KLM-style propositional knowledge base and a query string. The resulting
justification(s) and statement rankings are displayed in a text area of the GUI. Two external packages
are used to compute the defeasible justification: the Tweety Project [26, 27] and SAT4J SAT solver
[28, 29]. The Tweety Project is a software framework that provides models and operations for a number
of logics, including PL. Our implementation extends the PL models to construct models and operations
required by the KLM Framework. Due to the constraints defined by the Tweety Project, we cannot
denote the KLM Framework operations with conventional symbols. Instead, the negation symbol. ¬
is replaced with ! and the binary operations ∧, ∨, →, ↔ and |∼ are replaced with &&, ||, =>, <=>
and ∼>, respectively. Furthermore, we constructed a parser that reads strings such as “𝛼 ∼> 𝛽” and
produces an instance of DefeasibleImplication, which allows the software to perform operations such
as materialisation. Classical entailment computation is needed as a sub-procedure to the defeasible
justification calculations. The SAT4J SAT solver is used to compute this.
The source code of the defeasible justification tool for the KLM Framework can be found on Github
[30].

5. Conclusion
The two main contributions of this paper are: (i) a defeasible justification algorithm for the DL 𝒜ℒ𝒞 and
(ii) an implementation of the defeasible justification algorithm in the propositional case. The obvious
next step is to provide an implementation of the defeasible justification algorithm for 𝒜ℒ𝒞 as a Protégé
plugin. Further future work includes the definition and implementation of defeasible justification
algorithms for other logics equipped with KLM-style defeasibility. One such logic is the restricted
version of first-order logic with KLM-style defeasibility presented by Casini et al. [31]. Finally, here
we have focused on a procedural definition of defeasible justification in the form of Algorithm 3. An
investigation into a declarative definition of defeasible justification is left as future work.

Acknowledgments
This work has been partially supported by the H2020 STARWARS Project (GA No. 101086252), a type
of action HORIZON TMA MSCA Staff Exchanges.

References
[1] M. Horridge, Justification based explanation in ontologies, PhD Thesis, University of Manchester,
2011.
[2] K. Britz, G. Casini, T. Meyer, K. Moodley, U. Sattler, I. Varzinczak, Principles of KLM-style
Defeasible Description Logics, ACM Transactions on Computational Logic (TOCL) 22 (2020) 1 –
46. doi:10.1145/3420258.
[3] G. Casini, T. Meyer, K. Moodley, U. Sattler, I. Varzinczak, Introducing defeasibility into OWL
ontologies, in: International Semantic Web Conference, Springer, 2015, pp. 409–426.
[4] S. P. Bail, The justificatory structure of OWL ontologies, PhD Thesis, University of Manchester,
2013.
[5] J. L. Pollock, A theory of defeasible reasoning, International Journal of Intelligent Systems 6 (1991)
33–54.
[6] S. Kraus, D. Lehmann, M. Magidor, Nonmonotonic reasoning, preferential models and cumulative
logics, Artificial intelligence 44 (1990) 167–207.
[7] D. Lehmann, M. Magidor, What does a conditional knowledge base entail?, Artificial Intelligence
55 (1992) 1–60.
[8] L. Giordano, V. Gliozzi, N. Olivetti, G. L. Pozzato, Semantic characterization of rational closure:
From propositional logic to description logics, Artificial Intelligence 226 (2015) 1–33. URL: https:
//doi.org/10.1016/j.artint.2015.05.001. doi:10.1016/J.ARTINT.2015.05.001.
[9] P. A. Bonatti, Rational closure for all description logics, Artificial Intelligence 274 (2019) 197–223.
URL: https://doi.org/10.1016/j.artint.2019.04.001. doi:10.1016/J.ARTINT.2019.04.001.
[10] M. Schmidt-Schauß, G. Smolka, Attributive concept descriptions with complements, Artificial
intelligence 48 (1991) 1–26.
[11] F. Baader, D. Calvanese, D. McGuinness, P. Patel-Schneider, D. Nardi, The Description Logic
Handbook: Theory, Implementation and Applications, 2 ed., Cambridge university press, 2007.
[12] F. Baader, R. Penaloza, Axiom pinpointing in general tableaux, Journal of Logic and Computation
20 (2010) 5–34.
[13] K. Moodley, T. Meyer, I. J. Varzinczak, A defeasible reasoning approach for description logic
ontologies, in: Proceedings of the South African Institute for Computer Scientists and Information
Technologists Conference, ACM, 2012, pp. 69–78.
[14] L. Botha, T. Meyer, R. Pẽnaloza, The Probabilistic Description Logic ℬ𝒜ℒ𝒞, Theory and Practice
of Logic Programming (2020). doi:10.1017/s1471068420000460.
[15] P. Ke, U. Sattler, Next Steps for Description Logics of Minimal Knowledge and Negation as Failure,
Description Logics 353 (2008).
[16] L. Giordano, V. Gliozzi, A reconstruction of multipreference closure, Artificial Intelligence 290
(2021) 103398. URL: https://doi.org/10.1016/j.artint.2020.103398. doi:10.1016/J.ARTINT.2020.
103398.
[17] P. A. Bonatti, C. Lutz, F. Wolter, Description Logics with Circumscription., in: KR, 2006, pp.
400–410.
[18] P. A. Bonatti, M. Faella, I. M. Petrova, L. Sauro, A new semantics for overriding in description
logics, Artificial Intelligence 222 (2015) 1–48. URL: https://doi.org/10.1016/j.artint.2014.12.010.
doi:10.1016/J.ARTINT.2014.12.010.
[19] D. Lehmann, Another Perspective on Default Reasoning, Annals of Mathetics and Artificial Intel-
ligence 15 (1995) 61–82. URL: https://doi.org/10.1007/BF01535841. doi:10.1007/BF01535841.
[20] G. Casini, U. Straccia, Defeasible Inheritance-Based Description Logics, J. Artificial Intelligence
Res. 48 (2013) 415–473. URL: https://doi.org/10.1613/jair.4062. doi:10.1613/JAIR.4062.
[21] G. Casini, T. Meyer, I. Varzinczak, Taking Defeasible Entailment Beyond Rational Closure, in:
F. Calimeri, N. Leone, M. Manna (Eds.), Logics in Artificial Intelligence - 16th European Conference,
JELIA 2019, Rende, Italy, May 7-11, 2019, Proceedings, volume 11468 of Lecture Notes in Computer
Science, Springer, 2019, pp. 182–197. URL: https://doi.org/10.1007/978-3-030-19570-0_12. doi:10.
1007/978-3-030-19570-0\_12.
[22] G. Casini, U. Straccia, Rational closure for defeasible description logics, in: European Workshop
on Logics in Artificial Intelligence, Springer, 2010, pp. 77–90.
[23] K. Britz, G. Casini, T. Meyer, I. Varzinczak, A KLM Perspective on Defeasible Reasoning for
Description Logics, in: Description Logic, Theory Combination, and All That, Springer, 2019, pp.
147–173.
[24] L. Everett, E. Morris, T. Meyer, Explanation for klm-style defeasible reasoning, in: Southern
African Conference for Artificial Intelligence Research, Springer, 2021, pp. 192–207.
[25] S. Wang, T. Meyer, D. Moodley, Defeasible Justification Using the KLM Framework, in: Southern
African Conference for Artificial Intelligence Research, Springer, 2022, pp. 187–201.
[26] M. Thimm, Tweety - A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial
Intelligence and Knowledge Representation, in: Proceedings of the 14th International Conference
on Principles of Knowledge Representation and Reasoning (KR’14), 2014, pp. 528–537.
[27] M. Thimm, The Tweety Project, Available online, 2014. URL: https://tweetyproject.org/.
[28] N. Eén, N. Sörensson, An extensible SAT-solver, in: International conference on theory and
applications of satisfiability testing, Springer, 2003, pp. 502–518.
[29] N. Eén, N. Sörensson, SAT4J SAT Solver, 2003. URL: https://www.sat4j.org/index.php.
[30] S. Wang, GitHub - KLM Defeasible Justification Tool, Available online, 2023. URL: https://github.
com/SteveWang7596/DefeasibleJustificationForPropositionalLogic.
[31] G. Casini, T. Meyer, G. Paterson-Jones, I. Varzinczak, KLM-Style Defeasibility for Restricted
First-Order Logic, in: International Joint Conference on Rules and Reasoning, Springer, 2022, pp.
81–94.