ABSTRACT. Light-weight description logics like EL have been successfully used to represent the terminological knowledge of many application domains. Yet, identifying the characteristics of instances often requires sub-symbolic approaches. We introduce a neuro-symbolic extension of EL which allows for (neural) perception and classification of properties, accompanied by formal (symbolic) reasoning based on these perceptions. Through a prototypical implementation, based on a reduction to logic programming, we show that inferences and learning are effectively achievable. This is an extended abstract for a paper accepted for publication at KR 2026.

ABSTRACT. Whether carefully engineered or automatically learned, ontologies may still contain modeling errors. The problem of repairing Description Logic (DL) ontologies has been extensively studied, with a primary focus on minimizing information loss. A given ontology may have many different repairs that minimize information loss, and thus domain knowledge is needed to find the one that is correct in the given application domain. Consequently, interactive approaches have been proposed that involve users in the repair process, with the aim of reducing the number of user decisions required to obtain a valid repair. These methods usually assume that users are always able to make definitive decisions. However, users may face situations where the semantics of axioms alone are insufficient for them to determine whether an axiom should be retained or removed. In this work, we introduce an interactive repair approach that not only guides users through the exponential space of possible repairs while minimizing the decisions required, but also provides support in cases of uncertainty. Our approach augments the repair process with several decision-support features, including information about important entailments, distance to reachable repairs, and structural differences in the class hierarchy. We have implemented this approach both as a standalone command-line tool and as a web-based interactive visualization prototype that provides analytical capabilities not easily achievable otherwise.

ABSTRACT. CATS is a JFact-based ABox abduction solver that implements three classical complete approaches: Reiter’s minimal hitting set algorithm and its more recent variants HS-Tree and RC-Tree. In addition, it provides fast but incomplete methods, namely QuickXplain and MergeXplain, as well as hybrid variants in which the complete algorithms are ``boosted'' using MergeXplain. This hybrid strategy is theoretically motivated and is expected to provide significant performance advantages for specific classes of inputs, as suggested by earlier preliminary results. In this work, we report on the recently implemented optimizations and on the first empirical evaluation conducted on three real-world ontologies, enabling a comparison of all eight implemented algorithms. Among other insights, it shows a decisive advantage of the hybrid methods over all three baselines on all classes of inputs.

ABSTRACT. We present the HS-Tree Visualizer application, a visualization tool under development that currently supports displaying MHS and MHS-MXP trees from input JSON files produced by an abduction solver. The application supports step-by-step simulation of the algorithms, interactive manipulation of tree nodes and edges, and the ability to display or hide additional details, including branches that do not lead to explanations. These features make it a useful tool for learning, algorithm analysis, and debugging the underlying solver. In the future, the application will be extended to support additional abduction algorithms, and it also has the potential to be used by other abduction solvers. With further updates, it could even be adapted for other processes that can be represented using a tree/graph structure, as long as a suitable JSON file in the required format is provided.

ABSTRACT. Enriching an ontology with complex axioms enables the inference of new knowledge, contextualized querying, and consistency checking, but it is error-prone and time-consuming. A further challenge is that domain experts are rarely ontology engineers, while ontology engineers often lack sufficient domain knowledge. This "knowledge acquisition bottleneck" has led to a prevalence of inexpressive ontologies, highlighting the need to facilitate the acquisition of expressive description logic axioms. In this work, we propose a domain-independent text annotation schema that maps directly to OWL DL syntax, enabling the algorithmic generation of expressive axioms from the annotations. Annotated text allows domain experts to participate in the loop, ensuring the trustworthiness of the resulting knowledge base. Additionally, the annotation process can later be automated using NLP once a sufficient number of annotations have been completed. We demonstrate the applicability and scalability of the approach through two distinct use cases: building requirements and scientific claims.

ABSTRACT. It is well known that satisfiability for the modal logic K, with multiple modalities, is a notational variant of concept satisfiability in the description logic ALC. Likewise, extensions of K are notational variants of more expressive description logics. This close relationship extends to their reasoning tasks and is well understood. The same cannot be said for Quantified Boolean Formulas and Modal/Description Logic: despite their reasoning tasks belonging to the same complexity class, reasoners for QBF and K have been developed and investigated mostly separately. While there have been some attempts at using QBF solvers to solve modal logic formulae, such attempts were made before recent significant optimisations of QBF reasoners and have not resulted in a good understanding of the relationship between measures of difficulty in both logics, particularly the polynomial hierarchy division of classes of modal formulae. We define a translation from satisfiable K formulae to true closed QBF, with an optimisation to close the gap in understanding of how the polynomial hierarchy relates to modal logic - and consequently concept satisfiability in ALC. We empirically evaluate our translation together with a modern QBF reasoner, depQBF, against native state-of-the-art modal logic reasoners. We show that the translation-based reasoner compares very favourably, in some cases vastly outperforming the native reasoners.

