ABSTRACT. Many techniques have been developed to explain logical reasoning, such as proofs or abduction. However, such methods are useful mainly for experts in logic, e.g., for debugging ontologies. For actually explaining logical consequences and missing consequences to end users of logic-based systems, e.g., in the Semantic Web, it is necessary to study how to adapt and present such explanations in an understandable way. We report on a series of user studies investigating both entailment explanations via proofs and missing entailment explanations via abduction and counterexamples in the context of Description Logic (DL) ontologies. For the former, we assess the influence of prior knowledge on the necessary explanation granularity; for the latter, we compare the efficacy of abductive versus counterexample-based approaches. While we did not find objectively quantifiable results, we analyse and discuss the results of detailed qualitative user interviews, and extract recommendations for executing user studies on logical reasoning systems.

ABSTRACT. This abstract is for a paper published in 2025 in the proceedings of the 14th International Joint Conference on Natural Language Processing and the 4th Conference of the Asia-Pacific Chapter of the Association for Computational Linguistics, and we extend it here with a new study that closes the gap with previous research. Large language models (LLMs) are increasingly applied in domains that demand reliable and interpretable reasoning. While formal reasoning methods can generate correct proofs, these proofs are often inaccessible to non-expert users. This raises a natural question: Can LLMs, when given a proof, faithfully interpret its reasoning and communicate it clearly? Recently, we have introduced \texttt{ProofTeller}, a benchmark that evaluates this ability across three tasks: (1) identifying key proof steps, (2) summarizing the reasoning, and (3) explaining the result in concise natural language. The benchmark covers three domains: \emph{Biology}, \emph{Drones}, and \emph{Recipes}, representing scientific, safety-critical, and everyday reasoning scenarios. We find a consistent near-conclusion bias: LLMs tend to focus on steps closest to the final proof conclusion rather than on the most informative ones. A targeted human study confirms that explanations based on such steps are rated less appropriate for end users. These findings indicate that even when reasoning is provided, current LLMs face challenges in communicating key information in a useful manner, highlighting the need for LLMs that can communicate important details reliably.

ABSTRACT. Abduction is a central approach to explain missing entailments from a knowledge base by providing a hypothesis, that would, if added to the knowledge base, make the missing entailment become true. Abduction under repair semantics has recently been investigated in detail, where several desirable properties and optimality criteria were considered, such as signature-restrictions and minimality in size and of introduced conflicts. Naturally, hypotheses that satisfy more than one of these properties or combine a property with an optimality criterion would be even more desirable for applications. So far, such hypotheses have not been investigated in the literature. In the present paper, we consider the ABox abduction problem for hypotheses satisfying more than one property or additional optimality criteria, for EL_bot under brave and AR semantics. Our main observation is that often requiring additional properties for hypotheses does not lead to an increase of complexity.

ABSTRACT. The need for explanations to predictions in knowledge graphs is increasing because they are generally computed via embedding-based methods that are efficient, but do not explain predictions. Many explanation methods rely on axioms in the knowledge graph that are incomplete, thus often making the explanations incomplete. One way to address this gap is to consider, for explanations, hypothetical knowledge at the schema or assertion level. However, methods based on hypothetical assertions often ignore existing facts. Conversely, approaches that enrich explanations via rule learning typically disregard the available schema. We propose LPX-AbPoint, the first method using a combination of abduction and pinpointing techniques to compute explanations consisting of both schema axioms and existing or hypothetical assertions. We present a comparative empirical study showing that our method produces more useful explanations than approaches relying solely on observed knowledge, while remaining complementary to rule learning techniques.

ABSTRACT. One way of enhancing link prediction in knowledge graphs in an interpretable and trustworthy way is to use ontology embeddings. These embeddings translate a knowledge graph together with its background ontology into a vector space by representing concepts as convex sets and logical operators between these concepts as geometric operations between the resp. sets. This allows for using both geometric regularities and background knowledge for learning. Some fragments of the description logic ℰℒ++ such as ℰℒℋ𝒪(○)^\bot are particularly well-suited as a basis for an embedding, as they offer a good trade-off between expressiveness and complexity. One popularapproach for embedding these ontologies is to interpret concepts as boxes in some R^n. Although box embeddings proved to be particularly useful in this context, they are not able to represent every ontology correctly. In this work, we open the door to a new geometric framework by introducing prism embeddings. Firstly, we show that prisms do not suffer from the same restrictions as boxes. To illustrate this advantage, we present concrete ontology examples that are problematic for box embeddings but can be represented using prisms. Secondly, we show that prism embeddings extend box embeddings in the sense that each box interpretation of an ℰℒℋ𝒪(○)^\bot ontology induces a prism interpretation, though possibly at the cost of an increase in dimensionality of at most two. Finally, we discuss the usage of prism embeddings in practice by sketching adaptations of implementations of box-based embedding approaches to the prism case.

