09:00 | Torsten Schaub ASP Solving and Other Computing Paradigms Answer Set Programming (ASP) is on the verge of leaving the academic ivory tower and becoming an interesting alternative to established declarative solving paradigms in many application areas. This is due to its appealing combination of a highly expressive yet simple modeling language with high performance solving technology. Nonetheless certain applications require extensions or even an integration with other computing paradigms in order to be successfully solved. We discuss some of these extensions to ASP and elaborate upon the resulting systems available from potassco.sourceforge.net. |

10:30 | Christian Drescher, Oana Tifrea and Toby Walsh Symmetry-breaking Answer Set Solving In the context of Answer Set Programming, this paper investigates symmetry-breaking to eliminate symmetric parts of the search space and, thereby, simplify the solution process. We propose a reduction of disjunctive logic programs to a coloured digraph such that permutational symmetries can be constructed from graph automorphisms. Symmetries are then broken by introducing symmetry-breaking constraints. For this purpose, we formulate a preprocessor that integrates a graph automorphism system. Experiments demonstrate its computational impact. |

11:00 | Marcello Balduccini Improving DPLL Solver Performance with Domain-Specific Heuristics: the ASP Case In spite of the recent improvements in the performance of the solvers based on the DPLL procedure, it is still possible for the search algorithm to focus on the wrong areas of the search space, preventing the solver from returning a solution in an acceptable amount of time. This prospect is a real concern e.g. in an industrial setting, where users typically expect consistent performance. To overcome this problem, we propose a framework that allows learning and using domain-specific heuristics in solvers based on the DPLL procedure. The learning is done off-line, on representative instances from the target domain, and the learned heuristics are then used for choice-point selection. In this paper we focus on Answer Set Programming (ASP) solvers. In our experiments, the introduction of domain-specific heuristics improved performance on hard instances by up to 3 orders of magnitude (and 2 on average), nearly completely eliminating the cases in which the solver had to be terminated because the wait for an answer had become unacceptable. |

11:30 | Martin Gebser, Orkunt Sabuncu and Torsten Schaub An Incremental Answer Set Programming Based System for Finite Model Computation: Preliminary Report We address the problem of Finite Model Computation (FMC) of ﬁrst- order theories and show that FMC can efﬁciently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a ﬁnite model of the original ﬁrst-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE’s Automated Theorem Proving (ATP) competition. |

12:00 | Mario Alviano and Wolfgang Faber Dynamic Magic Sets for Super-Consistent Answer Set Programs For many practical applications of ASP, for instance data integration or planning, query answering is important, and therefore query optimization techniques for ASP are of great interest. Magic Sets are one of these techniques, originally defined for Datalog queries (ASP without disjunction and negation). Dynamic Magic Sets (DMS) are an extension of this technique, which has been proved to be sound and complete for query answering over ASP programs with stratified negation. A distinguishing feature of DMS is that the optimization can be exploited also during the nondeterministic phase of ASP engines. In particular, after some assumptions have been made during the computation, parts of the program may become irrelevant to a query under these assumptions. This allows for dynamic pruning of the search space, which may result in exponential performance gains. In this paper, the correctness of DMS is formally established and proved for brave and cautious reasoning over the class of super-consistent ASP programs (ASP^SC programs). ASP^SC programs guarantee consistency (i.e., have answer sets) when an arbitrary set of facts is added to them. This result generalizes the applicability of DMS, since the class of ASP^SC programs is richer than ASP programs with stratified negation, and in particular includes all odd-cycle-free programs. DMS has been implemented as an extension of DLV, and the effectiveness of DMS for ASP^SC programs is empirically confirmed by experimental results with this system. |

14:00 | Dov Gabbay, David Pearce and Agustin Valverde Interpolation in Equilibrium Logic and Answer Set Programming: the Propositional Case Interpolation is an important property of classical and many non classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the propositional version of the non-monotonic system of {\em equilibrium logic}, establishing weaker or stronger forms of interpolation depending on the precise interpretation of the inference relation. These results also yield a form of interpolation for ground logic programs under the answer sets semantics. For disjunctive logic programs we also study the property of uniform interpolation that is closely related to the concept of variable forgetting. |

14:30 | Pedro Cabalar A Logical Characterisation of Ordered Disjunction In this paper we consider a logical treatment for the ordered disjunction operator 'x' introduced by Brewka, Niemelä and Syrjänen in their Logic Programs with Ordered Disjunctions (LPOD). LPODs are used to represent preferences in logic programming under the answer set semantics. Their semantics is defined by first translating the LPOD into a set of normal programs (called split programs) and then imposing a preference relation among the answer sets of these split programs. We concentrate on the first step and show how a suitable translation of the ordered disjunction as a derived operator into the logic of Here-and-There allows capturing the answer sets of the split programs in a direct way. We use this characterisation not only for providing an alternative implementation for LPODs, but also for checking several properties (under strongly equivalent transformations) of the x operator, like for instance, its distributivity with respect to conjunction or regular disjunction. We also make a comparison to an extension proposed by Kärger, Lopes, Olmedilla and Polleres, that combines x with regular disjunction. |

15:30 | Stefania Costantini and Alessio Paolucci Towards Translating Natural Language Sentences into ASP We build upon recent work by Baral, Dzifcal and Son that define the translation into ASP of (some classes of) natural language sentences from the lambda-calculus intermediate format generated by CCG grammars. We introduce automatic generation of lambda-calculus expressions from template ones, thus improving the effectiveness and generality of the translation process. The enhanced representation adopts meta-level templates and is able on the one hand to represents in a single expression sets of sentences instead of single sentences and on the other hand to better express uncertain knowledge. |

16:00 | Cristina Feier and Stijn Heymans An Optimization for Reasoning with Forest Logic Programs Open Answer Set Programming (OASP) is an attractive framework for integrating ontologies and rules. In general OASP is undecidable. Recently we provided a sound, complete, and terminating tableau-based algorithm for satisfiability checking w.r.t. forest logic programs, a decidable fragment of OASP, which has the forest model property. In this paper we introduce an optimized version of that algorithm achieved by means of a knowledge pre-compiling technique. So-called unit completion structures, which are possible building blocks of a forest model, in the form of trees of depth 1, are computed in an initial step of the algorithm. Repeated computations are avoided by using these structures in a pattern-matching style when constructing a model. Furthermore we identify and discard redundant unit completion structures, where a structure is redundant if there is another structure which can always replace the original structure in a forest model. |

16:30 | Yves Moinard Using ASP with Recent Extensions for Causal Explanations We examine how recent developments in ASP formalisms facilitate the translation of a causal explanation formalism. Preceding translations in ASP were complicated by some limitations of ASP formalisms, such as the poor data structure and the difficulty in reusing parts of programs in several places of a larger system. Our formalism aims at capturing causal explanations from causal and ontological information. We provide a real implementation in terms of ASP, showing the naturalness and relative efficiency of this translation job. We identify two crucial improvements which could be made in future ASP systems in order to help ASP dealing with this kind of problem. |