We consider the setting of ontological database access, where an A-box is given in form of a relational database D and where a Boolean conjunctive query q has to be evaluated against D modulo a T-box Σ formulated in DL-Lite or Linear Datalog+/-. It is well-known that (Σ, q) can be rewritten into an equivalent nonrecursive Datalog program P that can be directly evaluated over D. However, for Linear Datalog+/- or for DL-Lite versions that allow for role inclusion, the rewriting methods described so far result in a nonrecursive Datalog program P of size exponential in the joint size of Σ and q . This gives rise to the interesting question whether such a rewriting necessarily needs to be of exponential size. In this paper we show that it is actually possible to translate (Σ, q ) into a polynomially sized equivalent nonrecursive Datalog program P.

We introduce the framework of qualitative optimization problems (or, simply, optimization problems) to represent preference theories. The formalism uses separate modules to describe the space of outcomes to be compared (the generator) and the preferences on outcomes (the selector). We consider two types of optimization problems. They differ in the way the generator, which we model by a propositional theory, is interpreted: by the standard propositional logic semantics, and by the equilibrium-model (answer-set) semantics. Under the latter interpretation of generators, optimization problems directly generalize answer-set optimization programs proposed previously. We study strong equivalence of optimization problems, which guarantees their interchangeability within any larger context. We characterize several versions of strong equivalence obtained by restricting the class of optimization problems that can be used as extensions and establish the complexity of associated reasoning tasks. Understanding strong equivalence is essential for modular representation of optimization problems and rewriting techniques to simplify them without changing their inherent properties.

Existing methods for dealing with knowledge updates differ greatly depending on the underlying knowledge representation formalism. When Classical Logic is used, update operators are typically based on manipulating the knowledge base on the model-theoretic level. On the opposite side of the spectrum stand the semantics for updating Answer-Set Programs where most approaches need to rely on rule syntax. Yet, a unifying perspective that could embrace all these approaches is of great importance as it enables a deeper understanding of all involved methods and principles and creates room for their cross-fertilisation, ripening and further development. This paper bridges these seemingly irreconcilable approaches to updates. It introduces a novel monotonic characterisation of rules, dubbed \emph{\RE-models}, and shows it to be a more suitable semantic foundation for rule updates than \SE-models. A generic framework for defining semantic rule update operators is then proposed. It is based on the idea of viewing a program as the \emph{set of sets of \RE-models} of its rules; updates are performed by introducing additional interpretations to the sets of \RE-models of rules in the original program. It is shown that particular instances of the framework are closely related to both belief update principles and traditional approaches to rule updates and enjoy a range of plausible syntactic as well as semantic properties.

Belief revision has been extensively studied in the framework of propositional logic, but just recently revision within fragments of propositional logic has gained attention. Hereby it is not only the belief set and the revision formula which are given within a certain language fragment, but also the result of the revision has to be located in the same fragment. So far, research in this direction has been mainly devoted to the Horn fragment of classical logic. In this work, we present a general approach to define new revision operators derived from known operators (as for instance, Satoh's and Dalal's revision operators), such that the result of the revision remains in the fragment under consideration. Our approach is not limited to the Horn case but applicable to any fragment of propositional logic where the models of the formulas are closed under a Boolean function. Thus we are able to uniformly treat cases as dual-Horn, Krom and affine formulas, as well.

Computing minimal models is an important task in Knowledge Representation and Reasoning that appears in formalisms such as circumscription, diagnosis and answer set programming. Even the most basic question of whether there exists a minimal model containing a given variable is known to be $\Sigma_2^P$-complete. In this work we study the problem of computing minimal models from the viewpoint of parameterized complexity theory. We perform an extensive complexity analysis of this problem with respect to eleven parameters. Tractable fragments based on combinations of these parameters are identified by giving several fixed-parameter algorithms. For the remaining combinations we show parameterized hardness results and thus prove that under usual complexity theoretic assumptions no further fixed-parameter algorithms exist for these parameters.

We analyze, along the lines of the knowledge compilation map, both the tractability and the succinctness of the propositional language URC of unit-refutation complete propositional formulae, as well as its disjunctive closure URC[V, ∃], and a superset of URC where variables can be existentially quantified and unit-refutation completeness concerns only consequences built up from free variables.

Fixpoints play a key role in the mathematical set up of abstract argumentation theory but, we argue, have been relatively underexamined in the literature. The paper studies the logical structure underlying the computation via approximation sequences of the sort of fixpoints relevant in argumentation. Concretely, it presents a number of novel results on the fixed point theory underpinning the main Dung's semantics and, inspired by recent literature on the logical analysis of equilibrium computation in games, it provides a characterization of those semantics in terms of iterated model updates.

Abstract argumentation frameworks (AFs) provide the basis for various reasoning problems in the areas of Knowledge Representation and Artificial Intelligence. Efficient evaluation of AFs has thus been identified as an important research challenge. So far, implemented systems for evaluating AFs have either followed a straight-forward reduction-based approach or been limited to certain tractable classes of AFs. In this work, we present a generic approach for reasoning over AFs, based on the novel concept of complexity-sensitivity. Establishing the theoretical foundations of this approach, we derive several new complexity results for preferred, semistable and stage semantics which complement the current complexity landscape for abstract argumentation, providing further understanding on the sources of intractability of AF reasoning problems. The introduced generic framework exploits decision procedures for problems of lower complexity whenever possible. This allows, in particular, instantiations of the generic framework via harnessing in an iterative way current sophisticated Boolean satisfiability (SAT) solver technology for solving the considered AF reasoning problems. First experimental results show that the SAT-based instantiation of our novel approach outperforms existing systems.

In software testing, the small-scope hypothesis states that a high proportion of errors can be found by testing a program for all test inputs within some small scope. In this paper, we evaluate the small-scope hypothesis for answer-set programming (ASP). To this end, we follow work in traditional testing and base our evaluation on mutation analysis. In fact, we show that a rather limited scope is sufficient for testing ASP encodings from a representative set of benchmark problems. Our experimental evaluation facilitates effective methods for testing in ASP. Also, it gives some justification to analyse programs at the propositional level after grounding them over a small domain.

Answer set programming is a programming paradigm where a given problem is formalized as a logic program whose answer sets correspond to the solutions to the problem. In this paper, we link answer set programming with another widely applied paradigm, viz.~mixed integer programming. As a theoretical result, we establish translations from non-disjunctive logic programs to linear constraints used in mixed integer programming so that the solutions to the constraints correspond to the answer sets of the programs. These translations create the basis for an extended answer set programming language that includes linear constraints as a primitive and enables more compact encodings of problems. On a practical level, we have implemented a prototype system that computes answer sets using a state-of-the-art mixed integer programming solver. The reported experiments demonstrate the effectiveness of this approach applied to a number of optimization problems and problems with variables ranging over large domains.