arXiv subjects

Stefan Borgwardt

Publications and source records attributed to Stefan Borgwardt.

At least 19 recordsLinked to original sources

arXiv2025

The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)

Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the $\mathcal{EL}$ family of DLs, each of which gives rise to proofs of different shapes. Here, we study three such calculi and the proofs they produce on a benchmark based on the OWL Reasoner Evaluation. The calculi are implemented using a translation into existential rules with stratified negation, which had already been demonstrated to be effective for the calculus of the ELK reasoner. We then use the rule engine NEMO to evaluate the rules and obtain traces of the rule execution. After translating these traces back into DL proofs, we compare them on several metrics that reflect different aspects of their complexity.

cs.LO↗

arXiv2025

Automated planning with ontologies under coherence update semantics (Extended Version)

Standard automated planning employs first-order formulas under closed-world semantics to achieve a goal with a given set of actions from an initial state. We follow a line of research that aims to incorporate background knowledge into automated planning problems, for example, by means of ontologies, which are usually interpreted under open-world semantics. We present a new approach for planning with DL-Lite ontologies that combines the advantages of ontology-based action conditions provided by explicit-input knowledge and action bases (eKABs) and ontology-aware action effects under the coherence update semantics. We show that the complexity of the resulting formalism is not higher than that of previous approaches and provide an implementation via a polynomial compilation into classical planning. An evaluation of existing and new benchmarks examines the performance of a planning system on different variants of our compilation.

cs.AI↗

arXiv2025

Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)

Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete domains, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in $\mathcal{ALCSCC}$, while the comparison of feature values of different individuals in $\mathcal{ALC}(\mathfrak{D})$ has been studied in the context of $ω$-admissible concrete domains $\mathfrak{D}$. In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL $\mathcal{ALCOSCC}(\mathfrak{D})$, which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of $\mathfrak{D}$ is also decidable in exponential time. It is thus not higher than the complexity of the basic DL $\mathcal{ALC}$. At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.

cs.LO↗

arXiv2024

The Precise Complexity of Reasoning in $\mathcal{ALC}$ with $ω$-Admissible Concrete Domains (Extended Version)

Concrete domains have been introduced in the context of Description Logics to allow references to qualitative and quantitative values. In particular, the class of $ω$-admissible concrete domains, which includes Allen's interval algebra, the region connection calculus (RCC8), and the rational numbers with ordering and equality, has been shown to yield extensions of $\mathcal{ALC}$ for which concept satisfiability w.r.t. a general TBox is decidable. In this paper, we present an algorithm based on type elimination and use it to show that deciding the consistency of an $\mathcal{ALC}(\mathfrak{D})$ ontology is ExpTime-complete if the concrete domain $\mathfrak{D}$ is $ω$-admissible and its constraint satisfaction problem is decidable in exponential time. While this allows us to reason with concept and role assertions, we also investigate feature assertions $f(a,c)$ that can specify a constant $c$ as the value of a feature $f$ for an individual $a$. We show that, under conditions satisfied by all known $ω$-admissible domains, we can add feature assertions without affecting the complexity.

cs.LO↗

arXiv2023

Why Not? Explaining Missing Entailments with Evee (Technical Report)

Understanding logical entailments derived by a description logic reasoner is not always straight-forward for ontology users. For this reason, various methods for explaining entailments using justifications and proofs have been developed and implemented as plug-ins for the ontology editor Protégé. However, when the user expects a missing consequence to hold, it is equally important to explain why it does not follow from the ontology. In this paper, we describe a new version of $\rm E{\scriptsize VEE}$, a Protégé plugin that now also provides explanations for missing consequences, via existing and new techniques based on abduction and counterexamples.

cs.AI↗

arXiv2023

Combining Proofs for Description Logic and Concrete Domain Reasoning (Technical Report)

Logic-based approaches to AI have the advantage that their behavior can in principle be explained with the help of proofs of the computed consequences. For ontologies based on Description Logic (DL), we have put this advantage into practice by showing how proofs for consequences derived by DL reasoners can be computed and displayed in a user-friendly way. However, these methods are insufficient in applications where also numerical reasoning is relevant. The present paper considers proofs for DLs extended with concrete domains (CDs) based on the rational numbers, which leave reasoning tractable if integrated into the lightweight DL $\mathcal{E}\hspace{-0.1em}\mathcal{L}_\bot$. Since no implemented DL reasoner supports these CDs, we first develop reasoning procedures for them, and show how they can be combined with reasoning approaches for pure DLs, both for $\mathcal{E}\hspace{-0.1em}\mathcal{L}_\bot$ and the more expressive DL $\mathcal{ALC}$. These procedures are designed such that it is easy to extract proofs from them. We show how the extracted CD proofs can be combined with proofs on the DL side into integrated proofs that explain both the DL and the CD reasoning.

cs.LO↗

arXiv2022

Explaining Ontology-Mediated Query Answers using Proofs over Universal Models (Technical Report)

