Symbolic AI approaches based on logic are inherently explainable-conclusions derived via automated reasoning can be traced through proofs showing step-by-step inference from axioms. Every inference step in symbolic reasoning carries explicit semantic meaning, enabling full transparency. However, to fully benefit from this, proofs must serve as efective explanations while remaining understandable. In ongoing work, we address these issues in the context of Description Logics (DLs) [1], proofs [2, 3] and our interactive visualization tool Evonne1 [4, 5]. In this paper, we concentrate on the extension of the proof visualization facilities of Evonne to DLs with so-called concrete domains (CDs) [6, 7]. In particular, we consider extensions of tractable DLs of the ℰ ℒ family [8] with two p-admissible concrete domains based on rational numbers, one (Q,lin) that can use linear equations to formulate constraints [9] and another (Q,dif ) based on diference constraints [ 10]. Such numerical constraints are useful for describing concepts whose definition involves quantitative information, as in the following examples. Example 1. For a delivery drone, its current battery percentage is measured at checkpoints, denoted as 1 and 2. Additionally, the following safety constraints are imposed: 1 − 0.2 = 2, 1 > 0.3 and 2 > 0.25. If the initial percentage (1) equals 0.4, then not all the constraints hold, and the drone is not permitted to fly-see Figure 1a. Example 2. Assume and ℎ represent the average normal and high battery discharge rates. Under normal conditions, the delivery drone (DD) can fly for 8 hours on a single charge with a 30Ah battery, i.e., 8 = 30. In cold conditions, one hour of flight increases the battery consumption such that 4 + ℎ = 30. Next, if a system consumes 30Ah in two hours at a high discharge rate, it qualifies as a large battery drone (LBD), i.e., [2ℎ = 30] ⊑ LBD. Given these constraints, it follows that the delivery drone is a large battery drone, i.e., DD ⊑ LBD-see the combined proof in Figure 1b, where the proof in Figure 1c shows the Q,lin inferences.
(a) Q,dif proof from Example 1 (b) Combined proof from Example 2 (c) Expanding CDP1 in (b) semantics [8, 9]. An implication is of the form C → , where is a constraint, i.e., a predicate with variables as arguments, and C is a set of constraints. The implication is valid if all variable assignments satisfying all constraints in C also satisfy . A set C is unsatisfiable if C → ⊥ is valid.
In [10], we have theoretically addressed the problem of generating proofs for consequences derived from knowledge bases formulated in such DLs. Here we contribute the practical proof visualization tool supporting DLs with linear equations and diference constraints.
This work introduces novel visual explanations for unsatisfiability and entailment in the considered CDs, designed to reflect their unique properties and ofer more intuitive insight into the underlying numerical reasoning.
Case Q,lin. If we consider systems of linear equations with at most two variables, which are shared across all equations, then we can use lines in the 2D Euclidean Space to achieve a compact representation of all solutions to the equations, as each solution corresponds to a point in the 2D space. Using dimensionality reduction, we can apply the same idea to equations with more than two variables. Let C be a set of equations where C → holds, let be a solution to C, and let and be any two variables appearing in . By replacing all the variables, except and , in all equations with their corresponding values in , we obtain equations involving at most two variables. Therefore, in the -plane all the lines must intersect in the same point. To explain unsatisfiability, we can use a similar approach.
Figure 2 shows examples of Q,lin explanations in Evonne. Users can toggle between planes and assign values to free variables. The equation system appears top-left, with current variable assignments shown top-right. Since the system in Figure 2a has one degree of freedom, setting 4 = 0 uniquely determines the remaining variables. In contrast, in Figure 2b, the top right shows the system of (a) Implication of 31 − 3 2 − 3 + 34 = 7 (b) Implication of ⊥ equations with respect to the currently chosen variable assignment. In this case the visualization makes contradictions immediately apparent—as demonstrated by the highlighted contradiction 3 = 0. Case Q,dif . It is well established [11] that diference constraints (i.e., − ≤ ) can be represented as weighted directed graphs such that every variable corresponds to a vertex and every constraint to a weighted edge between and labelled by . Given a set of diference constraints, deciding whether it is unsatisfiable can be reduced to finding a simple cycle in the corresponding graph with a negative weight [11].
We show how to rewrite all types of constraints in Q,dif into diference constraints. Thus, we can represent any set C of Q,dif constraints as a diference graph, and if C → ⊥, we can explain the contradiction in C by identifying the negative cycle in the graph. In the case when C is satisfiable and C → , we can explain the implication by showing that C ∪ {¬} → ⊥ , which allows us to efectively use the notion of negative cycles.
Figure 3 shows a screenshot of a negative cycle in Evonne. In the implementation, the cycle is animated, allowing users to visually follow its progression. Additionally, users can assign concrete values to variables. These values are then automatically propagated along the negative cycle, allowing users to observe how the set of constraints behaves under such assignments. In particular, this makes it possible to see exactly how the cycle leads to logical inconsistencies, which are highlighted in red, e.g., 3 = 3 ≤ 3 − .
Empirical Evaluation. We conducted an empirical validation through user studies and benchmarks, to demonstrate the efectiveness of our approach. The creation of these visualizations remains performant (under 200ms) with the largest proofs in our experiment, and the studies revealed areas of improvement for the visualization of proofs and our alternative CD explanations. The current version of Evonne is accessible through https://imld.de/evonne, further details of our evaluation results are also available there.
The latest extension of Evonne enables interactive visualization of proofs for DLs with concrete
domains—crucial for modeling concepts involving quantitative constraints. This extension contributes:
(
This work is funded by DFG under Germany’s Excellence Strategy: EXC 2050/1, 390696704 – “Centre for Tactile Internet” (CeTI); by DFG grant 389792660 as part of TRR 248 – CPEC; and by BMBF and Saxon State Ministry for Science, Culture and Tourism (SMWK) in Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI, SCADS22B).
During the preparation of this work, the authors used ChatGPT-4 [https://chat.openai.com/] and DeepSeek-V3 [https://chat.deepseek.com/] in order to: Grammar and spelling check, Paraphrase and reword. After using these services, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. International Conference on Automated Deduction 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, Springer, 2021, pp. 291–308. doi:10.1007/978-3-030-79876-5\_17. [4] C. Alrabbaa, F. Baader, S. Borgwardt, R. Dachselt, P. Koopmann, J. Méndez, Evonne: Interactive proof visualization for description logics (system description), in: Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, Springer, 2022, pp. 271–280. doi:10.1007/978-3-031-10769-6\_16. [5] J. Méndez, C. Alrabbaa, P. Koopmann, R. Langner, F. Baader, R. Dachselt, Evonne: A visual tool for explaining reasoning with OWL ontologies and supporting interactive debugging, Comput.
Graph. Forum 42 (2023). doi:10.1111/CGF.14730. [6] F. Baader, P. Hanschke, A scheme for integrating concrete domains into concept languages, in: Proceedings of the 12th International Joint Conference on Artificial Intelligence. Sydney, Australia, August 24-30, 1991, Morgan Kaufmann, 1991, pp. 452–457. URL: http://ijcai.org/Proceedings/91-1/ Papers/070.pdf. [7] C. Lutz, Description logics with concrete domains-a survey, in: Advances in Modal Logic 4, papers from the fourth conference on "Advances in Modal logic," held in Toulouse, France, 30 September - 2 October 2002, King’s College Publications, 2002, pp. 265–296. URL: http://www.aiml. net/volumes/volume4/Lutz.ps. [8] F. Baader, S. Brandt, C. Lutz, Pushing the EL envelope, in: IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30 - August 5, 2005, Professional Book Center, 2005, pp. 364–369. URL: http://ijcai.org/Proceedings/05/Papers/ 0372.pdf. [9] F. Baader, J. Rydval, Using model theory to find decidable and tractable description logics with concrete domains, J. Autom. Reason. 66 (2022) 357–407. doi:10.1007/s10817-022-09626-2. [10] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Combining proofs for description logic and concrete domain reasoning, in: Rules and Reasoning - 7th International Joint Conference, RuleML+RR 2023, Proceedings, volume 14244 of Lecture Notes in Computer Science, Springer, 2023, pp. 54–69. doi:10.1007/978-3-031-45072-3_4. [11] T. Cormen, C. Leiserson, R. Rivest, C. Stein, Introduction to Algorithms, third edition, Computer science, MIT Press, 2009. URL: https://books.google.de/books?id=i-bUBQAAQBAJ.