In this paper, we address the problem of merging multiple imprecise probabilistic beliefs represented as Probabilistic Logic Programs (PLPs) obtained from multiple sources. Beliefs in each PLP are modeled as conditional events attached with probability bounds. The major task of syntax-based merging is to obtain the most rational probability bound for each conditional event from the original PLPs to form a new PLP. We require the minimal change principle to be followed so that each source gives up its beliefs as little as possible. Some instantiated merging operators are derived from our merging framework. Furthermore, we propose a set of postulates for merging PLPs, some of which extend the postulates for merging classical knowledge bases, whilst others are specific to the merging of probabilistic beliefs.

First order decision diagrams (FODD) were recently introduced as a compact knowledge representation expressing functions over relational structures. FODDs represent numerical functions that, when constrained to the Boolean range, use only existential quantification. Previous work developed a set of operations over FODDs, showed how they can be used to solve relational Markov decision processes (RMDP) using dynamic programming algorithms, and demonstrated their success in solving stochastic planning problems from the International Planning Competition in the system FODD-Planner. A crucial ingredient of this scheme is a set of operations to remove redundancy in decision diagrams, thus keeping them compact. This paper makes three contributions. First, we introduce Generalized FODDs (GFODD) and combination algorithms for them, generalizing FODDs to arbitrary quantification. Second, we show how GFODDs can be used in principle to solve RMDPs with arbitrary quantification, and develop a particularly promising case where an arbitrary number of existential quantifiers is followed by an arbitrary number of universal quantifiers. Third, we develop a new approach to reduce FODDs and GFODDs using model checking. This yields a reduction that is complete for FODDs and provides a sound reduction procedure for GFODDs.

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.