Existential rules (also known as Datalog+/- or tuple-generating dependencies) have been intensively studied in recent years as a prominent formalism in knowledge representation and database systems. We consider them here as a querying formalism, extending classical Datalog, the language of deductive databases. It is well known that the classes of databases recognized by (Boolean) existential rule queries are closed under homomorphisms. Also, due to the existence of a semi-decision procedure (the chase), these database classes are recursively enumerable. We show that, conversely, every homomorphism-closed recursively enumerable query can be expressed as an existential rule query, thus arriving at a precise characterization of existential rules by model-theoretic and computational properties. Although the result is very intuitive, the proof turns out to be non-trivial. This result can be seen as a very expressive counterpart of the prominent Lyndon-Los-Tarski-Theorem characterizing the homomorphism-closed fragment of first-order logic. Notably, our result does not presume the existence of any additional built-in structure on the queried data, such as a linear order on the domain, which is a typical requirement for other characterizations in the spirit of descriptive complexity.

General Game Playing aims to create AI systems that can understand the rules of new games and learn to play them effectively without human intervention. The recent proposal for general game-playing robots extends this to AI systems that play games in the real world. Execution monitoring becomes a necessity when moving from a virtual to a physical environment, because in reality actions may not be executed properly and (human) opponents may make illegal game moves. We develop a formal framework for execution monitoring by which an action theory that provides an axiomatic description of a game is automatically embedded in a meta-game for a robotic player — called the arbiter — whose role is to monitor and correct failed actions. This allows for the seamless encoding of recovery behaviours within a meta-game, enabling a robot to recover from these unexpected events.

We investigate fundamental properties of three-valued semantics for abstract dialectical frameworks (ADFs). In particular, we deal with realizability, i.e., the question whether there exists an ADF that has a given set of interpretations as its semantics. We provide necessary and sufficient conditions that hold for a set of three-valued interpretations whenever there is an ADF realizing it under admissible, complete, grounded, or preferred semantics. Moreover, we discuss how to construct such an ADF in case of realizability. Our results lay the ground for studying the expressiveness of ADFs under three-valued semantics. As a first application we study implications of our results on the existence of certain join operators on ADFs.

The sentential decision diagram (SDD) has been recently proposed as a new  tractable representation of Boolean functions that generalizes the influential  ordered binary decision diagram (OBDD).  Empirically, compiling CNFs into SDDs  has yielded significant improvements in both time and space over compiling  them into OBDDs, using a bottom-up compilation approach. In this work, we present a top-down CNF to SDD compiler that is based on techniques  from the SAT literature. We compare the presented compiler empirically to the state-of-the-art, bottom-up SDD compiler, showing orders-of-magnitude improvements in compilation time.

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.

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.

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.

Agents can be thought of as following a social behaviour, depending on the context in which they are interacting. We devise a computationally grounded  mechanism to represent and reason about others in social terms, reflecting the local perspective of an agent (first-person view), to support both stereotypical and empathetic reasoning. We use a hierarchy of agent models to discriminate which behaviours of others are plausible, and decide which behaviour for ourselves is socially acceptable, i.e. conforms to the social context. To this aim, we investigate the implications of considering agents capable of various degrees of theory of mind, and discuss a scenario showing how this affects behaviour.