ABSTRACT. Earth Observation (EO) data publication and dissemination continues to grow driven by the need to consistently monitor the earth in times of climate change. openEO is one of the most well known APIs to query and process EO data and is operationally available on many EO cloud platforms such as the Copernicus Data Space Ecosystem or Destination Earth. To be truly valuable, EO data often needs to be combined with other data sources, notably relational databases. Knowledge graphs offer a way to bridge the semantic gap between EO data and these other sources. An unsolved issue with this solution is that the execution of integrated queries can be costly due to the enormous volume of EO data. In this paper, we tackle this challenge through the use of Virtual Knowledge Graphs — a paradigm that presents data to end-users as a knowledge graph, while being kept its original sources and formats. Our approach is prototyped and evaluated against multiple real-world openEO examples.

ABSTRACT. We clarify the complexity of answering unions of conjunctive queries over knowledge bases formulated in the description logic S, the extension of ALC with transitive roles. Contrary to what existing partial results suggested, we show that the problem is in fact 2ExpTime-complete; hardness already holds in the presence of two transitive roles and for Boolean conjunctive queries. We complement this result by showing that the problem remains in coNExpTime when the input query is rooted or is restricted to use at most one transitive role (but may use arbitrarily many non-transitive roles).

ABSTRACT. Propositional Dynamic Logic (PDL), known in the Description Logic community as ALCreg, is a well-established modal logic of programs. To increase its expressive power, several extensions have been proposed. One such extension is the loop operator, which expresses that an element can reach itself via a path defined by a regular expression. Although the satisfiability problem for LoopPDL is well understood, the decidability of its finite satisfiability problem has remained open for over 40 years. Our ongoing work aims to resolve this question. While a full solution is still pending, we have obtained some results of independent interest. In this workshop paper, we present a simplified version of our approach, applied to a logic with loops restricted to atomic roles and their transitive closures.

ABSTRACT. A central reasoning task in description logics is concept subsumption, which has been extensively studied, although important open problems remain for certain logics. In this work, we investigate subsumption in the restricted logic FL_⊥reg and related logics FL_reg, FL_⊥, and FL_0. These logics support value restrictions over role names, where the subscript "reg" indicates the use of regular expressions over roles. We show that deciding subsumption between two concept descriptions in FL_⊥reg and FL_reg is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. Our results are obtained via a novel reduction to parity pushdown games.

ABSTRACT. We introduce a general variety of equality-generating dependencies based on tree descriptions (TDs) for an expressive dialect of the FunDL family of description logics called tree description dependencies (TDDs). In general, TDDs enable capturing equality generating dependencies in an ontology. The new capability is tailored to structurally matching parts of structured documents/JSON objects. We show that logical entailment for this new FunDL dialect is complete for EXPTIME if a given ontology appeals to an exclusive use of TDDs, but that logical entailment becomes undecidable when more coarse grained varieties of TDDs (called Path Description Dependencies, PDDs) are simultaneously allowed in the ontology. An extension to a referring expression type language for defining concepts in this description logic to serve as referring expressions that depend on structural identification is also presented and is tied to a diagnosis of a singularity condition for such concepts to logical entailment of TDDs for an ontology.

ABSTRACT. Machine Learning (ML) models are regularly employed in diverse application domains to support decision-making processes. In this context, the knowledge is induced by the ML models. Combining this learned knowledge with intensional knowledge specified by logic-based formalisms would be highly beneficial to these processes. In this paper we present our recent work on this subject, describing a framework that combines these two forms of knowledge and enables formal reasoning. The framework is based on the novel notion of Hybrid Knowledge Base (HKB), which consists of an ontology and a set of ML binary classifiers. The ontology defines the intensional knowledge over the domain, while the ML classifiers implicitly define the extensional knowledge. Specifically, a HKB combines these two components by associating each predicate of the ontology with a classifier, which virtually populates the predicate with positively classified instances. A further contribution of our work is the study of the query answering task. In particular, we provide its computational complexity analysis for ontologies specified in (the Description Logic counterpart of) RDFS, and binary Multi-Layer Perceptrons.