In ontology-mediated query answering, access to incomplete data sources is mediated by a conceptual layer constituted by an ontology, which can be formulated in a description logic (DL) or using existential rules. In the literature, there exists a multitude of complex techniques for incorporating ontological knowledge into queries. However, few of these approaches were designed for explainability of the query answers. We tackle this challenge by adapting an existing proof framework toward conjunctive query answering, based on the notion of universal models. We investigate the data and combined complexity of determining the existence of a proof below a given quality threshold, which can be measured in different ways. By distinguishing various parameters such as the shape of the query, we obtain an overview of the complexity of this problem for several Horn DLs.

cs.LO↗

arXiv2022

Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Technical Report)

In ontology-mediated query answering, access to incomplete data sources is mediated by a conceptual layer constituted by an ontology. To correctly compute answers to queries, it is necessary to perform complex reasoning over the constraints expressed by the ontology. In the literature, there exists a multitude of techniques incorporating the ontological knowledge into queries. However, few of these approaches were designed for comprehensibility of the query answers. In this article, we try to bridge these two qualities by adapting a proof framework originally applied to axiom entailment for conjunctive query answering. We investigate the data and combined complexity of determining the existence of a proof below a given quality threshold, which can be measured in different ways. By distinguishing various parameters such as the shape of a query, we obtain an overview of the complexity of this problem for the lightweight ontology languages DL-Lite_R and EL, and also have a brief look at temporal query answering.

cs.DB↗

arXiv2022

On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (Extended Version)

When working with description logic ontologies, understanding entailments derived by a description logic reasoner is not always straightforward. So far, the standard ontology editor Protégé offers two services to help: (black-box) justifications for OWL 2 DL ontologies, and (glass-box) proofs for lightweight OWL EL ontologies, where the latter exploits the proof facilities of reasoner ELK. Since justifications are often insufficient in explaining inferences, there is thus only little tool support for explaining inferences in more expressive DLs. In this paper, we introduce EVEE-LIBS, a Java library for computing proofs for DLs up to ALCH, and EVEE-PROTEGE, a collection of Protégé plugins for displaying those proofs in Protégé. We also give a short glimpse of the latest version of EVONNE, a more advanced standalone application for displaying and interacting with proofs computed with EVEE-LIBS.

cs.LO↗

arXiv2022

Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report)

Logic-based approaches to AI have the advantage that their behavior can in principle be explained to a user. If, for instance, a Description Logic reasoner derives a consequence that triggers some action of the overall system, then one can explain such an entailment by presenting a proof of the consequence in an appropriate calculus. How comprehensible such a proof is depends not only on the employed calculus, but also on the properties of the particular proof, such as its overall size, its depth, the complexity of the employed sentences and proof steps, etc. For this reason, we want to determine the complexity of generating proofs that are below a certain threshold w.r.t. a given measure of proof quality. Rather than investigating this problem for a fixed proof calculus and a fixed measure, we aim for general results that hold for wide classes of calculi and measures. In previous work, we first restricted the attention to a setting where proof size is used to measure the quality of a proof. We then extended the approach to a more general setting, but important measures such as proof depth were not covered. In the present paper, we provide results for a class of measures called recursive, which yields lower complexities and also encompasses proof depth. In addition, we close some gaps left open in our previous work, thus providing a comprehensive picture of the complexity landscape.

cs.AI↗

arXiv2022

Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version

Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The "justifications" usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.

cs.LO↗

arXiv2022

Expressivity of Planning with Horn Description Logic Ontologies (Technical Report)

State constraints in AI Planning globally restrict the legal environment states. Standard planning languages make closed-domain and closed-world assumptions. Here we address open-world state constraints formalized by planning over a description logic (DL) ontology. Previously, this combination of DL and planning has been investigated for the light-weight DL DL-Lite. Here we propose a novel compilation scheme into standard PDDL with derived predicates, which applies to more expressive DLs and is based on the rewritability of DL queries into Datalog with stratified negation. We also provide a new rewritability result for the DL Horn-ALCHOIQ, which allows us to apply our compilation scheme to quite expressive ontologies. In contrast, we show that in the slight extension Horn-SROIQ no such compilation is possible unless the weak exponential hierarchy collapses. Finally, we show that our approach can outperform previous work on existing benchmarks for planning with DL ontologies, and is feasible on new benchmarks taking advantage of more expressive ontologies. That is an extended version of a paper accepted at AAAI 22.

cs.AI↗

arXiv2021

Temporal Minimal-World Semantics for Sparse ABoxes

