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.

Mixed integer linear programming (MILP) is a powerful representation often used to formulate decision-making problems under uncertainty. However, it lacks a natural mechanism to reason about objects, classes of objects, and relations. First-order logic (FOL), on the other hand, excels at reasoning about classes of objects, but lacks a rich representation of uncertainty. While representing propositional logic in MILP has been extensively explored, no theory exists yet for fully combining FOL with MILP. We propose a new representation, called first-order programming or FOP, which subsumes both FOL and MILP. We establish formal methods for reasoning about first order programs, including a sound and complete lifted inference procedure for integer first order programs. Since FOP can offer exponential savings in representation and proof size compared to FOL, and since representations and proofs are never significantly longer in FOP than in FOL, we anticipate that inference in FOP will be more tractable than inference in FOL for corresponding problems.

Circumscription and logic programs under the stable model semantics are two well-known nonmonotonic formalisms. The former has served as a basis of classical logic based action formalisms, such as the situation calculus, the event calculus and temporal action logics; the latter has served as a basis of a family of action languages, such as language A and several of its descendants. Based on the discovery that circumscription and the stable model semantics coincide on a class of canonical formulas, we reformulate the situation calculus and the event calculus in the general theory of stable models. We also present a translation that turns the reformulations further into answer set programs, so that efficient answer set solvers can be applied to compute the situation calculus and the event calculus.