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.

We consider the problem of reasoning from inconsistent hybrid theories, i.e., combinations of a structural part given by a classical first order theory (e.g., an ontology) and a rules part as a set of declarative logic program rules (under answer-set semantics). Paraconsistent reasoning is achieved by defining an appropriate semantics, so-called paraconsistent semi-equilibrium model semantics for such hybrid theories. Appropriateness of the semantics is established with respect to desirable properties attesting design objectives, such us to generalize the underlying semantics in case of consistency, as well as to generalize existing paraconsistent semantics for the individual parts. A complexity analysis of corresponding reasoning tasks complements these results.

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.

Temporal logics can be used in reasoning about actions for specifying constraints on domain descriptions and temporal properties to be verified. In this paper, we exploit Bounded Model Checking (BMC) techniques in the verification of Dynamic Linear Time Temporal Logic (DLTL) properties of an action theory, which is formulated in a temporal extension of Answer Set Programming (ASP). To achieve completeness, we propose an approach to BMC which exploits the Buechi automaton construction while searching for a counterexample. We provide an encoding in ASP of the temporal action domain and of Bounded Model Checking of DLTL formulas.

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.

The stable model semantics treats a logic program as a mechanism for specifying its intensional predicates. In this paper we discuss a modification of that semantics in which functions, rather than predicates, are intensional. The idea of the new definition comes from nonmonotonic causal logic.

In classical logic, nonBoolean fluents, such as the location of an object and the color of a ball, can be naturally described by functions, but this is not the case with the traditional stable model semantics, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee and Lifschitz to allow intensional functions. The new formalism is closely related to multi-valued nonmonotonic causal logic, logic programs with intensional functions, and other extensions of logic programs with functions, while keeping similar properties as those of the first-order stable model semantics. We show how to eliminate intensional functions in favor of intensional predicates and vice versa, and use these results to encode fragments of the language in the input language of ASP solvers and CSP solvers.

We define a notion of bounded action theory in the situation calculus, where the theory entails that in all situations, the number of ground fluent atoms is bounded by a constant. Such theories can still have an infinite domain and an infinite set of states. We argue that such theories are fairly common in applications, either because facts do not persist indefinitely or because one eventually forgets some facts, as one learns new ones. We discuss various ways of obtaining bounded action theories. The main result of the paper is that verification of an expressive class of first-order mu-calculus temporal properties in such theories is in fact decidable.

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.

The advance of Internet and Sensor technology has brought about new challenges evoked by the emergence of continuous data streams. While existing data-stream management systems allow for high-throughput stream processing, they lack complex reasoning capacities. We address this shortcoming and elaborate upon an approach to knowledge-intense stream reasoning based on Answer Set Programming (ASP). The emphasis thus shifts from rapid data processing to complex reasoning. To accommodate this in ASP, we develop new techniques that allow us to formulate problem encodings dealing with emerging as well as expiring data in a seamless way. We thus propose novel language constructs and modeling techniques for specifying and reasoning with time-decaying logic programs.