| Sergei Odintsov and David Pearce. Routley Semantics for Answer Sets |
| Abstract: We present an alternative model theory for answer sets based on the possible worlds semantics proposed by Routley (1974) as a framework for the propositional logics of Fitch and Nelson. By introducing a falsity constant or second negation into Routley models, we show how paraconsistent as well as ordinary answer sets can be represented via a simple minimality condition on models. This means we can define in the obvious way a paraconsistent version of equilibrium logic, or paraconsistent answer sets (PAS) for propositional theories. The underlying logic N9 of PAS belongs to the lattice of logics studied by Odintsov (2004). We axiomatise the logic, showing it to be the least conservative extension of the logic of here-and-there with strong negation, representable via the full twist-structure on the 3-element Heyting algebra. The latter means that N9 can be viewed as a 9-valued logic. In addition, we show that the logic suffices to characterise the strong equivalence of programs in the paraconsistent case and can thus serve as a useful mathematical foundation for PAS. We conclude by showing that the logic has the Interpolation Property. |
| Paolo Ferraris. Answer Sets for Propositional Theories |
| Abstract: Equilibrium logic, introduced by David Pearce, extends the concept of an answer set from logic programs to arbitrary sets of formulas. Logic programs correspond to the special case in which every formula is a ``rule'' --- an implication that has no implications in the antecedent (body) and consequent (head). The semantics of equilibrium logic looks very different from the usual definitions of an answer set in logic programming, as it is based on Kripke models. In this paper we propose a new definition of equilibrium logic which uses the concept of a reduct as the standard definition of an answer set. Second, we apply the generalized concept of an answer set to the problem of defining the semantics of aggregates in answer set programming. We propose, in particular, a semantics for weight constraints that covers the problematic case of negative weights. Our semantics of aggregates is an extension of the approach due to Faber, Leone, and Pfeifer that includes choice rules and, more generally, arbitrary rules with nested expressions. |
| Francesco Buccafurri and Gianluca Caminiti. A Social Semantics for Multi-Agent Systems |
Abstract: As in human world many of our goals could not be achieved without interacting with other people, in case many agents are part of the same environment one agent should be aware that he is not alone and he cannot assume other agents sharing his own goals. Moreover, he may be required to interact with other agents and to reason about their mental state (beliefs, desires and intentions -- BDI) in order to find out potential friends to join with (or opponents to fight against).
In this paper we focus on a language derived from logic programming which both supports the representation of mental states of agent communities in a BDI-like fashion and provides each agent with the capability of reasoning about other agents' mental states and acting accordingly.
The proposed semantics is shown to be translatable into stable model semantics of logic programs with aggregates. |
| Martin Gebser and Torsten Schaub. Loops: Relevant or Redundant? |
| Abstract: Loops and the corresponding loop formulas play an important role in answer set programming. On the one hand, they are used for guaranteeing correctness and completeness in SAT-based answer set solvers. On the other hand, they can also be used by conventional answer set solvers for finding unfounded sets of atoms. Unfortunately, the number of loops has recently been shown to be exponential in the worst case. Loops are usually defined by means of the positive atom dependency graph. In what follows, we show that not all such loops are actually needed for the previous purposes. Rather we characterize a subset of so-called elementary loops by means of a program's positive body-head dependency graph. We show that every general loop is a union of elementary ones and that all elementary loops are essential for selecting the answer sets among the models of a program's completion. |
| Federico Banti, José Alferes, Antonio Brogi and Pascal Hitzler. A well supported semantics for multidimensional dynamic logic programs |
| Abstract: Multidimensional dynamic logic programs are a paradigm which allows to express (partially) hierarchically ordered evolving knowledge bases through (partially) ordered multi sets of logic programs and allowing to solve contradictions among rules in different programs by allowing rules in more important programs to reject rules in less important ones. These class of programs extends the class of dynamic logic program that provides meaning and semantics to sequences of logic programs. Recently a semantics named refined stable model semantics had solved some controversial behaviours of previously existing semantics for dynamic logic programs. However, it is not possible to directly extend the definitions and concepts of the refined semantics to the multidimensional case and hence more sophisticated principles and techniques are in order. In this paper we face the problem of defining a proper semantics for multidimensional dynamic logic programs by extending the idea of well supported model to this class of programs and by showing that this concept alone is enough for univocally characterizing a proper semantics. We show then how the newly defined semantics coincide with the refined one when applied to sequences of programs. |
| Marek Sergot and Robert Craven. Some logical properties of nonmonotonic causal theories |
| Abstract: The formalism of nonmonotonic causal theories, presented in a recent paper by Giunchiglia, Lee, Lifschitz, McCain, and Turner, provides a general purpose formalism for nonmonotonic reasoning and knowledge representation, as well as a higher level, special purpose notation, the action language C+, for specifying and reasoning about the effects of actions and the persistence (`inertia') of facts over time, with support for indirect effects, non-deterministic actions, and concurrency. In this paper we investigate some logical properties of these formalisms. The aims are twofold. From the technical point of view, we seek to gain additional insights into the properties of the formalism when viewed as a species of conditional logic. From the practical point of view, we are seeking to find conditions under which two sets of causal theories, or two action descriptions in C+, can be said to be equivalent, with the further aim of helping to decide between alternative formulations when constructing practical applications. |
| Wolfgang Faber. Unfounded Sets for Disjunctive Logic Programs with Arbitrary Aggregates |
Abstract: Aggregates in answer set programming (ASP) have recently been studied quite intensively. The main focus of previous work has been on defining suitable semantics for programs with arbitrary, potentially recursive aggregates. By now, these efforts appear to have converged. On another line of research, the relation between unfounded sets and (aggregate-free) answer sets has lately been rediscovered. It turned out that most of the currently available answer set solvers rely on this or closely related results.
In this paper, we unite these lines and give a new definition of unfounded sets for disjunctive logic programs with arbitrary, possibly recursive aggregates. While being syntactically somewhat different, we can show that this definition properly generalizes all notions of unfounded sets that have previously been defined for fragments of the language.
We demonstrate that, as for restricted languages, answer sets can be crisply characterized by unfounded sets. This result can be seen as a confirmation of the robustness of the definition of answer sets for arbitrary aggregates. We also provide a comprehensive complexity analysis for unfounded sets, and study its impact on answer set computation. |
| Victor W. Marek, Inna Pivkina and Miroslaw Truszczynski. Approximating answer sets of unitary Lifschitz-Woo programs |
| Abstract: We investigate techniques for approximating answer sets of general logic programs of Lifschitz and Woo, whose rules have single literals as heads. We propose three different methods of approximation and obtain results on the relationship between them. Since general logic programs with single literals as heads are equivalent to revision programs, we obtain results on approximations of justified revisions of databases by revision programs. |
| Joost Vennekens and Marc Denecker. An Algebraic Account of Modularity in ID-logic |
| Abstract: ID-logic uses ideas from the field of logic programming to extend second order logic with non-monotone inductive defintions. In this work, we reformulate the semantics of this logic in terms of approximation theory, an algebraic theory which generalizes the semantics of several non-monotonic reasoning formalisms. This allows us to apply certain abstract modularity theorems, developed within the framework of approximation theory, to ID-logic. As such, we are able to offer elegant and simple proofs of generalizations of known theorems, as well as some new results. |
| Paolo Ferraris. On Modular Translations and Strong Equivalence |
| Abstract: We are interested in the existence of a modular translation from one class of logic programs to another that would be sound under the answer set semantics. The main theorem of this paper characterizes this relationship between classes of programs in terms of strong equivalence. The theorem is used to study the expressiveness of several classes of programs, including the comparison of programs with cardinality constraints with programs with monotone cardinality atoms. |
| Alberto Finzi and Thomas Lukasiewicz. Game-Theoretic Reasoning about Actions in Nonmonotonic Causal Theories |
| Abstract: We present the action language GC+ for reasoning about actions in multi-agent systems with cooperative agents, which is a generalization of both the action language C+ and partially observable stochastic games. We provide a finite-horizon value iteration for this framework and show that it characterizes finite-horizon Nash equilibria. We also describe how the framework can be implemented on top of nonmonotonic causal theories. We then present acyclic action descriptions in GC+ as a special case where transitions are computable in polynomial time. We also give an example that shows the usefulness of our approach in practice. |
| Jean Gressmann, Tomi Janhunen, Robert Mercer, Torsten Schaub, Richard Tichy and Sven Thiele. Platypus: A platform for distributed answer set solving |
| Abstract: We propose a model to manage the distributed computation of answer sets within a general framework. This design incorporates a variety of software and hardware architectures and allows its easy use with a diverse cadre of computational elements. Starting from a generic algorithmic scheme, we develop a platform for distributed answer set computation, describe its current state of implementation, and give some experimental results. |
| Tran Cao Son, Phan Huy Tu, Michael Gelfond and A. Ricardo Morales. An Approximation of Action Theories of AL and its Application to Conformant Planning |
| Abstract: In this paper we further investigate the notion of approximation of action theories introduced in [Gelfond & Morales 2004, Son & Baral 2001]. We introduce a logic programming based method for constructing approximation of action theories of AL, study some properties of these approximations, describe several approximation based conformant planners, and compare their performance and degree of elaboration tolerance with other state-of-the-art conformant planners. |
| Antonis Kakas, Loizos Michael and Rob Miller. Modular-E: an Elaboration Tolerant Approach to the Ramification and Qualification Problems |
| Abstract: We describe Modular-E (ME), a specialized, model-theoretic logic for narrative reasoning about actions, able to represent non-deterministic domains involving concurrency, static laws (constraints) and indirect effects (ramifications). We give formal results which characterize ME’s high degree of modularity and elaboration tolerance, and show how these properties help to separate out, and provide a principled solutions to, the endogenous and exogenous qualification problems. We also show how a notion of (micro) processes can be used to facilitate reasoning at the dual levels of temporal granularity necessary for narrative-based domains involving “instantaneous” series of indirect and knock-on effects. |
| Wolfgang Faber and Francesco Ricca. Solving Hard ASP Programs Efficiently |
Abstract: Recent research on answer set programming (ASP) systems, has mainly focused on solving NP problems more efficiently. Yet, disjunctive logic programs allow for expressing every problem in the complexity classes SigmaP2 and PiP2. These classes are widely believed to be strictly larger than NP.
In this paper we focus on improving the evaluation of SigmaP2/PiP2-hard ASP programs. To this end, we define a new heuristic hDS and implement it in the (disjunctive) ASP system DLV. The definition of hDS is geared towards the peculiarites of hard programs, while it maintains the benign behaviour of the well-assessed heuristic of DLV for NP problems.
We have conducted extensive experiments with the new heuristic. hDS significantly outperforms the previous heuristic of DLV on hard 2QBF problems. We also compare the DLV system (with hDS) to the QBF solvers Ssolve, Quantor, Semprop, and yQuaffle, which performed best in the QBF evaluation of 2004. The results of the comparison indicate that ASP systems currently seem to be the best choice for solving SigmaP2/PiP2-complete problems. |
| Alex Dekhtyar and Michael I. Dekhtyar. Revisiting the Semantics of Interval Probabilistic Logic Programs |
Abstract: Two approaches to logic programming with probabilities emerged over time: bayesian reasoning and probabilistic satisfiability (PSAT). The attractiveness of the former is in tying the logic programming research to the body of work on Bayes networks. The second approach ties reasoning about probabilities with linear programming, and allows for natural expression of imprecision in probabilities via the use of intervals.
In this paper we construct precise semantics for one PSAT-based formalism for reasoning with inteval probabilities, probabilistic logic programs (p-programs), orignally considered by Ng and Subrahmanian. We show that the probability ranges of atoms and formulas in p-programs cannot be expressed as single intervals. We construct the prescise description of the set of models of p-programs and study the computational complexity if this problem, as well as the problem of consistency of a p-program. We also study the conditions under which our semantics coincides with the single-interval semantics originally proposed by Ng and Subrahmanian for p-programs. Our work sheds light on the complexity of construction of reasoning formalisms for imprecise probabilities and suggests that interval probabilities alone are inadequate to support such reasoning. |
| Jia-Huai You, Guohua Liu, Li Yuan Yuan and Curtis Onuczko. Lookahead in Smodels Compared to Local Consistencies in CSP |
| Abstract: In answer set programming systems like Smodels and some SAT solvers, constraint propagation is carried out by a mechanism called lookahead. The question arises as what the pruning power of lookahead is in these systems, and how such pruning power fares in comparison with the consistency techniques in solving constraint satisfaction problems. In this paper, we show how local consistencies of various degrees may be captured in lookahead. As a result, lookahead as a general constraint propagation mechanism for answer set and SAT solvers provides a uniform algorithm for enforcing a variety of local consistencies. |
| Francesco Calimeri and Giovambattista Ianni. External sources of computation for Answer Set Solvers |
| Abstract: The paper introduces Answer Set Programming with External Predicates (ASP-EX), a framework aimed at enabling ASP to deal with external sources of computation. This feature is realized by the introduction of parametric external predicates, whose extension is not specified by means of a logic program but implicitly computed through external code. With respect to existing approaches it is explicitly addressed the issue of invention of new information coming from external predicates, in form of new, and possibly infinite, constant symbols. Several decidable restrictions of the language are identified as well as suitable algorithms for evaluating Answer Set Programs with external predicates. The framework paves the way to Answer Set Programming in several directions such as Semantic Web applications, pattern manipulation as well as nearly unrestricted possibility to exploit function symbols. ASP-EX has been successfully implemented in the DLV system, which is now enabled to make external function calls. |
| Alvaro Cortes-Calabuig, Marc Denecker, Ofer Arieli, Bert Van Nuffelen and Maurice Bruynooghe. On the Local Closed-World Assumption of Data-Sources |
| Abstract: We present an alternative formalization of the local closed-world concept for relational data-sources. The idea amounts to specify the domain of expertise where a data-source stores complete knowledge about certain world. We separate the `explicit' data from the `implicit' assumptions about it. The information of the data-source remains a set of facts, while the external knowledge is expressed by a first-order theory; the combination of these two components will define the {\it meaning} of a data-source in a system of distributed knowledge. By this, one can still consider data-sources as relational databases, and process the information about their completeness by an independent reasoning system (sometimes called a mediator). We provide an expressive syntax and an intuitive semantics that facilitate its application in real-life representations, and we show how our formalization matches, under certain assumptions, with alternative proposals. |
| Iseline Engan, Tore Langholm, Espen Lian and Arild Waaler. Default Reasoning with Preference within Only Knowing Logic |
| Abstract: The main construction in this paper is an encoding of default logic into an ``Only knowing'' logic with confidence levels. By means of simple and natural constraints on the encoding we show that the ``Only knowing'' logic can accommodate ordered default theories implementing a prescriptive interpretation of preference. Moreover, the encoding provides a transparent formal rendition of the semantics of prescriptive ordered defaults. A consequence of the construction is that the generation of extensions can be carried out entirely at the object level within the ``Only knowing'' logic. |
| Bert Van Nuffelen, Ofer Arieli, Alvaro Cortes-Calabuig and Maurice Bruynooghe. An ID-Logic Formalization of the Composition of Autonomous Databases |
| Abstract: We introduce a declarative approach for a coherent composition of autonomous databases. For this we use ID-logic, a formalism that extends classical logic with inductive definitions. We consider ID-logic theories that express, at the same time, the two basic challenges in database composition problems: relating different schemas of the local databases to one global schema (schema integration) and amalgamating the distributed and possibly contradictory data to one consistent database (data integration). We show that our framework supports different methods for schema integration(as well as their combinations) and that it provides a straightforward way of dealing with inconsistent data. Moreover,in this context database repair and consistent query answering are easily implemented by a variety of reasoning systems. |
| Hai-Feng Guo. Mode-Directed Fixed Point Computation |
| Abstract: Goal-directed fixed point computation strategies have been widely adopted in the tabled logic programming paradigm. However, there are many situations in which a fixed point contains a large number or even infinite number of solutions. In these cases, a fixed point computation engine may not be efficient enough or feasible at all. We present a mode-declaration scheme which provides the capabilities to reduce a fixed point from a big solution set to a preferred small one, or from an infeasible infinite set to a finite one. We show the correctness of the mode-declaration scheme. One motivating application of our mode-declaration scheme is for dynamic programming, which is typically used for solving optimization problems. There is no need to define the value of an optimal solution recursively, instead, defining a general solution suffices. The optimal value as well as its corresponding concrete solution can be derived implicitly and automatically using a mode-directed fixed point computation engine. This mode-directed fixed point computation engine has been successfully implemented in a commercial Prolog system. |
| Stijn Heymans, Davy Van Nieuwenborgh and Dirk Vermeir. Guarded Open Answer Set Programming |
Abstract: Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed point logic (FPL) extension of Clark's completion such that open answer sets correspond to models of FPL formulas and identify a syntactic subclass of programs, called (loosely) guarded programs. Whereas reasoning with general programs in OASP is undecidable, the FPL translation of (loosely) guarded programs falls in the decidable (loosely) guarded fixed point logic (mu-(L)GF).
Moreover, we reduce normal closed ASP to loosely guarded OASP, enabling a characterization of an answer set semantics by mu-LGF formulas. Finally, we relate guarded OASP to Datalog LITE, thus linking an answer set semantics to a semantics based on fixed point models of extended stratified Datalog programs. From this correspondence, we deduce 2-EXPTIME-completeness of satisfiability checking w.r.t. (loosely) guarded programs. |
| Carlos Iván Chesńevar, Guillermo Ricardo Simari and Lluis Godo. Computing Dialectical Trees Efficiently in Possibilistic Defeasible Logic Programming |
| Abstract: Possibilistic Defeasible Logic Programming (P-Delp) is a logic programming language which combines features from argumentation theory and logic programming, incorporating as well the treatment of possibilistic uncertainty and fuzzy knowledge at object-language level. As in many argumentation frameworks based in logic programming, solving a P-Delp query Q accounts for performing an exhaustive analysis of arguments and defeaters for Q, resulting in a so-called dialectical tree, usually computed in a depth-first fashion. Computing dialectical trees efficiently in P-Delp is an important issue, as some dialectical trees may be computationally more expensive than others which lead to equivalent results. In this paper we explore different aspects concerning how to speed up dialectical inference in P-Delp. We introduce definitions which allow to characterize dialectical trees constructively rather than declaratively, identifying relevant features for pruning the associated search space. The resulting approach can be easily generalized to be applied in other argumentation frameworks based in logic programming. |
| Kewen Wang and Yan Zhang. Nested Epistemic Logic Programs |
| Abstract: Nested logic programs and epistemic logic programs are two important extensions of answer set programming. However, the relationship between these two formalisms is rarely explored. In this paper we first introduce the epistemic HT-logic, and then propose a more general extension of logic programs called nested epistemic logic programs. The semantics of this extension - named equilibrium views - is defined on the basis of the epistemic HT-logic. We prove that equilibrium view semantics extends both the answer sets of nested logic programs and the world views of epistemic logic programs. Therefore, our work establishes a unifying framework for both nested logic programs and epistemic logic programs. Furthermore, we also provide a characterization of the strong equivalence of two nested epistemic logic programs. |
