In the field of psychology, a considerable amount of knowledge is expressed using only natural language, which complicates accurate studies and comparisons. We believe that Answer Set Programming (ASP) can be used successfully for the formalization of psychological knowledge. To demonstrate the viability of ASP for this task, in this paper we develop an ASP-based formalization of the mechanics of Short-Term Memory, and show how it correctly reproduces the observed behavior of human subjects.

In this paper, we propose a progression semantics for first-order answer set programs. Based on this new semantics, we are able to define the notion of boundedness for answer set programming. We prove that boundedness coincides with the notions of recursion-free and loop-free under program equivalence, and is also equivalent to first-order definability of answer set programs on arbitrary structures.

Cardinality constraints or, more generally, weight constraints are well recognized as an important extension of answer-set programming. Clearly, all common algorithmic tasks related to programs with cardinality or weight constraints (PWCs) - like checking the consistency of a program - are intractable. Many intractable problems in the area of knowledge representation and reasoning have been shown to become tractable if the treewidth of the programs or formulas under consideration is bounded by some constant. The goal of this paper is to apply the notion of treewidth to PWCs and to identify tractable fragments. It will turn out that the straightforward application of treewidth to PWCs does not suffice to obtain tractability. However, by imposing further restrictions, tractability can be achieved.

We address the problem of repairing large-scale biological networks and corresponding yet often discrepant measurements in order to predict unobserved variations. To this end, we propose a range of different operations for altering experimental data and/or a biological network in order to re-establish their mutual consistency-an indispensable prerequisite for automated prediction. For accomplishing repair and prediction, we take advantage of the distinguished modeling and reasoning capacities of Answer Set Programming. We validate our framework by an empirical study on the widely investigated organism Escherichia coli.

We study the problem of reasoning from incoherent answer set programs, i.e., from logic programs that do not have an answer set due to cyclic dependencies of an atom from its default negation. As a starting point we consider so-called semi-stable models which have been developed for this purpose building on a program transformation, called epistemic transformation. We give a model-theoretic characterization of this semantics, considering pairs of two-valued interpretations of the original program, rather than resorting to its epistemic transformation. Moreover, we show some anomalies of semi-stable semantics with respect to basic epistemic properties and propose an alternative semantics satisfying these properties. In addition to a model-theoretic and a transformational characterization of the alternative semantics, we prove precise complexity results for main reasoning tasks under both semantics.

We present a decidable class of first-order formulas in the general theory of stable models that can be instantiated even in the presence of function constants. The notion of an argument-restricted formula presented here is a natural generalization of both the notion of an argument-restricted program and the notion of a semi-safe sentence that have been studied in different contexts. Based on this new notion, we extend the notion of safety defined by Cabalar, Pearce and Valverde to arbitrary formulas that allow function constants, and apply the result to $\raspl$ programs and programs with arbitrary aggregates, ensuring finite groundability of those programs in the presence of function constants. We also show that under a certain syntactic condition, argument-restricted formulas can be turned into argument-restricted programs.

A wide range of problems, from contingent and multiagent planning to process/service orchestration, can be viewed as games. In many of these, it is natural to spec- ify the possible behaviors procedurally. In this paper, we develop a logical framework for specifying these types of problems/games based on the situation calculus and ConGolog. The framework incorporates game-theoretic path quantifiers as in ATL. We show that the framework can be used to model such problems in a natural way. We also show how verification/synthesis techniques can be used to solve problems expressed in the framework. In particular, we develop a method for dealing with infinite state settings using fixpoint approximation and “characteristic graphs”.

We present a framework for reasoning about actions that not only solves the frame and ramification problems, but also the state default problem—the problem to determine what normally holds at a given time point. Yet, the framework is general enough not to be tied to a specific time structure. This is achieved as follows: We use effect axioms that draw ideas both from Reiter's successor state axioms and the non-monotonic causal theories by Giunchiglia et al. These axioms are formulated in a recently proposed unifying action calculus to guarantee independence of a specific underlying notion of time. Reiter's default logic is then wrapped around the resulting calculus and plays a key role in solving the ramification as well as the state default problem.

A plan with rich control structures like branches and loops can usually serve as a general solution that solves multiple planning instances in a domain. However, the correctness of such generalized plans is non-trivial to define and verify, especially when it comes to whether or not a plan works for all of the infinitely many instances of the problem. In this paper, we give a precise definition of a generalized plan representation called an FSA plan, with its semantics defined in the situation calculus. Based on this, we identify a class of infinite planning problems, which we call one-dimensional (1d), and prove a correctness result that 1d problems can be verified by finite means. We show that this theoretical result leads to a practical algorithm that does this verification practically, and a planner based on this verification algorithm efficiently generates provably correct plans for 1d problems.

We provide two approaches for explaining inconsistency in multi-context systems, where decentralized and heterogeneous system parts interact via nonmonotonic bridge rules. Inconsistencies arise easily in such scenarios, and nonmonotonicity calls for specific methods of inconsistency analysis. Both our approaches characterize inconsistency in terms of involved bridge rules: either by pointing out rules which need to be altered for restoring consistency, or by finding combinations of rules which cause inconsistency. We show duality and modularity properties, give precise complexity characterizations, and provide algorithms for computation using HEX-programs. Our results form a basis for inconsistency management in heterogeneous knowledge integration systems.