We study logical principles connecting two relations: independence, which is known as nondeducibility in the study of information flow, and functional dependence. Two different epistemic interpretations for these relations are discussed: semantics of secrets and probabilistic semantics. A logical system sound and complete with respect to both of these semantics is introduced and is shown to be decidable.

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.

We consider positive rules in which the conclusion may contain existentially quantified variables, which makes reasoning tasks (such as Deduction) undecidable. These rules, called "ForallExists-rules," have the same logical form as TGD (tuple-generating dependencies) in databases and as conceptual graph rules. The aim of this paper is to provide a clearer picture of the frontier between decidability and non-decidability of reasoning with these rules. We show that Deduction remains undecidable with a single rule; then we show that none of the known abstract decidable classes is recognizable. Turning our attention to concrete decidable classes, we provide new classes and classify all known classes by inclusion. Finally, we study, in a systematic way, the question "given two decidable sets of rules, is their union decidable?" and provide an answer for all known decidable cases except one.

We present a novel algorithm and a new understanding of reasoning about a sequence of deterministic actions with a probabilistic prior. When the initial state of a dynamic system is unknown, a probability distribution can be still specified over the initial states. Estimating the posterior distribution over states filtering after some deterministic actions occurred is a problem relevant to AI planning, natural language processing (NLP), and robotics among others. Current approaches to filtering deterministic actions are not tractable even if the distribution over the initial system state is represented compactly. The reason is that state variables become correlated after a few steps. The main innovation in this paper is a method for sidestepping this problem by redefining state variables dynamically at each time step such that the posterior for time t is represented in a factored form. This update is done using a progression algorithm as a subroutine, and our algorithm's tractability follows when that subroutine is tractable. Our results are for general deterministic actions and in particular, our algorithm is tractable for one-to-one and STRIPS actions. We apply our reasoning algorithm about deterministic actions to reasoning about sequences of probabilistic actions and improve the efficiency of the current probabilistic reasoning approaches. We demonstrate the efficiency of the new algorithm empirically over AI-Planning data sets.

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.