Model counting is the problem of computing the number of models that satisfy a given propositional theory. It has recently been applied to solving inference tasks in probabilistic logic programming, where the goal is to compute the probability of given queries being true provided a set of mutually independent random variables, a model (a logic program) and some evidence. The core of solving this inference task involves translating the logic program to a propositional theory and using a model counter. In this paper, we show that for some problems that involve inductive definitions like reachability in a graph, the translation of logic programs to SAT can be expensive for the purpose of solving inference tasks. For such problems, direct implementation of stable model semantics allows for more efficient solving. We present two implementation techniques, based on unfounded set detection, that extend a propositional model counter to a stable model counter. Our experiments show that for particular problems, our approach can outperform a state-of-the-art probabilistic logic programming solver by several orders of magnitude in terms of running time and space requirements, and can solve instances of significantly larger sizes on which the current solver runs out of time or memory.

This paper introduces a modal logic for reasoning about game strategies. The logic is based on a variant of the well-known game description language for describing game rules and further extends it with two modalities for reasoning about actions and strategies. We develop an axiomatic system and prove its soundness and completeness with respect to a specific semantics based on the state transition model of games. Interestingly, the completeness proof makes use of forgetting techniques that have been widely used in the KR&R literature. We demonstrate how general game-playing systems can apply the logic to develop game strategies.

The theory of (variable) forgetting has received significant attention in nonmonotonic reasoning, especially, in answer set programming. However, the problem of establishing a theory of forgetting for some expressive nonmonotonic logics such as McCarthy's circumscription is rarely explored.In this paper a theory of forgetting for propositional circumscription is proposed, which is not a straightforward adaption of existing approaches. In particular, some properties that are essential for existing proposals do not hold any longer or have to be reformulated. Several useful properties of the new forgetting are proved, which demonstrate suitability of the forgetting for circumscription. A sound and complete algorithm for the forgetting is developed and an analysis of computational complexity is given.

We analyze the relative expressiveness of the two-valued semantics of abstract argumentation frameworks, normal logic programs and abstract dialectical frameworks. By expressiveness we mean the ability to encode a desired set of two-valued interpretations over a given propositional vocabulary A using only atoms from A. While the computational complexity of the two-valued model existence problem for all these languages is (almost) the same, we show that the languages form a neat hierarchy with respect to their expressiveness. We then demonstrate that this hierarchy collapses once we allow to introduce a linear number of new vocabulary elements.

Broad application of answer set programming (ASP) for declarative problem solving requires the development of tools supporting the coding process. Program debugging is one of the crucial activities within this process. Modern ASP debugging approaches allow efficient computation of possible explanations of a fault. However, even for a small program a debugger might return a large number of possible explanations and selection of the correct one must be done manually. In this paper we present an interactive query-based ASP debugging method which extends previous approaches and finds the preferred explanation by means of observations. The system automatically generates a sequence of queries to a programmer asking whether a set of ground atoms must be true in all (cautiously) or some (bravely) answer sets of the program. Since some queries can be more informative than the others, we discuss query selection strategies which - given user's preferences for an explanation - can find the most informative query reducing the overall number of queries required for the identification of a preferred explanation.

A fundamental task in reasoning about action and change is projection, which refers to determining what holds after a number of actions have occurred. A powerful method for solving the projection problem is regression, which reduces reasoning about the future to reasoning about the initial state. In particular, regression has played an important role in the situation calculus and its epistemic extensions. Recently, a modal variant of the situation calculus was proposed, which allows an agent to revise its beliefs based on so-called belief conditionals as part of its knowledge base. In this paper, we show how regression can be extended to reduce beliefs about the future to initial beliefs in the presence of belief conditionals. Moreover, we show how any remaining belief operators can be eliminated as well, thus reducing the belief projection problem to ordinary first-order entailments.

Logic Programming and Argumentation Theory have been existing side by side as two separate, yet related, techniques in the field of Knowledge Representation and Reasoningfor many years.When Assumption-Based Argumentation (ABA) was first introduced in the nineties,the authors showed how a logic program can be encoded in an ABA framework andproved that the stable semantics of a logic program corresponds to the stable extension semantics of the ABA framework encoding this logic program.We revisit this initial work by provingthat the 3-valued stable semantics of a logic program coincides with the complete semantics of the encoding ABA framework,and that the L-stable semantics of this logic program coincides with the semi-stable semantics of the encoding ABA framework.Furthermore, we show how to graphically represent the structure of a logic program encoded in an ABA frameworkand that not only logic programming and ABA semanticsbut also Abstract Argumentation semantics can be easily applied to a logic program using these graphical representations.

Modularity is an essential aspect of knowledge representation theory and practice. It has received substantial attention. We introduce model-based modular systems, an abstract framework for modular knowledge representation formalisms, similar in scope to multi-context systems but employing a simpler information-flow mechanism. We establish the precise relationship between the two frameworks, showing that they can simulate each other. We demonstrate that recently introduced modular knowledge representation formalisms integrating logic programming with satisfiability and, more generally, with constraint satisfaction can be cast as modular systems in our sense. These results show that our formalism offers a simple unifying framework for studies of modularity in knowledge representation.

This paper proposes an alternative definition of elementary loops and extends the notion of proper loops for disjunctive logic programs. Different from normal logic programs, the computational complexities of recognizing elementary loops and proper loops for disjunctive programs are coNP-complete. To address this problem, we introduce weaker versions of both elementary loops and proper loops and provide polynomial time algorithms for identifying them respectively. On the other hand, based on the notion of elementary loops, the class of Head-Elementary-loop-Free (HEF) programs was presented, which can be turned into equivalent normal logic programs by shifting head atoms into bodies. However, the problem of recognizing an HEF program is coNP-complete. Then we present a subclass of HEF programs which generalizes the class of Head-Cycle-Free programs and provide a polynomial time algorithm to identify them. At last, some experiments show that both elementary loops and proper loops could be replaced by their weak versions in practice.

Lifschitz and Turner introduced the notion of the splitting set and provided a method to divide a logic program into two parts. They showed that the task of computing the answer sets of the program can be converted into the tasks of computing the answer sets of these parts. However, the empty set and the set of all atoms are the only two splitting sets for many programs, then these programs cannot be divided by the splitting method. In this paper, we extend Lifschitz and Turner's splitting set theorem to allow the program to be split by an arbitrary set of atoms, while some new atoms may be introduced in the process. To illustrate the usefulness of the result, we show that for some typical programs the splitting process is efficient and the program simplification problem can be investigated using the concept of splitting.