In a seminal paper, Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. Unfortunately, progression is not first-order definable in general. Recently, Vassos, Lakemeyer, and Levesque showed that in case actions have only local effects, progression is first-order representable. However, they could show computability of the first-order representation only for a restricted class. Also, their proofs were quite involved. In this paper, we present a result stronger than theirs that for local-effect actions, progression is always first-order definable and computable. We give a very simple proof for this via the concept of forgetting. We also show first-order definability and computability results for a class of knowledge bases and actions with non-local effects. Moreover, for a certain class of local-effect actions and knowledge bases for representing disjunctive information, we show that progression is not only first-order definable but also efficiently computable.

In previous work, we proposed a modal fragment of the situation calculus called ES, which fully captures Reiter's basic action theories. ES also has epistemic features, including only-knowing, which refers to all that an agent knows in the sense of having a knowledge base. While our model of only-knowing has appealing properties in the static case, it appears to be problematic when actions come into play. First of all, its utility seems to be restricted to an agent's initial knowledge base. Second, while it has been shown that only-knowing correctly captures default inferences, this was only in the static case, and undesirable properties appear to arise in the presence of actions.  In this paper, we remedy both of these shortcomings and propose a new dynamic semantics of only-knowing, which is closely related to Lin and Reiter's notion of progression when actions are performed and where defaults behave properly.

On the other hand, the Recently, Ferraris, Lee and Lifschitz presented a solution provided by answer set programming (ASP), that is general definition of a stable model that is similar carried over to high level action language A [Gelfond and to the definition of circumscription, and can even Lifschitz, 1998] and many of its descendants that are based be characterized in terms of circumscription. In on ASP, uses both default negation (not) and strong negation this paper, we show the opposite direction, which ()--the idea of which is closely related to Reiter's default is, how to turn circumscription into the general stable logic solution [Reiter, 1980]. Interestingly, the development model semantics, and based on this, how to turn of the event calculus has spanned over both classical circumscriptive event calculus into answer set programs.

In this paper, we present a novel approach to the evaluation of propositional answer-set programs. In particular, for programs with bounded treewidth, our algorithm is capable of (i) computing the number of answer sets in linear time and (ii) enumerating all answer sets with linear delay. Our algorithm relies on dynamic programming, which so far has not been applied to ASP-problems. Therefore, our approach significantly differs from standard ASP-systems which implement techniques stemming from SAT or CSP, and thus usually do not exploit fixed parameter properties of the programs. We provide first experimental results which underline that, for programs with low treewidth, already a prototypical implementation is competitive compared to state-of-the-art systems.

Recently, the notion of accrual of arguments has received some attention from the argumentation community. Three principles for argument accrual have been identified as necessary to hold in argumentation frameworks. In this paper we propose an approach to model the accrual of arguments in the context of Defeasible Logic Programming, a logic programming approach to argumentation which has proven to be successful for many real-world applications. We will analyze the above mentioned principles in the context of our proposal, studying other interesting properties.

Splitting a logic program allows us to reduce the task of computing its stable models to similar tasks for smaller programs.  This idea is extended here to the general theory of stable models that replaces traditional logic programs by arbitrary first-order sentences and distinguishes between intensional and extensional predicates.  We discuss two kinds of splitting: a set of intensional predicates can be split into subsets, and a formula can be split into its conjunctive terms.

Current Answer Set Programming (ASP) solvers largely build on Datalog, which, unlike general logic programming, lacks function symbols. This limitation makes ASP decidable, but greatly complicates the modeling of indefinite time, recursive data structures (e.g., lists), and infinite processes and objects in general. Recent research thus aims at finding decidable fragments of ASP with function symbols and studying their complexity. We identify bidirectional ASP programs as an expressive, but yet decidable, language that is useful, e.g., for reasoning about actions involving both the future and the past. We tightly characterize the computational complexity of bidirectional programs and some of their subclasses, addressing the main reasoning tasks. Our results also show that the recently introduced FDNC programs can be extended by inverse rules while retaining decidability, but computational costs are unavoidably higher.

We present a method to decompose a declarative knowledge base, given by a logic program under Answer Set Semantics with access to external sources. It overcomes the ineffectiveness of current methods due to a lack of structural information about these sources, viewed as black boxes, by exploiting independency information in accesses to them.  To this end, we develop a generic notion of domain independence that allows to restrict the evaluation domain and, as a consequence, to prune unnecessary dependency assumptions between atoms. This leads to increased decomposability, which we demonstrate by an evaluation method for HEX-programs based on program rewriting. Experiments show that this may yield large performance gains. While developed for a particular formalism, the notions and ideas of this  paper might be adapted to related formalisms as well.

We present an unified methodology for representation and development of dialectical proof procedures in both abstract and assumption-based argumentation based on the notions of legal environments and dispute derivation. A legal environment specifies the legal moves of the dispute parties while a dispute derivation describes the procedure structure. A key insight of this paper is that the opponent moves determine the soundness of a dispute while its completeness depends on the proponent moves.

In this article we discuss two alternative proposals for neighbourhood semantics (which we call strict and loose neighbourhood semantics, NSS and NSL respectively) that have been previously introduced in the literature. Our main tools are suitable notions of bisimulation. While an elegant notion of bisimulation exists for NSL, the required bisimulation for NSS is rather involved. We propose a simple extension of NSS with a universal modality that we call NSS(E), which comes together with a natural notion of bisimulation. We also investigate the complexity of the satisfiability problem for NSL and NSS(E).