The AGM paradigm of belief change studies the dynamics of belief states in light of new information. Finding, or even approximating, dependent or relevant beliefs to a change is valuable because, for example, it can narrow the set of beliefs considered during belief change operations. Gärdenfors' preservation criterion (GPC) suggests that formulas independent of a belief change should remain intact. GPC allows to build dependence relations that are theoretically linked with belief change. Such dependence relations can in turn be used as a theoretical benchmark against which to evaluate other approximate dependence or relevance relations. There are already some studies, based on GPC, on the parallelism between belief change and dependence. One study offers a dependence relation parallel to AGM contraction for belief sets. Another study links base dependence relation to a more general belief base contraction, saturated kernel contraction. Here we offer yet a more general parallelism between kernel contraction and base dependence. At this level of generalization, different types of base dependence emerge. We prove that this differentiation of base dependence types is a result of possible redundancy in the base. This provides a theoretical means to distinguish between redundant and informative parts of a belief base.

Materialisation precomputes all consequences of a set of facts and a datalog program so that queries can be evaluated directly (i.e., independently from the program). Rewriting optimises materialisation for datalog programs with equality by replacing all equal constants with a single representative; and incremental maintenance algorithms can efficiently update a materialisation for small changes in the input facts. Both techniques are critical to practical applicability of datalog systems; however, we are unaware of an approach that combines rewriting and incremental maintenance. In this paper we present the first such combination, and we show empirically that it can speed up updates by several orders of magnitude compared to using either rewriting or incremental maintenance in isolation.

In the context of ontology-based data access with description logics (DLs), we study ontology-mediated queries in which selected predicates can be closed (OMQCs). In particular, we contribute to the classification of the data complexity of such queries in several relevant DLs. For the case where only concept names can be closed, we tightly link this question to the complexity of surjective CSPs. When also role names can be closed, we show that a full complexity classification is equivalent to classifying the complexity of all problems in coNP, thus currently out of reach. We also identify a class of OMQCs based on ontologies formulated in DL-LiteR that are guaranteed to be tractable and even FO-rewritable.

When Golog programs are used to control agents' behaviour in a high-level manner, their partial correctness naturally becomes an important concern. In this paper we propose a sound but incomplete method for automatic verification of partial correctness of Golog programs.  We introduce the notion of extended regression, which reduces partial correctness of Golog programs to first-order entailment problems.  During the process loop invariants are automatically discovered by heuristic methods.  We propose progression of small models wrt Golog programs, which are used to filter out too strong heuristic candidates.  In this way we combine the methods of static and dynamic analysis from the software engineering community.  Furthermore, our method can also be adapted to verify state constraints.  Experiments show that our method can not only handle sequential and nested loops uniformly in a reasonable among of time, but also be used to discover succinct and comprehensible loop invariants and state constraints.

We address the issue of Ontology-Based Query Answering (OBQA), which seeks to exploit knowledge expressed in ontologies when querying data. Ontologies are represented in the framework of existential rules (aka Datalog+/-). A commonly used technique consists in rewriting queries into unions of conjunctive queries (UCQs). However, the obtained queries can be prohibitively large in practice. A well-known source of combinatorial explosion are very simple rules, typically expressing taxonomies and relation signatures. We propose a rewriting technique, which consists in compiling these rules into a preorder on atoms and embedding this preorder into the rewriting process. This allows to compute compact rewritings that can be considered as ``pivotal'' representations, in the sense that they can be evaluated by different kinds of database systems. The provided algorithm computes a sound, complete and minimal UCQ rewriting, if one exists. Experiments show that this technique leads to substantial gains, in terms of size and runtime, and scales on very large ontologies. We also compare to other tools for OBQA with existential rules and related lightweight description logics.

Description Logic (DL) based ontologies and non-monotonic rules provide complementary features whose combination is crucial in many applications. In hybrid knowledge bases (KBs), which combine both formalisms, for large real-world applications, often integrating knowledge originating from different sources, inconsistencies can easily occur. These commonly trivialize standard reasoning and prevent us from drawing any meaningful conclusions. When restoring consistency by changing the KB is not possible, paraconsistent reasoning offers an alternative by allowing us to obtain meaningful conclusions from its consistent part. In this paper, we address the problem of efficiently obtaining meaningful conclusions from (possibly inconsistent) hybrid KBs. To this end, we define two paraconsistent semantics for hybrid KBs which, beyond their differentiating properties, are faithful to well-known paraconsistent semantics as well as the non-paraconsistent logic they extend, and tractable if reasoning in the DL component is.

We study the problem of rewriting an ontology O1 expressed in a DL L1 into an ontology O2 in a Horn DL L2 such that O1 and O2 are equisatisfiable when extended with an arbitrary dataset.  Ontologies that admit such rewritings are amenable to reasoning techniques ensuring tractability in data complexity.  After showing undecidability whenever L1 extends ALCF , we focus on devising efficiently checkable conditions that ensure existence of a Horn rewriting.  By lifting existing techniques for rewriting Disjunctive Datalog programs into plain Datalog to the case of arbitrary first-order programs with function symbols, we identify a class of ontologies that admit Horn rewritings of polynomial size.  Our experiments indicate that many real-world ontologies satisfy our sufficient conditions and thus admit polynomial Horn rewritings.

Large formal mathematical knowledge bases encode considerable parts of advanced mathematics and exact science, allowing deep semantic computer assistance and verification of complicated theories down to the atomic logical rules. An essential part of automated reasoning over such large theories are methods learning selection of relevant knowledge from the thousands of proofs in the corpora. Such methods in turn rely on efficiently computable features characterizing the highly structured and inter-related mathematical statements.  In this work we (i) propose novel semantic features characterizing the statements in such large semantic knowledge bases, (ii) propose and carry out their efficient implementation using deductive-AI data-structures such as substitution trees and discrimination nets, and (iii) show that they significantly improve the strength of existing knowledge selection methods and automated reasoning methods over the large formal knowledge bases. In particular, on a standard large-theory benchmark we improve the average predicted rank of a mathematical statement needed for a proof by 22% in comparison with state of the art. This allows us to prove 8% more theorems in comparison with state of the art.

Forgetting is an important mechanism for logic-based agent systems. A recent interest has been in the desirable properties of forgetting in answer set programming  (ASP)and their impact on the design of forgetting operators. It is known that some subsets of these propertiesare incompatible, i.e., they cannot be satisfied at the same time. In this paper, we are interested in the question onthe largest set Δ of pairs (Π, V), where Π is  a logic program and V is a set of atoms, such that a forgetting operator exists that satisfies all the desirable properties for each  (Π, V) in Δ.  We answer this question positively by discovering the precise condition under which the knowledge forgetting, a well-established approach to forgetting in ASP, satisfies the property of strong persistence, which leads to a sufficient and necessary condition for a forgetting operator to satisfy all the desirable properties proposed in the literature. We explore computational complexities on checking the condition and present a syntactic characterization which can serve as the basis of computing knowledge forgetting in ASP.

A consequence of a logic program is a consistent set of literals that are satisfied by every answer set. The well-founded model is a consequence that can be used to simplify the logic program. In this paper, we extend the notion of well-founded models to consequences for simplifying disjunctive logic programs (DLPs) in a general manner. Specifically, we provide two main notions, strong reliable set and weak reliable set, and show that a DLP is strongly equivalent to the simplified program if and only if the consequence is a strong reliable set, and they have the same answer sets if and only if the consequence is a weak reliable set. Then we provide computational complexity on identifying both notions. In addition, we provide an algorithm to compute some strong reliable sets and show that the approach is an extension of the well-founded model in simplifying logic programs.