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. In the extended abstract we report about a many-valued and multi-preferential conditional logic with typicality developed in https://academic.oup.com/logcom/article/36/2/exaf063/8442302, which is based on a multi-preferential semantics and is proven to be a generalization of KLM preferential semantics to the many-valued case. The multi-preferential semantics provides a preferential interpretation to gradual argumentation, considering both weighted and non-weighted argumentation graphs. The approach allows for conditional reasoning over arguments and boolean combination of arguments, with respect to some gradual semantics, through the verification of graded (strict or defeasible) implications over argumentation graphs.

ABSTRACT. We study realizability in terms of stable labellings for classical Dung frameworks. Although there is a close relationship between extension-based and labelling-based semantics, realizability with respect to labellings is significantly more challenging. This is due to the explicit treatment of non-accepted arguments (i.e., undecided and rejected ones), which fixes the argument set of any witnessing framework and rules out auxiliary arguments commonly used in constructions for extension-based semantics. Consequently, existing characterizations for extension-based semantics can only be reused to a limited extent. Towards a characterization we introduce so-called candidate sets. This notion captures maximal conflict-free sets that have the potential to become stable but should not. These sets constitute a central obstacle in our approach. In the absence of such sets, we provide a characterization theorem. For the general case, we identify a canonical over-approximating framework such that every stably realizable labelling set admits a witnessing argumentation framework obtainable as a subgraph of it. However, we observed an inherent non-determinism for our proposed method. Finally, we identified a connection between labelling-based realizability and the long-standing open problem of compact stable extension realizability.

ABSTRACT. We introduce tenability, a dialogue-based semantics for Dung-style Argumentation Frameworks that formalizes when a designated argument (or a set of arguments) can be maintained in debate by a proponent against any legitimate (conflict-free) attack which the opponent may present. The approach naturally corresponds to one-shot debate scenarios in which a uniform defense against all possible counterarguments is not required, and is robust with respect to further constraints placed on the rules of the dialogue game.

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. Partial expansion operators were presented in Zhang (2018) as intermediate operators that, when combined with choice contraction, lead to choice revision operators. We propose analyzing partial expansion operators in their own right, generalizing the original proposal, and studying different alternatives for this family. In doing so, we also point out a flaw in the original definition where some postulates are incompatible, and propose how to amend it by considering new postulates that maintain the original purpose of these operators.

ABSTRACT. We study the computational aspects of \emph{epistemic preference relations} in non-classical logics, particularly \emph{linear temporal logic} (LTL). Epistemic preferences form the backbone of \emph{belief contraction operators}, which describe how to rationally relinquish obsolete beliefs. These preference relations have to satisfy certain innocuous conditions; and constructing such relations is usually assumed to be a trivial process. However, in the case of LTL, where relations are represented with Büchi automata, we show that this is a challenging task: the core condition, which guarantees the success of contraction, is in fact \emph{undecidable}. Towards achieving effective LTL belief contraction, we then propose several concrete constructions of novel preference relations that satisfy the required conditions \emph{by design}. These constructions include, among others, (1) generalisations of distance measures (e.g.\ Dalal) beyond the classical setting, as well as (2) the ability to hierarchically compose different preference relations. Our results not only provide rich families of preference relations for LTL, but also generalise the limited pool of concrete preference relations for the classical cases, allowing us to go beyond Dalal to achieve full rationality.

ABSTRACT. In this paper we investigate truth-tracking properties of iterated belief revision methods. We focus on the multi-agent context when several agents revise their plausibility spaces simultaneously and arrive at joint beliefs through merge. We investigate the convergence properties of such a process: given a distributed sequence of information that truthfully and completely describes the actual world, will the process converge to true beliefs about the actual world? We focus on two methods that were previously proven to work for single-agents truth-tracking based on belief revision: conditioning and lexicographic revision. We show that some of the positive results carry on to our multi-agent setting. We introduce a novel kind of belief merge operation that is memory-based. We also study how to deal with occasional erroneous information by applying priority merge techniques.

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.

ABSTRACT. Machine learning classifiers work by being given a dataset of instances described by observed properties and labels, and then learning how to predict the label of a new instance. Some methods do this in an interpretable way, producing simple if-then rules that a person can read directly. A learned rule set may say that one feature pattern usually supports label~1, except when a more specific pattern supports label~0. People naturally read such outputs as defaults and exceptions, but a readable rule set is not automatically a defeasible theory: it may look defeasible without any formal guarantee that its predictions correspond to principled nonmonotonic reasoning. This paper provides such a guarantee. We identify a single structural condition on learned conjunctive rule sets for binary classification, called strict global exception closure, under which every prediction the classifier makes is provably a defeasible entailment. To make this precise, we translate the rule set into a defeasible knowledge base in the framework of Kraus, Lehmann, and Magidor (KLM), a standard approach to reasoning with rules that can have exceptions. We then prove that, for every fully observed instance, the classifier's Most Specific Wins prediction agrees exactly with the entailment of the translated knowledge base under three well-known KLM-style formalisms: Rational Closure, Lexicographic Closure, and System~W. The classifier is therefore not merely interpretable; it is a formally grounded defeasible theory. We further show that strict global exception closure is the only condition that needs to be checked directly: one additional property follows from it logically, and another is restored by a prediction-preserving pruning step. We analyse what breaks when the condition fails, revealing insights for both machine learning and nonmonotonic reasoning. Experiments on several benchmark datasets confirm that the condition arises naturally from decision tree extraction, producing rule sets with nontrivial exception hierarchies at competitive accuracy.

ABSTRACT. Structural causal models (SCMs) are the default substrate for counterfactual explanation, responsibility, and causal recourse in the Halpern-Pearl account of actual causation. In SCMs, interventions quantify over arbitrary assignments to endogenous variables. However, in socio-technical systems, agent actions (and hence responsibility) are constrained by procedures, authority, permissions, and coordination requirements. Thus counterfactual `alternatives' may include states that the relevant agent could not have feasibly executed. We characterize this intervention--feasibility gap and show how it can yield misplaced responsibility attributions or infeasible recourse recommendations even when the underlying SCM is descriptively adequate. We propose a principled restriction of intervention admissibility via \emph{Resource-aware SCMs} (R-SCMs). Without abandoning SCM semantics, we equip models with agent-controlled endogenous variables, enablement predicates evaluated against the acting agent's observation, and consumable resources modelled by a partial commutative monoid. We interpret agent-relative counterfactual feasibility via executable, resource-consuming intervention traces (a sequence of actions) and prove basic properties of R-SCMs (well-definedness, monotonicity, conservativity under trivial feasibility). Finally, we prove \textsf{NP-completeness} of the bounded-horizon feasibility decision problem for R-SCMs.

ABSTRACT. Reinforcement learning (RL) is notoriously sample-inefficient and opaque, a problem that error-prone techniques like reward shaping or feature engineering often fail to resolve. In this work, we introduce a method to induce temporal advice from expert demonstrations via Inductive Logic Programming. We then show how this advice, transformed to answer set automata, enables the transparent guidance of RL agents. The advice is symbolic and interpretable, being expressed in linear temporal logic over finite traces with answer set programming queries. Formula-learning experiments show that our encoding successfully induces generalizable temporal advice from executions of a partially observable environment. We apply the learned advice to guide an RL agent, benchmarking its performance against three baselines: standard unguided Q-learning, guidance via time-independent rules, and guidance using persistent macro-action rules. Our findings show that temporal advice learned on small maps transfers successfully to larger instances, outperforming standard Q-learning and both baseline guidance approaches in convergence rate.