The study of preferences has a long tradition in many disciplines, but it has only relatively recently entered the realm of data management through their application in answering queries to relational databases. The current revolution in data availability through the Web and, perhaps most importantly in the last few years, social media sites and applications, puts ontology languages at the forefront of data and information management technologies. In this paper, we propose the first (to our knowledge) integration of ontology languages with preferences as in relational databases by developing PrefDatalog+/-, an extension of the Datalog+/- family of languages with preference management formalisms closely related to those previously studied for relational databases. We focus on two kinds of answers to queries that are relevant to this setting, skyline and k-rank (a generalization of top-k queries), and develop algorithms for computing these answers to both DAQs (disjunctions of atomic queries) and CQs (conjunctive queries). We show that DAQ answering in PrefDatalog+/- can be done in polynomial time in the data complexity, as in relational databases, as long as query answering can also be done in polynomial time (in the data complexity) in the underlying classical ontology.

We define a family of epistemic extensions of Halpern-Shoham logic for reasoning about temporal-epistemic properties of multi-agent systems. We exemplify their use and study the complexity of their model checking problem. We show a range of results ranging from PTIME to PSPACE-hard depending on the logic considered.

In dynamic systems, state constraints are formulas that hold in every reachable state. It has been shown that state constraints can be used to greatly reduce the planning search space. They are also useful in program verification. In this paper, we propose a sound but incomplete method for automatic verification and discovery of state constraints for a class of action theories that include many planning benchmarks. Our method is formulated in the situation calculus, theoretically based on Skolemization and Herbrand Theorem, and implemented with SAT solvers. Basically, we verify a state constraint by strengthening it in a novel and smart way so that it becomes a state invariant. We experimented with the blocks world, logistics and satellite domains, and the results showed that, almost all known state constraints can be verified in a reasonable amount of time, and meanwhile succinct and intuitive related state constraints are discovered.

Answer Set Programming Modulo Theories (ASPMT) is a new framework of tight integration of answer set programming (ASP) and satisfiability modulo theories (SMT). Similar to the relationship between first-order logic and SMT, it is based on a recent proposal of the functional stable model semantics by fixing interpretations of background theories. Analogously to a known relationship between ASP and SAT, "tight'' ASPMT programs can be translated into SMT instances. We demonstrate the usefulness of ASPMT by enhancing action language C+ to handle continuous changes as well as discrete changes. We reformulate the semantics of C+ in terms of ASPMT, and show that SMT solvers can be used to compute the language. We also show how the language can represent cumulative effects on continuous resources.

The action description languages B and C have significant common core. Nevertheless, some expressive possibilities of B are difficult or impossible to simulate in C, and the other way around. The main advantage of B is that it allows the user to give Prolog-style recursive definitions, which is important in applications. On the otherhand, B solves the frame problem by incorporating the commonsense law of inertia in its semantics, which makes it difficult to talk about fluents whose behavior is described by defaults other than inertia. In C and in its extension C+, the inertia assumption is expressed by axioms that the user is free to include or not to include, and other defaults can be postulated as well. This paper defines a new action description language, called BC, that combines the attractive features of B and C. Examples of formalizing commonsense domains discussed in the paper illustrate the expressive capabilities of BC and the use of answer set solvers for the automation of reasoning about actions described inthis language.

Fuzzy description logics (DLs) serve as a tool to handle vagueness in real-world knowledge. There is particular interest in logics implementing Lukasiewicz semantics, which has a number of favourable properties. Current decision procedures for Lukasiewicz fuzzy DLs work by reduction to exponentially large mixed integer programming problems. Here, we present a decision method that stays closer to logical syntax, a labelled tableau algorithm for Lukasiewicz Fuzzy ALC that calls only on (pure) linear programming, and this only to decide atomic clashes. The algorithm realizes the best known complexity bound, NEXPTIME. Our language features a novel style of fuzzy ABoxes that work with comparisons of truth degrees rather than explicit numerical bounds.

Counting the models of a propositional formula is a key issue for a number of AI problems, but few propositional languages offer the possibility to count models efficiently. In order to fill the gap, we introduce the language EADT of (extended) affine decision trees. An extended affine decision tree simply is a tree with affine decision nodes and some specific decomposable conjunction or disjunction nodes. Unlike standard decision trees, the decision nodes of an EADT formula are not labeled by variables but by affine clauses. We study EADT, and several subsets of it along the lines of the knowledge compilation map. We also describe a CNF-to-EADT compiler and present some experimental results. Those results show that the EADT compilation-based approach is competitive with (and in some cases is able to outperform) the model counter Cachet and the d-DNNF compilation-based approach to model counting.

While function symbols are widely acknowledged as an important feature in logic programming, they make common inference tasks undecidable. To cope with this problem, recent research has focused on identifying classes of logic programs imposing restrictions on the use of function symbols, but guaranteeing decidability of common inference tasks. This has led to several criteria, called termination criteria, providing sufficient conditions for a program to have finitely many stable models, each of finite size.This paper introduces the new class of bounded programs which guarantees the aforementioned property and strictly includes the classes of programs determined by current termination criteria. Different results on the correctness, the expressiveness, and the complexity of the class of bounded programs are presented.

We introduce a new approach to disjunctive ASP solving that aims at an equitable interplay between "generating" and "testing" solver units. To this end, we develop novel characterizations of answer sets and unfounded sets allowing for a bidirectional dynamic information exchange between solver units for orthogonal tasks. This results in the new multi-threaded disjunctive ASP solver claspD-2, greatly improving the performance of existing systems.

Entities in two-dimensional space are often approximated using rectangles that are parallel to the two axes that define the space, so-called minimum-bounding rectangles (MBRs). MBRs are popular in Computer Vision and other areas as they are easy to obtain and easy to represent. In the area of Qualitative Spatial Reasoning, many different spatial representations are based on MBRs. Surprisingly, there has been no such representation proposed for general rectangles, i.e., rectangles that can have any angle, nor for general solid rectangles (GSRs) that cannot penetrate each other. GSRs are often used in computer graphics and computer games, such as Angry Birds, where they form the building blocks of more complicated structures. In order to represent and reason about these structures, we need a spatial representation that allows us to use GSRs as the basic spatial entities. In this paper we develop and analyze a qualitative spatial representation for GSRs. We apply our representation and the corresponding reasoning methods to solve a very interesting practical problem: Assuming we want to detect GSRs in computer games, but computer vision can only detect MBRs. How can we infer the GSRs from the given MBRs? We evaluate our solution and test its usefulness in a real gaming scenario.