Querying large databases while taking ontologies into account is currently a very active domain research. In this paper, we consider ontologies described by existential rules (also known as Datalog+/-), a framework that generalizes lightweight description logics. A common approach is to rewrite a conjunctive query w.r.t an ontology into a union of conjunctive queries (UCQ) which can be directly evaluated against a database. However, the practicability of this approach is questionable due to 1) the weak expressivity of classes for which efficient rewriters have been implemented 2) the large size of optimal rewritings using UCQ. We propose to use semi-conjunctive queries (SCQ), which are a restricted form of positive existential formulas, and compute sound and complete rewritings, which are union of SCQ (USCQ). A novel algorithm for query rewriting, Compact, is presented. It computes sound and complete rewritings for large classes of ontologies. First experiments show that USCQ are both efficiently computable and more efficiently evaluable than their equivalent UCQ.

Nominal schemas have recently been introduced as a new approach for the integration of DL-safe rules into the Description Logic framework. The efficient processing of knowledge bases with nominal schemas remains, however, challenging. We address this by extending the well-known optimisation of absorption as well as the standard tableau calculus to directly handle the (absorbed) nominal schema axioms. We implement the resulting extension of standard tableau calculi in a novel reasoning system and we integrate further optimisations. In our empirical evaluation, we show the effect of these optimisations and we find that the proposed approach performs well even when compared to other DL reasoners with dedicated rule support.

Update semantics for Answer-Set Programming assign models to sequences of answer-set programs which result from the iterative process of updating programs by programs. Each program in the sequence represents an update of the preceding ones. One of the enduring problems in this context is state condensing, or the problem of determining a single logic program that faithfully represents the sequence of programs. Such logic program should 1) be written in the same alphabet, 2) have the same stable models, and 3) be equivalent to the sequence of programs when subject to further updates. It has been known for more than a decade that update semantics easily lead to non-minimal stable models, so an update sequence cannot be represented by a single non-disjunctive program. On the other hand, more expressive classes of programs were never considered, mainly because it was not clear how they could be updated further. In this paper we solve the state condensing problem for two foundational rule update semantics, using nested logic programs. Furthermore, we also show that disjunctive programs with default negation in the head can be used for the same purpose.

Default reasoning and interpolation are two important forms of commonsense rule-based reasoning. The former allows us to draw conclusions from incompletely specified states, by making assumptions on normality, whereas the latter allows us to draw conclusions from states that are not explicitly covered by any of the available rules. Although both approaches have received considerable attention in the literature, it is at present not well understood how they can be combined to draw reasonable conclusions from incompletely specified states and incomplete rule bases. In this paper, we introduce an inference system for interpolating default rules, based on a geometric semantics in which normality is related to spatial density and interpolation is related to geometric betweenness. We view default rules and information on the betweenness of natural categories as particular types of constraints on qualitative representations of Gärdenfors conceptual spaces. We propose an axiomatization, extending the well-known System P, and show its soundness and completeness w.r.t. the proposed semantics. Subsequently, we explore how our extension of preferential reasoning can be further refined by adapting two classical approaches for handling the irrelevance problem in default reasoning: rational closure and conditional entailment.

Vast amounts of video data are available on the weband are being generated daily using surveillancecameras or other sources. Being able to efficientlyanalyse and process this data is essential for a numberof different applications. We want to be ableto efficiently detect activities in these videos or beable to extract and store essential information containedin these videos for future use and easy searchand access. Cohn et al. (2012) proposed a comprehensiverepresentation of spatial features that canbe efficiently extracted from video and used forthese purposes. In this paper, we present a modifiedversion of this approach that is equally efficientand allows us to extract spatial informationwith much higher accuracy than previously possible.We present efficient algorithms both for extractingand storing spatial information from video,as well as for processing this information in orderto obtain useful spatial features. We evaluate ourapproach and demonstrate that the extracted spatialinformation is considerably more accurate than thatobtained from existing approaches.

Product defects and rework efforts due to flawed specifications represent major issues for a project’s performance, so that there is a high motivation for providing effective means that assist designers in assessing and ensuring a specification’s quality. Recent research in the context of formal specifications, e.g. on coverage and vacuity, offers important means to tackle related issues. In the currently underrepresented research direction of diagnostic reasoning on a specification, we propose a scenario-based diagnosis at a specification’s operator level using weak or strong fault models. Drawing on efficient SAT encodings, we show in this paper how to achieve that effectively for specifications in LTL. Our experimental results illustrate our approach’s validity and attractiveness.

Abductive reasoning (or Abduction, for short) is among the most fundamental AI reasoning methods, with a broad range of applications, including fault diagnosis, belief revision, and automated planning. Unfortunately, Abduction is of high computational complexity; even propositional Abduction is Σ 2 P -complete and thus harder than NP and coNP. This complexity barrier rules out the existence of a polynomial transformation to propositional satisfiability (SAT). In this work we use structural properties of the Abduction instance to break this complexity barrier. We utilize the problem structure in terms of small backdoor sets. We present fixed-parameter tractable transformations from Abduction to SAT, which make the power of today's SAT solvers available to Abduction.

Diagnosis, i.e., the identification of root causes for failing or unexpected system behavior, is an important task in practice. Within the last three decades, many different AI-based solutions for solving the diagnosis problem have been presented and have been gaining in attraction. This leaves us with the question of which algorithm to prefer in a certain situation. In this paper we contribute to answering this question. In particular, we compare two classes of diagnosis algorithms. One class exploits conflicts in their search, i.e., sets of system components whose correct behavior contradicts given observations. The other class ignores conflicts and derives diagnoses from observations and the underlying model directly. In our study we use different reasoning engines ranging from an optimized Horn-clause theorem prover to general SAT and constraint solvers. Thus we also address the question whether publicly available general reasoning engines can be used for an efficient diagnosis.

In this work, we consider function-free existential rules extended with nonmonotonic negation under a stable model semantics. We present new acyclicity and stratification conditions that identify a large class of rule sets having finite, unique stable models, and we show how the addition of constraints on the input facts can further extend this class. Checking these conditions is computationally feasible, and we provide tight complexity bounds. Finally, we demonstrate how these new methods allowed us to solve relevant reasoning problems over a real-world knowledge base from biochemistry using an off-the-shelf answer set programming engine.

When answering queries in the presence of ontologies, adopting the closed world assumption for some predicates easily results in intractability. We analyze this situation on the level of individual ontologies formulated in the description logics DL-Lite and EL and show that in all cases where answering CQs with (open and) closed predicates is tractable, it coincides with answering CQs with all predicates assumed open. In this sense, CQ answering with closed predicates in inherently intractable. Our analysis also yields a dichotomy between AC0 and coNP for CQ answering in DL-Lite and a dichotomy between PTime and coNP for EL. Interestingly, the situation is less dramatic in the more expressive description logic ELI, where we find ontologies for which CQ answering is in PTime, but does not coincide with CQ answering where all predicates are open.