Ontology-mediated query answering is a popular paradigm for enriching answers to user queries with background knowledge. For querying the absence of information, however, there exist only few ontology-based approaches. Moreover, these proposals conflate the closed-domain and closed-world assumption, and therefore are not suited to deal with the anonymous objects that are common in ontological reasoning. Many real-world applications, like processing electronic health records (EHRs), also contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. Our contribution consists of two main parts: In the first part we introduce a new closed-world semantics for answering conjunctive queries with negation over ontologies formulated in the description logic ELHb, which is based on the minimal canonical model. We propose a rewriting strategy for dealing with negated query atoms, which shows that query answering is possible in polynomial time in data complexity. In the second part, we extend this minimal-world semantics for answering metric temporal conjunctive queries with negation over the lightweight temporal logic TELHb and obtain similar rewritability and complexity results. This paper is under consideration in Theory and Practice of Logic Programming (TPLP).

cs.DB↗

arXiv2020

Safe Handover in Mixed-Initiative Control for Cyber-Physical Systems

For mixed-initiative control between cyber-physical systems (CPS) and its users, it is still an open question how machines can safely hand over control to humans. In this work, we propose a concept to provide technological support that uses formal methods from AI -- description logic (DL) and automated planning -- to predict more reliably when a hand-over is necessary, and to increase the advance notice for handovers by planning ahead of runtime. We combine this with methods from human-computer interaction (HCI) and natural language generation (NLG) to develop solutions for safe and smooth handovers and provide an example autonomous driving scenario. A study design is proposed with the assessment of qualitative feedback, cognitive load and trust in automation.

cs.HC↗

arXiv2020

Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)

Logic-based approaches to AI have the advantage that their behaviour can in principle be explained by providing their users with proofs for the derived consequences. However, if such proofs get very large, then it may be hard to understand a consequence even if the individual derivation steps are easy to comprehend. This motivates our interest in finding small proofs for Description Logic (DL) entailments. Instead of concentrating on a specific DL and proof calculus for this DL, we introduce a general framework in which proofs are represented as labeled, directed hypergraphs, where each hyperedge corresponds to a single sound derivation step. On the theoretical side, we investigate the complexity of deciding whether a certain consequence has a proof of size at most $n$ along the following orthogonal dimensions: (i) the underlying proof system is polynomial or exponential; (ii) proofs may or may not reuse already derived consequences; and (iii) the number $n$ is represented in unary or binary. We have determined the exact worst-case complexity of this decision problem for all but one of the possible combinations of these options. On the practical side, we have developed and implemented an approach for generating proofs for expressive DLs based on a non-standard reasoning task called forgetting. We have evaluated this approach on a set of realistic ontologies and compared the obtained proofs with proofs generated by the DL reasoner ELK, finding that forgetting-based proofs are often better w.r.t. different measures of proof complexity.

cs.LO↗

arXiv2020

Temporal Conjunctive Query Answering in the Extended DL-Lite Family

Ontology-based query answering (OBQA) augments classical query answering in databases by domain knowledge encoded in an ontology. Systems for OBQA use the ontological knowledge to infer new information that is not explicitly given in the data. Moreover, they usually employ the open-world assumption, which means that knowledge that is not stated explicitly in the data and that is not inferred is not assumed to be true or false. Classical OBQA however considers only a snapshot of the data, which means that information about the temporal evolution of the data is not used for reasoning and hence lost. We investigate temporal conjunctive queries (TCQs) that allow to access temporal data through classical ontologies. In particular, we study combined and data complexity of TCQ entailment for ontologies written in description logics from the extended DL-Lite family. Many of these logics allow for efficient reasoning in the atemporal setting and are successfully applied in practice. We show comprehensive complexity results for temporal reasoning with these logics.

cs.LO↗

arXiv2018

Deep Learning for Quality Control of Subcortical Brain 3D Shape Models

We present several deep learning models for assessing the morphometric fidelity of deep grey matter region models extracted from brain MRI. We test three different convolutional neural net architectures (VGGNet, ResNet and Inception) over 2D maps of geometric features. Further, we present a novel geometry feature augmentation technique based on a parametric spherical mapping. Finally, we present an approach for model decision visualization, allowing human raters to see the areas of subcortical shapes most likely to be deemed of failing quality by the machine. Our training data is comprised of 5200 subjects from the ENIGMA Schizophrenia MRI cohorts, and our test dataset contains 1500 subjects from the ENIGMA Major Depressive Disorder cohorts. Our final models reduce human rater time by 46-70%. ResNet outperforms VGGNet and Inception for all of our predictive tasks.

q-bio.NC↗

arXiv2017

Machine Learning for Large-Scale Quality Control of 3D Shape Models in Neuroimaging

As very large studies of complex neuroimaging phenotypes become more common, human quality assessment of MRI-derived data remains one of the last major bottlenecks. Few attempts have so far been made to address this issue with machine learning. In this work, we optimize predictive models of quality for meshes representing deep brain structure shapes. We use standard vertex-wise and global shape features computed homologously across 19 cohorts and over 7500 human-rated subjects, training kernelized Support Vector Machine and Gradient Boosted Decision Trees classifiers to detect meshes of failing quality. Our models generalize across datasets and diseases, reducing human workload by 30-70\%, or equivalently hundreds of human rater hours for datasets of comparable size, with recall rates approaching inter-rater reliability.

q-bio.QM↗