Given a knowledge base (KB) with a non-entailed fact, the ABox abduction problem asks for possible extensions of the KB that would entail this fact. This problem has many applications, ranging from diagnosis to explainability and repair. ABox abduction has been well-investigated for consistent KBs and classical semantics, but little is known for the case of inconsistent KBs, which can be caused by erroneous data. In this paper we define suitable notions of abduction in this setting and propose criteria that guide abduction towards useful hypotheses. To regain meaningful reasoning in the presence of inconsistencies, we use well-established repair semantics. We provide a comprehensive landscape of the complexity of ABox abduction under repair semantics, treating different variants of the abduction problem for the light-weight description logics DL-Lite and EL_bot.

Answering temporal CQs over temporalized Description Logic knowledge bases (TKB) is a main technique to realize ontology-based situation recognition. In case the collected data in such a knowledge base is inaccurate, important query answers can be missed. In this paper we introduce the TKB Alignment problem, which computes a variant of the TKB that minimally changes the TKB, but entails the given temporal CQ and is in that sense (cost-) optimal. We investigate this problem for ALC TKBs and conjunctive queries with LTL operators and devise a solution technique to compute (cost-optimal) alignments of TKBs that extends techniques for the alignment problem for propositional LTL over finite traces.

Abstract The inexpressive Description Logic (DL) ${\cal F}{{\cal L}_0}$ , which has conjunction and value restriction as its only concept constructors, had fallen into disrepute when it turned out that reasoning in ${\cal F}{{\cal L}_0}$ w.r.t. general TBoxes is ExpTime-complete, that is, as hard as in the considerably more expressive logic ${\cal A}{\cal L}{\cal C}$ . In this paper, we rehabilitate ${\cal F}{{\cal L}_0}$ by presenting a dedicated subsumption algorithm for ${\cal F}{{\cal L}_0}$ , which is much simpler than the tableau-based algorithms employed by highly optimized DL reasoners. Our experiments show that the performance of our novel algorithm, as prototypically implemented in our ${\cal F}{{\cal L}_0}$ wer reasoner, compares very well with that of the highly optimized reasoners. ${\cal F}{{\cal L}_0}$ wer can also deal with ontologies written in the extension ${\cal F}{{\cal L}_ \bot }$ of ${\cal F}{{\cal L}_0}$ with the top and the bottom concept by employing a polynomial-time reduction, shown in this paper, which eliminates top and bottom. We also investigate the complexity of reasoning in DLs related to the Horn-fragments of ${\cal F}{{\cal L}_0}$ and ${\cal F}{{\cal L}_ \bot }$ .

Abstract Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of state based operational models such as Markov decision processes. Description logics (DLs) provide a well-suited formalism to describe and reason about knowledge and are used as basis for the web ontology language (OWL). We investigate how such knowledge described by DLs can be integrated into the PMC process, introducingontology-mediatedPMC. Specifically, we proposeontologized programsas a formalism that links ontologies to behaviors specified by probabilistic guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Through DL reasoning, inconsistent states in the modeled system can be detected. We present three ways to resolve these inconsistencies, leading to different Markov decision process semantics. We analyze the computational complexity of checking whether an ontologized program is consistent under these semantics. Further, we present and implement a technique for the quantitative analysis of ontologized programs relying on standard DL reasoning and PMC tools. This way, we enable the application of PMC techniques to analyze knowledge-intensive systems.We evaluate our approach and implementation on amulti-server systemcase study,where different DL ontologies are used to provide specifications of different server platforms and situations the system is executed in.

Many SPARQL benchmark generation techniques rely on SPARQL query templates or on selecting representative queries from a set of input queries by inspecting their syntactic features. Hence, prototype queries from such benchmarks mainly capture combinations of SPARQL features, but not the semantics nor the conceptual association between queries. We present congenial benchmarks---a novel type of benchmark that can detect conceptual associations and thus reflect prototypical user intentions when selecting prototype queries. We study SPARROW, an instantiation of congenial benchmarks, where the conceptual associations of SPARQL queries are measured by concept similarity measures. To this end, we transform unary acyclic conjunctive SPARQL queries into ELH-description logic concepts. Our evaluation of three popular triple stores on two datasets shows that the benchmarks generated by SPARROW differ considerably from benchmarks generated using a feature-based approach. Moreover, our evaluation suggests that SPARROW can characterize the performance of common triple stores with respect to user needs by exploiting conceptual associations to detect prototypical user needs.

Reasoning for Description logics with concrete domains and w.r.t. general TBoxes easily becomes undecidable. However, with some restriction on the concrete domain, decidability can be regained. We introduce a novel way to integrate concrete domains 𝒟 into the well-known description logic, we call the resulting logic. We then identify sufficient conditions on 𝒟 that guarantee decidability of the satisfiability problem, even in the presence of general TBoxes. In particular, we show decidability offor several domains over the integers, for which decidability was open. More generally, this result holds for all negation-closed concrete domains with the EHD-property, which stands for ‘the existence of a homomorphism is definable’. Such technique has recently been used to show decidability of CTL*with local constraints over the integers.