Research in description logics (DLs) and formal ontologies has dedicated quite an efort 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 efort 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.
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.
lfy”. 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 [
Conclusions produced by reasoning tools are often dificult 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 [
[7], but has also been lifted to the case for DLs [
computes explanations for conclusions produced by reasoning services. After a brief introduction to the
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 ℒ
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 ifnite 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].
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 [
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, ⎫ ⎨⎪⎪⎪⎪⎪⎪⎪⎪ SpePcBeinairlgdPue⊑inngW⊑uiin¬ngF⊑sly,F,ly, ⎪⎪⎪⎬⎪⎪⎪⎪⎪ ⎪⎪⎪ 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.
what follows we will refer to it as Algorithm ComputeAllJustifications(Algorithm 4.1), that, given a
2.3. Defeasible Reasoning
enables us to reason with rules and generalisations that model typical scenarios that admit exceptions.
There is existing work for extending description logics with defeasible reasoning [
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 ⊑ [
Penguin ⊑ Bird,
Robin ⊑ Bird
⎩SpecialPenguin ⊑ Penguin⎭
⎧⎪⎨⎪ BBirdir d⊏∼⊏∼WFinlyg,s, ⎫⎪⎪⎬
⎪ 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. [
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,
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):
1Note 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 [
Input: = ∪ Output: * = * ∪ * , an exceptionality sequence ℰ0, . . . , ℰ and a partitioning = {0, . . . , } for * 1 * ← 2 * ← 3 ← ∅ 4 repeat 5 ← 6 7 8 9 10 − 1 ← ℰ − 1 ∖ ℰ ← ∪ {− 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 lfy, 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 (line 11): ℰ2 ℰ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 diferent w.r.t. the Function RationalClosure in [
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). 1 (* = * ∪ * , ℰ = (ℰ0, . . . , ℰ)) ← 2 ← 0 3 while * |= d ℰ ⊓ ⊑ ⊥ and ≤ do 4 ← + 1 5 if ≤ then 6 return * |= d ℰ ⊓ ⊑ , i
return * |= ⊑ , i
Input: = ∪ and a query = ⊏∼ .
Output: true if ⊏∼ is in the rat. clos. of , false otherwise; and a rank value i ComputeRanking()
ComputeDefeasibleJustifications. It is obtained by using RationalClosureForJustifications and ComputeAllJustification s* as sub-procedures. ComputeAllJustification s* is a simple modification of
given = ∪ and a defeasible inclusion ⊏∼ , ComputeAllJustification s* (, ⊏∼ ) returns every minimal set = ′ ∪ ′ s.t. ⊆ and ′ |= d ′ ⊓ ⊑ .
base (line 1), and only if it is the case, does it proceed to calculate the justifications (lines 3-15). From
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}.
Input: = ∪ and a query = ⊏∼ .
Output: RationalClosureForJustifications(, ); the set of justifications 1 if RationalClosureForJustifications(, ) = false then 2 return RationalClosureForJustifications(, ) ←
0 3 else 4 5 6 7 8 9 = {0, . . .} ← from ComputeRanking() while < do ← ← ∖
+ 1 ← ComputeAllJustification s* (, ) 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.
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}
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
|∼ with → .
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 justification 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.
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 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.
[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:
//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
[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
[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 Intelligence 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:
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
147–173. [24] L. Everett, E. Morris, T. Meyer, Explanation for klm-style defeasible reasoning, in: Southern
[25] S. Wang, T. Meyer, D. Moodley, Defeasible Justification Using the KLM Framework, in: Southern
[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
81–94.