Recent work on approximate linear programming (ALP) techniques for first-order Markov Decision Processes (FOMDPs) represents the value function linearly w.r.t. a set of first-order basis functions and uses linear programming techniques to determine suitable weights. This approach offers the advantage that it does not require simplification of the first-order value function, and allows one to solve FOMDPs independent of a specific domain instantiation. In this paper, we address several questions to enhance the applicability of this work: (1) Can we extend the first-order ALP framework to approximate policy iteration to address performance deficiencies of previous approaches? (2) Can we automatically generate basis functions and evaluate their impact on value function quality? (3) How can we decompose intractable problems with universally quantified rewards into tractable subproblems? We propose answers to these questions along with a number of novel optimizations and provide a comparative empirical evaluation on logistics problems from the ICAPS 2004 Probabilistic Planning Competition.

Combining first-order logic and probability has long been a goal of AI. Markov logic (Richardson & Domingos, 2006) accomplishes this by attaching weights to first-order formulas and viewing them as templates for features of Markov networks. Unfortunately, it does not have the full power of first-order logic, because it is only defined for finite domains. This paper extends Markov logic to infinite domains, by casting it in the framework of Gibbs measures (Georgii, 1988). We show that a Markov logic network (MLN) admits a Gibbs measure as long as each ground atom has a finite number of neighbors. Many interesting cases fall in this category. We also show that an MLN admits a unique measure if the weights of its non-unit clauses are small enough. We then examine the structure of the set of consistent measures in the non-unique case. Many important phenomena, including systems with phase transitions, are represented by MLNs with non-unique measures. We relate the problem of satisfiability in first-order logic to the properties of MLN measures, and discuss how Markov logic relates to previous infinite models.

Answer Set Programming (ASP) is a well-established paradigm of declarative programming in close relationship with other declarative formalisms such as SAT Modulo Theories, Constraint Handling Rules, FO(.), PDDL and many others. Since its first informal editions, ASP systems have been compared in the now well-established ASP Competition. The Third (Open) ASP Competition, as the sequel to the ASP Competitions Series held at the University of Potsdam in Germany (2006-2007) and at the University of Leuven in Belgium in 2009, took place at the University of Calabria (Italy) in the first half of 2011. Participants competed on a pre-selected collection of benchmark problems, taken from a variety of domains as well as real world applications. The Competition ran on two tracks: the Model and Solve (M&S) Track, based on an open problem encoding, and open language, and open to any kind of system based on a declarative specification paradigm; and the System Track, run on the basis of fixed, public problem encodings, written in a standard ASP language. This paper discusses the format of the Competition and the rationale behind it, then reports the results for both tracks. Comparison with the second ASP competition and state-of-the-art solutions for some of the benchmark domains is eventually discussed. To appear in Theory and Practice of Logic Programming (TPLP).

Human users who execute an automatically generated plan want to understand the rationale behind it. Knowledge-rich plans are particularly suitable for this purpose, because they provide the means to give reason for causal, temporal, and hierarchical relationships between actions. Based on this information, focused arguments can be generated that constitute explanations on an appropriate level of abstraction. In this paper, we present a formal approach to plan explanation. Information about plans is represented as first-order logic formulae and explanations are constructed as proofs in the resulting axiomatic system. With that, plan explanations are provably correct w.r.t. the planning system that produced the plan. A prototype plan explanation system implements our approach and first experiments give evidence that finding plan explanations is feasible in real-time.

Cardinality constraints or, more generally, weight constraints are well recognized as an important extension of answer-set programming. Clearly, all common algorithmic tasks related to programs with cardinality or weight constraints - like checking the consistency of a program - are intractable. Many intractable problems in the area of knowledge representation and reasoning have been shown to become linear time tractable if the treewidth of the programs or formulas under consideration is bounded by some constant. The goal of this paper is to apply the notion of treewidth to programs with cardinality or weight constraints and to identify tractable fragments. It will turn out that the straightforward application of treewidth to such class of programs does not suffice to obtain tractability. However, by imposing further restrictions, tractability can be achieved.

This paper introduces and studies a declarative framework for updating views over indefinite databases. An indefinite database is a database with null values that are represented, following the standard database approach, by a single null constant. The paper formalizes views over such databases as indefinite deductive databases, and defines for them several classes of database repairs that realize view-update requests. Most notable is the class of constrained repairs. Constrained repairs change the database "minimally" and avoid making arbitrary commitments. They narrow down the space of alternative ways to fulfill the view-update request to those that are grounded, in a certain strong sense, in the database, the view and the view-update request.

Argumentation is a natural meaning of reasoning in the daily life, and has also become a highly interested topic of knowledge representation in the past few years. In this paper, we will use the phrase "two-sided argumentation" for a type of formalization for our real world debate: an issue with a pro-side supports it and a con-side opposes it. Then, we will point out that, when we use the term "argumentation," we in fact mean a binary concept: a method of reasoning, and a type of negotiation. For both case, we will consider the semantics: argumentative models for the former, argumentation games for the latter. We will also give out some results about the relationship between them.

This paper addresses questions of the transition related to conscious processes and unconscious processes, namely aims to substantiating a primary framework to the following open question: The vast majority of brain activity is non-conscious. What is the criterion to distinguish the non-conscious activities from conscious ones? To support our answers in a principled way, we present a general framework for the study of mental processes resting on two main principles: firstly, we endorse Matte Blanco’s principle of symmetry by giving central stage to the concept of unconscious processes. Secondly, to structure and combine the notions of infinity and part-whole equivalence in a mathematical logic method, moreover we base our work on modern non-classical logics in the disposition of context-dependency, as forcefully put forward by CJS Clarke. In particular, we employ the paraconsistent logic as the underlying logical system for defining the general framework for mental processes, highly structural and formal representation, called bi-logic framework.

In some relative discussions about the conceptual analysis of translation paradox where people Studies about logic translation could be traced back to (Kolmogorov found the following situation paradoxical with an assumption 1925) (Glivenko 1929) (Gentzen 1933) (Gödel of stronger-weaker distinction about the strength of logics (1933). In this chapter, the discussion on Béziau's case of by weakening the condition of some logical constant on the translation paradox provides an easier way for people purpose: given two logics, one is weaker than the other in to understand how it is possible for people to consider the sense of proving everything the former proves, while at a more general and abstract logic by the bivaluation approach.

Modern SAT solvers are routinely used as core solving engines in vast numbers of different AI and industrial applications. In this short article, we will provide an overview of the SAT solver competitions. The solvers), and another one based on wall clock time, second SAT competition took place during the second which promotes solvers using all available Dimacs challenge in 1993 (Johnson and Trick resources to answer as quickly as possible (for 1996). Another SAT competition took place in answers incorrectly if it reports satisfiable but Beijing in 1996, organized by James Crawford. Each survey propagation (Braunstein and Zecchina category is defined through the type of instances 2004), a new approach to efficiently solve randomly used as benchmarks.