ABSTRACT. In this paper we study a preferential temporal description logic with typicality, which allows for defeasible reasoning in a temporal description logic. We consider an encoding of preferential temporal description logics with typicality into temporal extensions of ALC, based on Linear Time Temporal Logic, a result which extends to the multi-preferential case. For the multi-preferential case, we revisit a previous semantics of weighted knowledge bases by considering preference combination.

ABSTRACT. Description Logic reasoners enable automated reasoning over ontologies expressed using the Web Ontology Language (OWL). They can be used to infer logical consequences from a set of asserted facts or axioms within an ontology. However, many well known reasoners are currently non-maintained, or are not actively developed. This can lead to unpatched bugs, missing features, or non-adherence to possible new standards that might arise in the future. In this paper, we analyse and show how we can employ coding agents for the development and maintenance of OWL DL reasoners. To this end, we propose OxidOWL, an OWL DL reasoner developed and maintained through coding agents. We validate our approach through thorough testing and compare the proposed approach with existing well-known reasoners.

ABSTRACT. Knowledge base (KB) embeddings aim at combining the capability of classical knowledge graph embeddings to generalize the information present in facts, the ABox, with conceptual knowledge represented in an ontology language, the TBox. Several authors have recently explored the idea of mapping concepts to convex regions in a vector space. This is useful to represent hierarchies, typically present in TBoxes, since more general concepts can be mapped to larger regions, containing those regions associated with more specific concepts. However, the power of convexity is rarely leveraged during the actual learning tasks. Here, we introduce BoxLitE, a KB embedding model for DL-Lite that allows for convex optimization. We show that for any satisfiable DL-Lite KB, there is a BoxLitE embedding that is a weakly faithful model. As a proof of concept, we show how to formulate the KB embedding task as a convex optimization problem and how to obtain embeddings with such desirable faithfulness properties.

ABSTRACT. The identification and mitigation of bias in machine learning systems requires a precise formal representation of the norms against which inferences are evaluated. Formal ontologies provide a natural foundation for this task. In this work, we develop a Description Logic–based general formalization of the structure underlying several types of bias, with explicit attention to the epistemic states of agents. First, we employ the Description Logic $\mathcal{ALC}$ to axiomatize the ontological structure that encodes the normative conditions under which an inference counts as biased or unbiased. Second, we provide a translation of the $\mathcal{ALC}$ formalization into a first-order modal framework enriched with necessity and knowledge operators. This step allows us to integrate ontological constraints with representations of agents' epistemic attitudes, thereby connecting DL-based knowledge representation with epistemic reasoning. The combined framework makes it possible to characterize formally the epistemic conditions under which agents may generate biased inferences and to distinguish them from configurations in which bias cannot arise.

ABSTRACT. Learning concepts from data examples is an intensively investigated topic in description logics (DLs), in particular for the EL-family. So far, hardly any of these works on concept learning consider the Kleene star to express the (reflexive) transitive closure of roles. However, the star plays a central role in some closely related settings, like learning shape expressions in graph constraint languages such as SHACL, and learning graph queries from graph data. As a first step towards developing techniques for learning SHACL shape expressions, we consider learning from examples (aka the fitting problem) for the logic EL^*, which extends EL by the reflexive transitive closure of named roles. In contrast to EL, the DL EL^* can express a limited form of disjunction that can result in more informative fittings. By adapting the automata-based techniques for EL, we obtain complexity bounds for deciding existence of EL^* fittings that coincide with those for EL. We also develop an algorithm for computing most specific fittings in EL^*.

ABSTRACT. We study the problem of finitely characterizing ontologies, concept inclusions, and concept equivalences, all formulated in the description logic ℰℒ, in terms of positive and negative examples. We consider two different kinds of examples: finite interpretations and finite pointed interpretations, with the expressive power of the latter being higher than that of the former. We prove that non-tautological concept inclusions and concept equivalences are characterizable by a finite set of pointed examples, and that acyclic inclusions and equivalences are even characterizable by a finite set of non-pointed examples. For ontologies, in contrast, finite characterizability fails even for pointed examples. This leads us to consider the important class of left-atomic ontologies, where only concept names can appear on the left side of concept inclusions and equivalences. There, finite characterizability in terms of pointed examples is regained.