The following activity recognition problem is considered: a description of the action capabilities of an agent being observed is given. This includes the preconditions and effects of atomic actions and of the activities (sequences of actions) the agent may execute. Given this description and a set of propositions, called history, about action occurrences, intended actions and properties of the world all at various points in time, the problem is to complete the picture as much as possible and determine what has already happened, what the intentions of the agent are, and what may happen as a result of the agent acting on those intentions. We present a framework to solve these activity recognition problems based on a formal language for reasoning about actions that includes a notion of intended actions, and a corresponding formalization in answer set programming.

Local pattern mining is concerned with finding the set of patterns that satisfy a constraint in a database. We study local pattern mining in the context of ProbLog, a probabilistic Prolog system, and introduce an approach for finding correlated patterns in the form of queries in such a Prolog system. The approach combines principles of inductive logic programming, data mining and statistical relational learning. Experiments on a challenging biological network mining task provide evidence for the interestingness of the approach.

Modal correspondence theory is a powerful and effective way to guarantee that adding specific syntactic axioms to a modal logic is mirrored by requiring 'corresponding' properties of the underlying Kripke models. However, such axioms not only  quantify over all formulas, but they are also global  in the sense that the corresponding semantic property is assumed to hold for all states. However, in  for instance epistemic logic one would like to have  the flexibility to say that certain properties (like "agent b knows at least what agent a knows") are  true locally in a specific state, but not necessarily  globally, in all states. This would enable one to  say "currently, b knows at least what a knows, but  this is not common knowledge," or ". . . but this is  not always true," or ". . . but this could be changed  by action α." We offer a logic for "knowing at least  as," where the (global) axiom scheme Ka ϕ → Kb ϕ  is replaced by a (local) inference rule. We give  a complete modal system, and discuss some consequences of the axiom in an epistemic setting.  Our completeness proof also suggests how achieving such local properties can be generalized to other  axioms schemes and modal logics. 

We address the problem of providing a logical formalization of arithmetic in declarative modelling languages for NP search problems. The challenge is to simultaneously allow quantification over an infinite domain such as the natural numbers, provide natural modelling facilities, and control expressive power of the language. To address the problem, we introduce an extension of the model expansion (MX) based framework to finite structures embedded in an infinite secondary structure, together with "double-guarded" logics for representing MX specifications for these structures. The logics also contain multi-set functions (aggregate operations). Our main result is that these logics capture the complexity class NP on "small-cost" arithmetical structures. 

This is also a key issue in formalizing deals with incomplete information, preferences, negotiation, which seems to prefer argumentationbased and changing goals. We assume that each negotiation [Rahwan et al., 2003]. Recent proposals agent is equipped with a knowledge base for negotiation on formalizing negotiation (see, e.g., [Amgoud et al., 2006; which consists of a CRprogram, a set of possible Kakas and Moraitis, 2006; Rahwan et al., 2003]) seem to be assumptions, and a set of ordered goals.

We consider query answering on Description Logic (DL) ontologies with DBoxes, where a DBox is a set of assertions on individuals involving atomic concepts and roles called DBox predicates. The extension of a DBox predicate is exactly defined in every interpretation by the contents of the DBox, i.e., a DBox faithfully represents a database whose table names are the DBox predicates and the tuples are the DBox assertions. Our goals are (i) to find out whether the answers to a given query are solely determined by the DBox predicates and, if so, (ii) to find a rewriting of the query in terms of them. The resulting query can then be efficiently evaluated using standard database technology. We have that (i) can be reduced to entailment checking and (ii) can be reduced to finding an interpolant. We present a procedure for computing interpolants in the DL ALC with general TBoxes. We extend the procedure with standard tableau optimisations, and we discuss abduction as a technique for amending ontologies to gain definability of queries of interest.

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.

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.

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.