A general game player is a system that understands the rules of an unknown game and learns to play this game well without human intervention. To succeed in this endeavor, systems need to be able to extract and prove game-specific knowledge from the mere game rules. We present a practical approach to this challenge with the help of Answer Set Programming. The key idea is to reduce the automated theorem proving task to a simple proof of an induction step and its base case. We prove correctness of this method and report on experiments with an off-the-shelf Answer Set Programming system in combination with a successful general game player.

We look at composition of (possibly nonterminating) high-level programs over situation calculus action theories. Specifically the problem we look at is as follows: given a library of available ConGolog programs and a target program not in the library, verify whether the target program executions be realized by composing fragments of the executions of the available programs; and, if so, synthesize a controller that does the composition automatically. This kind of composition problems have been investigated in the CS and AI literature, but always assuming finite states settings. Here, instead, we investigate the issue in the context of infinite domains that may go through an infinite number of states as a result of actions.  Obviously in this context the problem is undecidable. Nonetheless, by exploiting recent results in the AI literature, we devise a sound and well characterized technique to actually solve the problem.

This article falls within the field of abstract argumentation frameworks. In particular, we focus on the study of frameworks using a proof procedure based on dialectical trees. These trees rely on a marking procedure to determine the warrant status of their root argument. Thus, our objective is to formulate rationality postulates to characterize the marking criterion over dialectical trees. The behavior of the marking procedure is closely tied to the alteration of trees, which is the keystone of any model of change based on dialectical argumentation. Hence, the results achieved in this work will benefit research on dynamics in argumentation.

The problem of revising an ontology consistently is closely related to the problem of belief revision which has been widely discussed in the literature. Some syntax-based belief revision operators have been adapted to revise ontologies in Description Logics (DLs). However, these operators remove the whole axioms to resolve logical contradictions and thus are not fine-grained. In this paper, we propose three model-based revision operators to revise terminologies in DLs. We show that one of them is more rational than others by comparing their logical properties. Therefore, we focus on this revision operator. We also consider the problem of computing the result of revision by our operator with the help of the notion of concept forgetting. Finally, we analyze the computational complexity of our revision operator.

We propose a new framework for reasoning about knowledge, action and time for domains that include actions with non-deterministic and context-dependent effects. The axiomatization is based on the Event Calculus and combines the expressiveness of possible worlds semantics with the efficiency of approaches that dispense the use of the accessibility relation. The framework is proved logically sound and, when restricted to deterministic domains, is also logically complete. To prove correctness of the approach, we construct a knowledge theory based on a branching version of the Event Calculus and study their correlation.

Calendar management tools assist users with coordinating their daily life. Different tasks have to be scheduled according to the user preferences. In many cases, tasks are at different locations and travel times have to be considered. Therefore, these kinds of calendar management problems can be regarded as spatio-temporal optimisation problems and are often variants of traveling salesman problems (TSP) or vehicle routing problems. While standard TSPs require a solution to include all tasks, prize-collecting TSPs are more suited for calendar management problems as they require a solution that optimises the total sum of prizes we assigned to tasks at different locations. If we now add time windows that limit when tasks can occur, these prize-collecting TSPs with time windows (TW-TSP) are excellent abstractions of spatio-temporal optimisation problems such as calendar management. Due to the inherent complexity of TW-TSPs, the existing literature considers mainly approximation algorithms or special cases. We present a novel algorithm for TW-TSPs that enables us to find the optimal solution to TW-TSP problems occurring in real-world calendar management applications efficiently. Our algorithm is a fixed-parameter tractable algorithm that depends on the maximal number of tasks that can be revisited from some other task, a parameter which is small in the application scenario we consider.

Dung's abstract theory of argumentation has become established as a general framework for various species of non-monotonic reasoning, and reasoning in the presence of conflict. A Dung framework consists of arguments related by attacks, and the extensions of a framework, and so the status of arguments, are defined under different semantics. Developments of Dung's work have also defined argument labellings as an alternative way of characterising extensions, and dialectical argument game proof theories for establishing the status of individual arguments. Recently, Extended Argumentation Frameworks extend Dung's theory so that arguments not only attack arguments, but attacks themselves. In this way, the extended theory provides an abstract framework for principled integration of meta-level argumentation about defeasible preferences applied to resolve conflicts between object level arguments. In this paper we formalise labellings and argument games for a selection of Dung's semantics defined for the extended frameworks.

The aim of this work is to propose a logical framework for the specification of cognitive emotions that are based on counterfactual reasoning about agents’ choices. An example of this kind of emotions is regret. In order to meet this objective, we exploit the well-known STIT logic [Belnap et al., 2001; Horty, 2001]. STIT logic has been proposed in the domain of formal philosophy in the nineties and, more recently, it has been imported into the field of theoretical computer science where its formal relationships with other logics for multiagent systems such as ATL and Coalition Logic (CL) have been studied. STIT is a very suitable formalism to reason about choices and capabilities of agents and groups of agents. Unfortunately, the version of STIT with agents and groups has been recently proved to be undecidable. In this work we study a decidable fragment of STIT with agents and groups which is sufficiently expressive for our purpose of formalizing counterfactual emotions.

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.

Increasing the expressiveness of qualitative spatial calculi is an essential step towards meeting the requirements of applications. This can be achieved by combining existing calculi in a way that we can express spatial information using relations from both calculi. The great challenge is to develop reasoning algorithms that are correct and complete when reasoning over the combined information. Previous work has mainly studied cases where the interaction between the combined calculi was small, or where one of the two calculi was very simple. In this paper we tackle the important combination of topological and directional information for extended spatial objects. We combine some of the best known calculi in qualitative spatial reasoning (QSR), the RCC8 algebra for representing topological information, and the Rectangle Algebra (RA) and the Cardinal Direction Calculus (CDC) for directional information. Although CDC is more expressive than RA, reasoning with CDC is of the same order as reasoning with RA. We show that reasoning with basic RCC8 and basic RA relations is in P, but reasoning with basic RCC8 and basic CDC relations is NP-Complete.