ABSTRACT. We study TEL^o , an extension of the description logic EL with the temporal operator O^n (‘in n instants from now’),by encoding its canonical models with sets of integers. We characterise reasoning in TEL^o in terms of operations on such sets and arrive at a correspondence between (fragments of) TEL^o and (classes of) resolved systems of equations over sets of integers. This generalises the previously established link between TEL^o and formal grammars, leading to simpler proofs of known results as well as yielding new results.

ABSTRACT. Bipolar disorder is a condition characterised by episodes of extreme mood fluctuation. Effective treatment typically includes psychoeducation, which aims to equip patients with the knowledge needed to make informed decisions that can influence the course of their illness. Key to this process is the ability to monitor the patient’s behaviour (both by patients themselves and involved healthcare specialists) in order to recognise early signs of future episodes. To support this monitoring task, we propose a framework grounded in medical ontologies and metric interval temporal logic (MITL). The framework enables monitoring of patient behaviour and the identification of emerging episodes based on behavioral patterns and established clinical guidelines. This work is the abstract of a paper accepted at the Semantic Technologies for Data Management workshop (ST4DM 2026), outlining the formal foundations of the framework and describes future steps towards its adoption in practice.

ABSTRACT. Temporal extensions of description logics often lead to a substantial increase in the complexity of reasoning. Nevertheless, tractable extensions of ℰℒ have been developed by restricting the occurrences of temporal concepts. One can even add so-called convex metric temporal diamond operators to ℰℒ, if they are only allowed to occur on the left-hand side of concept inclusions. In this paper, we consider the dual convex box operators for the first time, and investigate the behavior of complex temporal formulas in which convex diamond and box operators can be combined via composition, union and intersection. We demonstrate the intricate interplay between these operators, and present decision procedures for checking subsumption between complex temporal formulas.

ABSTRACT. We investigate a formula-based approach for updating ABoxes in DL-Lite (ℋℱ) horn, a description logic that enjoys a low computational complexity of reasoning. Specifically, we extend the existing coherence update semantics from DL-Lite (ℋℱ) core to deal with conjunctions on the left-hand side of TBox axioms, which introduce ambiguity in the update result. We address this problem by proposing the new prioritized coherence update semantics that employs rankings over conjuncts to select among competing updates while preserving the central properties of minimal change, syntax independence, and uniqueness. We further show that updated ABoxes can be computed via a stratified Datalog¬ program based on a novel consequence-based calculus. The approach runs in polynomial time, matching the complexity of standard reasoning in DL-Lite (ℋℱ) horn.

ABSTRACT. The literature on ontology-mediated query answering (OMQA) has been shaped by two key results: first-order rewritability for DL-Lite, and PTime hardness of data complexity for essentially every description logic beyond it. This has effectively positioned DL-Lite as the only practical choice for query rewriting, restricting OMQA solutions to first-order queries and ontologies that can be rewritten into them. This AC0--PTime dichotomy is especially limiting if we consider that OMQA targets graph-structured data, and that standard graph query languages (including the recent ISO standards GQL and SQL/PGQ) are typically NL-complete. Towards identifying a rich Horn DL that can be rewritten into graph query languages and that can still express many ELI and DL-Lite ontologies, we introduce a stratification mechanism for ELI^\bot that controls the interaction between conjunction and recursion. In this way, we obtain ELI^\bot_\preceq, a description logic that strictly extends the core DL-Lite, supports reachability axioms and restricted conjunction, and allows for reasoning in NL. We establish the NL upper bound via a rewriting into nested two-way regular path queries, a fragment of GQL, providing initial evidence that our ontology language is a promising candidate for extending OMQA to graph query languages.

ABSTRACT. In this extended abstract, we summarize our recent work (to appear at KR 2026) on the complexity of deciding whether a given fact is relevant to a Boolean conjunctive query (CQ), i.e. whether the fact belongs to some minimal subset of the data that makes the query hold. Despite being of central importance to query answer explanation, the combined complexity of deciding query relevance has not been studied in detail, leaving open what makes this problem hard, and which restrictions can yield lower complexity. Relevance has previously been shown to be harder than query evaluation: namely, Sigma^p_2-complete for CQs, even over a binary signature. We further observe that NP-hardness applies already to (acyclic) chain CQs. Our work identifies self-joins (multiple atoms with the same relation) as the culprit. Indeed, we prove that if we forbid or bound the occurrence of self-joins, then relevance has the same complexity as query evaluation, namely, NP (without structural restrictions) and LogCFL (for bounded hypertreewidth classes). In the ontology setting, we establish an analogous result for ontology-mediated queries consisting of a CQ and DL-Lite_R ontology, namely that relevance is no harder than query answering provided that we bound the interaction width (which generalizes both self-join width and a recently introduced ‘interaction-free’ condition). Our results thus provide useful insights into what makes relevance harder than query evaluation and allow us to identify natural classes of queries which admit efficient relevance computation.