ICLP on Saturday, July 17th

09:00‑10:00 ICLP Invited talk
Chair: Torsten Schaub
Location: AT LT3
09:00 Francois Fages (INRIA Paris-Rocquencourt)
A Logical Paradigm for Systems Biology
10:30‑12:30 Answer Set Programming
Chair: Stefan Woltran
Location: AT LT3
10:30 Christian Drescher and Toby Walsh
A Translational Approach to Constraint Answer Set Solving

We present a new approach to enhancing Answer Set Programming (ASP) with Constraint Processing techniques which allows for solving interesting Constraint Satisfaction Problems in ASP. We show how constraints on finite domains can be decomposed into logic programs such that unit-propagation achieves arc, bound or range consistency. Experiments with our encodings demonstrate their computational impact.

11:00 Sabrina Baselice and Piero Bonatti
Decidable subclasses of finitary programs

Finitary programs are a general class of normal logic programs with function symbols whose stable model semantics is decidable under mild conditions. The class of finitary programs, however, is undecidable; this limitation has triggered several research efforts aimed at characterizing other restricted classes of normal programs with good computational properties. In this paper we introduce some new decidable subclasses of finitary programs whose stable model semantics is decidable. Unlike most previous approaches, these subclasses preserve much of the expressive power of unrestricted finitary programs, including the ability of defining infinite and infinitely many stable models.

11:30 Mario Alviano, Wolfgang Faber and Nicola Leone,
Disjunctive ASP with Functions: Decidable Queries and Effective Computation

Querying over disjunctive ASP with functions is a highly undecidable task in general. In this paper we focus on disjunctive logic programs with stratified negation and functions under the stable model semantics (ASP^{fs}). We show that query answering in this setting is decidable, if the query is finitely recursive (ASP^{fs}_{fr}). Our proof yields also an effective method for query evaluation. It is done by extending the magic set technique to ASP^{fs}_{fr}. We show that the magic-set rewritten program is query equivalent to the original one (under both brave and cautious reasoning). Moreover, we prove that the rewritten program is also finitely ground, implying that it is decidable. Importantly, finitely ground programs are evaluable using existing ASP solvers, making the class of ASP^{fs}_{fr} queries usable in practice.

12:00 Johannes Oetsch, Joerg Puehrer and Hans Tompits
Catching the Ouroboros: On Debugging Non-ground Answer-Set Programs

An important issue towards a broader acceptance of answer-set programming (ASP) is the deployment of tools which support the programmer during the coding phase. In particular, methods for debugging an answer-set program are recognised as a crucial step in this regard. Initial work on debugging in ASP mainly focused on propositional programs, yet practical debuggers need to handle programs with variables as well. In this paper, we discuss a debugging technique that is directly geared towards non-ground programs. Following previous work, we address the central debugging question why some interpretation is not an answer set. The explanations provided by our method are computed by means of a meta-programming technique, using a uniform encoding of a debugging request in terms of ASP itself. Our method also permits programs containing comparison predicates and integer arithmetics, thus covering a relevant core language commonly supported by all state-of-the-art ASP solvers.

14:00‑15:00 Technical Communications - II
Chair: John Gallagher
Location: AT LT3
14:00 Selen Basol, Ozan Erdem, Michael Fink and Giovambattista Ianni
HEX Programs with Action Atoms

HEX programs were originally introduced as a general framework for extending declarative logic programming, under the stable model semantics, with the possibility of bidirectionally accessing external sources of knowledge and/or computation. The original framework, however, does not deal satisfactorily with stateful external environments: the possibility of predictably influencing external environments has thus not yet been considered explicitly. This paper lifts HEX programs to ACTHEX programs: ACTHEX programs introduce the notion of action atoms, which are associated to corresponding functions capable of actually changing the state of external environments. The execution of specific sequences of action atoms can be declaratively programmed. Furthermore, ACTHEX programs allow for selecting preferred actions, building on weights and corresponding cost functions. We introduce syntax and semantics of ACTHEX programs; ACTHEX programs can successfully be exploited as a general purpose language for the declarative implementation of executable specifications, which we illustrate by encodings of knowledge bases updates, action languages, and an agent programming language. A system capable of executing ACTHEX programs has been implemented and is publicly available.

14:12 Christoph Wernhard
Circumscription and Projection as Primitives of Logic Programming

We pursue a representation of logic programs as classical first-order sentences. Different semantics for logic programs can then be expressed by the way in which they are wrapped into -- semantically defined -- operators for circumscription and projection. (Projection is a generalization of second-order quantification.) We demonstrate this for the stable model semantics, Clark's completion and a three-valued semantics based on the Fitting operator. To represent the latter, we utilize the polarity sensitiveness of projection, in contrast to second-order quantification, and a variant of circumscription that allows to express predicate minimization in parallel with maximization. In accord with the aim of an integrated view on different logic-based representation techniques, the material is worked out on the basis of first-order logic with a Herbrand semantics.

14:24 Luis Moniz Pereira and Alexandre Miguel Pinto
Tight Semantics for Logic Programs

We define the Tight Semantics (TS), a new semantics for all NLPs complying with the requirements of: 2-valued semantics; preserving the models of SM; guarantee of model existence (even in face of odd loops over negation or infinite chains); relevance; cumulativity; and compliance with the Well-Founded Model. We also extend TS to adumbrate ELPs and Disjunctive LPs, though a full account of these is left to other papers. When complete models are unnecessary, and top-down querying (à la Prolog) is desired, TS provides the 2-valued option that guarantees model existence, as a result of its relevance property. Top-down querying with abduction by need is rendered available too by TS. The user need not pay the price of computing whole models, nor of generation all possible abductions, only to filter irrelevant ones subsequently. In a nutshell, a TS model of a NLP P is any minimal model M of P that further satisfies ^P - the program remainder of P - in that each loop in ^P has a minimal model contained in M, whilst respecting the constraints imposed by the minimal models of the other loops so-constrained too. The applications afforded by TS are all those of Stable Models, which it generalizes, plus those permitting to solve OLONs for model existence, plus those employing OLONs for productively obtaining problem solutions, not just filtering them (like ICs).

14:36 Joseph Near
From Relational Specifications to Logic Programs

We present a compiler from expressive, relational specifications to logic programs. Specifically, our tool compiles the Imperative Alloy specification language to Prolog. Imperative Alloy is a declarative, relational specification language based on first-order logic and extended with imperative constructs; Alloy specifications are traditionally not executable. In spite of this theoretical limitation, our compiler produces efficient Prolog programs for many specifications; when better performance is required, an automatically-verified refinement step may be performed on the original specification to help the compiler produce faster code.

14:48 Stefan Brass
Implementation Alternatives for Bottom-Up Evaluation

Bottom-up evaluation is a central part of query evaluation / program execution in deductive databases. It is used after a source code optimization like magic sets or SLDmagic that ensures that only facts relevant for the query can be derived. Then bottom-up evaluation simply performs the iteration of the standard T_P-operator to compute the minimal model. However, there are different ways to implement bottom-up evaluation efficiently. Since this is most critical for the performance of a deductive database system, and since performance is critical for the acceptance of deductive database technology, this question deserves a thorough analysis. In this paper we start this work by discussing several different implementation alternatives. Especially, we propose a new implementation of bottom-up evaluation called ``Push-Method''. First runtime comparisons are given.

15:30‑16:30 ALP community meeting
Chair: Gopal Gupta
Location: AT LT3