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.

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.

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.

A Forgetting is an operation for eliminating variables from a semantic theory of forgetting for normal logic programs knowledge base (Lin and Reiter 1994; Lang, Liberatore, and under answer set semantics is introduced in (Wang, Sattar, Marquis 2003). It constitutes a reduction in an agent's language and Su 2005), in which a sound and complete algorithm or, more accurately, the agent's signature. It has also is developed based on a series of program transformations; been studied under different names, such as variable elimination, this theory is further developed and extended uniform interpolation and relevance (Subramanian, to disjunctive logic programs in (Eiter and Wang 2006; Greiner, and Pearl 1997). Forgetting has various possible 2008). However, this theory of forgetting is defined in terms applications in a reasoning system. For example, in query of answer sets rather than SE models, and so again is not answering, if one can determine what is relevant to a query, syntax-independent.

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.

The recent years have seen several proposals aimed at placing the revision of logic programs within the belief change frameworks established for classical logic. A crucial challenge of this task lies in the nonmonotonicity of standard logic programming semantics. Existing approaches have thus used the monotonic characterisation via SE-models to develop semantic revision operators, which however neglect any syntactic information, or reverted to a syntax-oriented belief base approach altogether. In this paper, we bridge the gap between semantic and syntactic techniques by adapting the idea of a partial meet construction from classical belief change. This type of construction allows us to define new model-based operators for revising as well as contracting logic programs that preserve the syntactic structure of the programs involved. We demonstrate the rationality of our operators by testing them against the classic AGM or alternative belief change postulates adapted to the logic programming setting. We further present an algorithm that reduces the partial meet revision or contraction of a logic program to performing revision or contraction only on the relevant subsets of that program.

We present a probabilistic extension of logic programs under the stable model semantics, inspired by the concept of Markov Logic Networks. The proposed language takes advantage of both formalisms in a single framework, allowing us to represent commonsense reasoning problems that require both logical and probabilistic reasoning in an intuitive and elaboration tolerant way.

An original method for the extraction of one maximal subset of a set of Boolean clauses that must be satisfiable with possibly mutually contradictory assumptive contexts is motivated and experimented. Noticeably, it performs a direct computation and avoids the enumeration of all subsets that are satisfiable with at least one of the contexts. The method applies for subsets that are maximal with respect to inclusion or cardinality.

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.

Our paper is actually two contributions in one. First, we argue that IBM's Jeopardy! playing machine needs a formal semantics. We present several arguments as we discuss the system. We also situate the work in the broader context of contemporary AI. Our second point is that the work in this area might well be done as a broad collaborative project. Hence our "Blue Sky'' contribution is a proposal to organize a polymath-style effort aimed at developing formal tools for the study of state of the art question-answer systems, and other large scale NLP efforts whose architectures and algorithms lack a theoretical foundation.