In this paper, we propose a translation from normal first-order logic programs under the answer set semantics to first-order theories on finite structures. Specifically, we introduce ordered completions which are modifications of Clark's completions with some extra predicates added to keep track of the derivation order, and show that on finite structures, classical models of the ordered-completion of a normal logic program correspond exactly to the answer sets (stable models) of the logic program.

This paper summarizes our line of research about the introduction of function symbols (functions) in Answer Set Programming (ASP) – a powerful language for knowledge representation and reasoning. The undecidability of reasoning on ASP with functions, implied that functions were subject to severe restrictions or disallowed at all, drastically limiting ASP applicability. We overcame most of the technical difficulties preventing this introduction, and we singled out a highly expressive class of programs with functions (FG-programs), allowing the (possibly recursive) use of function terms in the full ASP language with disjunction and negation. Reasoning on FG-programs is decidable, and they can express any computable function (causing membership in this class to be semi-decidable). We singled out also FD-programs, a subset of FG-programs which are effectively recognizable, while keeping the computability of reasoning. We implemented all results into the DLV system, thus obtaining an ASP system allowing to encode any computable function in a rich and fully declarative KRR language, ensuring termination on every FG program. Finally, we singled out the class of DFRP programs, where decidability of reasoning is guaranteed and Prolog-like functions are allowed.

We introduce DTProbLog, a decision-theoretic extension of Prolog and its probabilistic variant ProbLog. DTProbLog is a simple but expressive probabilistic programming language that allows the modeling of a wide variety of domains, such as viral marketing. In DTProbLog, the utility of a strategy (a particular choice of actions) is defined as the expected reward for its execution in the presence of probabilistic effects. The key contribution of this paper is the introduction of exact, as well as approximate, solvers to compute the optimal strategy for a DTProbLog program and the decision problem it represents, by making use of binary and algebraic decision diagrams.  We also report on experimental results that show the effectiveness and the practical usefulness of the approach.

Approaches to reasoning about knowledge in imperfect information games typically involve an exhaustive description of the game, the dynamics characterized by a tree and the incompleteness in knowledge by information sets. Such specifications depend on a modeler's intuition, are tedious to draft and vague on where the knowledge comes from. Also, formalisms proposed so far are essentially propositional, which, at the very least, makes them cumbersome to use in realistic scenarios. In this paper, we propose to model imperfect information games in a new multi-agent epistemic variant of the situation calculus. By using the concept of only-knowing, the beliefs and non-beliefs of players after any sequence of actions, sensing or otherwise, can be characterized as entailments in this logic. We show how de re vs. de dicto belief distinctions come about in the framework. We also obtain a regression theorem for multi-agent beliefs, which reduces reasoning about beliefs after actions to reasoning about beliefs in the initial situation.

Representations that combine first-order logic and probability have been the focus of much recent research. Lifted inference algorithms for them avoid grounding out the domain, bringing benefits analogous to those of resolution theorem proving in first-order logic. However, all lifted probabilistic inference algorithms to date treat potentials as black boxes, and do not take advantage of their logical structure. As a result, inference with them is needlessly inefficient compared to the logical case. We overcome this by proposing the first lifted probabilistic inference algorithm that exploits determinism and context specific independence. In particular, we show that AND/OR search can be lifted by introducing POWER nodes in addition to the standard AND and OR nodes. Experimental tests show the benefits of our approach.

Approximation (WARA-2010), scheduled to be held on July Topics of interest for this AAAI workshop include all 12, 2010 in Atlanta, Georgia, USA in conjunction with aspects of abstraction, reformulation and approximation, AAAI-10, aims to provide a forum for intensive interaction including (but not limited to) the following: new techniques among researchers in all areas of artificial intelligence for automatically constructing and selecting appropriate and computer science with an interest in the different aspects ARA methods; frameworks that unify and classify of abstraction, reformulation, and approximation techniques. ARA techniques; empirical and theoretical studies of the The goal and scope of this workshop are similar to costs and benefits of ARA; applications of ARA to search, an independent symposium called SARA. The diverse backgrounds constraint satisfaction, deterministic and probabilistic planning, of participants of previous SARA symposia has led theorem proving, logic programming, game playing, to a rich and lively exchange of ideas, allowed the comparison parallel and distributed search, distributed data and knowledge of goals, techniques, and paradigms, and helped identify bases, internet search and navigation, knowledge compilation, important research issues and engineering hurdles. This knowledge acquisition, knowledge reformulation, workshop continues to do the same.

Inductive Logic Programming (ILP) deals with the problem of finding a hypothesis covering positive examples and excluding negative examples, where both hypotheses and examples are expressed in first-order logic. In this paper we employ constraint satisfaction techniques to model and solve a problem known as template ILP consistency, which assumes that the structure of a hypothesis is known and the task is to find a unification of the contained variables such that no negative example is subsumed by the hypothesis and all positive examples are subsumed.

In this paper, we introduce Bayesian Abductive Logic Programs (BALPs), a new formalism that integrates Bayesian Logic Programs (BLPs) and Abductive Logic Programming (ALP) for abductive reasoning. Like BLPs, BALPs also combine first-order logic and Bayesian networks. However, unlike BLPs that use logical deduction to construct Bayes nets, BALPs employ logical abduction. As a result, BALPs are more suited for solving problems like plan/activity recognition and diagnosis that require abductive reasoning. First, we present the necessary enhancements to BLPs in order to support logical abduction. Next, we apply BALPs to the task of plan recognition and demonstrate its efficacy on two data sets. We also compare the performance of BALPs with several existing approaches for abduction.

We present a formal approach for combining programming by demonstration (PbD) with programming by instruction (PbI) — a largely unsolved problem. Our solution is based on the integration of two successful formalisms: version space algebras and the logic programming language Golog. Version space algebras have been successfully applied to programming by demonstration. Intuitively, a version space describes a set of candidate procedures and a learner filters this space as necessary to be consistent with all given demonstrations of the target procedure. Golog, on the other hand, is a logical programming language defined in the situation calculus that allows for the specification of non-deterministic programs. While Golog was originally proposed as a means for integrating programming and automated planning, we show that it serves equally well as a formal framework for integrating PbD and PbI. Our approach is the result of two key insights: (a) Golog programs can be used to define version spaces, and (b) with only a minor augmentation, the existing Golog semantics readily provides the update-function for such version spaces, given demonstrations. Moreover, as we will show, two or more programs can be symbolically synchronized, resulting in the intersection of two, possibly infinite, version spaces. The framework thus allows for a rather flexible integration of PbD and PbI, and in addition establishes a new connection between two active research areas, enabling cross-fertilization.

We describe how to use propositional model counting for a quantitative analysis of product configuration data. Our approach computes valuable meta information such as the total number of valid configurations or the relative frequency of components. This information can be used to assess the severity of documentation errors or to measure documentation quality. As an application example we show how we apply these methods to product documentation formulas of the Mercedes-Benz line of vehicles. In order to process these large formulas we developed and implemented a new model counter for non-CNF formulas. Our model counter can process formulas, whose CNF representations could not be processed up till now.