ICLP on Thursday, August 17th

FLoC Second Opening and Plenary Session (08:45‑10:00)
Chair: Moshe Vardi, Thomas Ball, Wolfram Schulte, Ken McMillan
Location: Metropolitan A/B

08:45‑09:00

Introduction and Welcome

09:00‑10:00

David Dill (Stanford University) I Think I Voted: E-voting vs. Democracy [ppt] Touch-screen voting machines store records of cast votes in internal memory, where the voter cannot check them. Because of our system of secret ballots, once the voter leaves the polls there is no way anyone can determine whether the vote captured was what the voter intended. Why should voters trust these machines? In January 2003, I drafted a "Resolution on Electronic Voting" stating that every voting system should have a "voter verifiable audit trail," which is a permanent record of the vote that can be checked for accuracy by the voter, and which is saved for a recount if it is required. I posted the page with endorsements from many prominent computer scientists. At that point, I became embroiled in a nationwide battle for voting transparency that has continued now for three years. In this talk, I'll explain the basic problems and solutions in electronic voting.

Break (10:00‑10:30)

Session 1: Theory (10:30‑12:30)
Chair: Brigitte Pientka
Location: Cirrus

10:30‑11:00	Martin Gebser (University of Potsdam) Torsten Schaub (University of Potsdam) Tableau Calculi for Answer Set Programming We introduce a family of calculi for Answer Set Programming (ASP) based on tableaux methods. Our approach furnishes declarative and fine-grained instrumentalities for characterizing operations as well as strategies of ASP-solvers. First, the granulation is detailed enough to capture the variety of propagation and choice operations in algorithms used for ASP; this also includes SAT-based approaches. Second, it is general enough to encompass the various strategies pursued by existing ASP-solvers, like assat, cmodels, dlv, nomore++, smodels, etc. This provides us with a uniform framework for comparing existing solvers. Third, the approach is flexible enough to integrate new inference patterns, so to study their relation to existing ones. As a result, we obtain a new approach to computing unfounded sets by means of loops. Furthermore, it allows us to define a backward inference for unfounded set computation that appears to be the first of its kind. Finally, our approach allows us to investigate the proof complexity of ASP-solvers, depending on choice operations. In particular, we show that exponentially different best-case computations can be obtained for different ASP-solvers.
11:00‑11:30	Luciano Caroprese (University of Calabria) Sergio Greco (University of Calabria) Cristina Sirangelo (University of Calabria) Ester Zumpano (University of calabria) Declarative Semantics of Production Rules for Integrity Maintenance The paper presents a declarative semantics for the maintenance of integrity constraints expressed by means of production rules. Here a production rule is a special form of active rule, called active integrity constraint, whose body contain an integrity constraint (conjunction of literals which must be false) and the head contains a disjunction of update atoms, i.e. actions to be performed if the corresponding constraints is not satisfied (i.e. is true). The paper introduces i) a formal declarative semantics allowing to compute founded repairs, that is repairs whose actions are specified and supported by active integrity constrains, ii) an equivalent semantics obtained by rewriting production rules into disjunctive logic rules, so that repairs can be derived from the answer sets of the logic program, iii) a characterization of production rules allowing a methodology for the definition of production rules for integrity maintenance for integrity maintenance.
11:30‑12:00	Remy Haemmerle (INRIA) Francois Fages (INRIA) Modules for Prolog Revisited Module systems are an essential feature of programming languages as they facilitate the re-use of existing code and the development of general purpose libraries. Unfortunately, there has been no consensual module system for Prolog, hence no strong development of libraries, in sharp contrast to what exists in Java for instance. One difficulty comes from the call predicate which interferes with the protection of the code, an essential task of a module system. By distinguishing the called module code protection from the calling module code protection, we review the existing syntactic module systems for Prolog. We show that no module system ensures both forms of code protection, with the noticeable exceptions of Ciao-Prolog and XSB. We then present a formal module system for logic programs with calls and closures, define its operational semantics and formally prove the code protection property. Interestingly, we also provide an equivalent logical semantics of modular logic programs without calls nor closures, which shows how they can be translated into constraint logic programs over a simple module constraint system.
12:00‑12:30	Diptikalyan Saha (Stony Brook University) C.R. Ramakrishnan (SUNY, Stony Brook) A Local Algorithm for Incremental Evaluation of Tabled Logic Programs This paper considers the problem of efficient incremental maintenance of memo tables in a tabled logic programming system when the underlying data are changed. Most existing techniques for incremental evaluation (or materialized view maintenance in deductive databases) consider insertion and deletion of facts as primitive changes, and treat update as deletion of the old version followed by insertion of the new version. They handle insertion and deletion using independent algorithms, consequently performing many redundant computations when processing updates. In this paper, we present a local algorithm for handling updates to facts. We maintain a dynamic (and potentially cyclic) dependency graph between and among calls and answers in the memo tables. The key idea is to interleave the propagation of deletion and insertion operations generated by the updates through this graph. The dependency graph used in our algorithm is more general than that used in algorithms previously proposed for incremental evaluation of attribute grammars and functional programs. Nevertheless, our algorithm's complexity matches that of the most efficient algorithms built for these specialized cases. We demonstrate the effectiveness of our algorithm using data-flow analysis and parsing examples.

Lunch break (12:30‑14:00)

Session 2: Functional and Constraint Logic Programming (14:00‑16:00)
Chair: Maurizio Proietti
Location: Cirrus

14:00‑14:30	Jon Sneyers (K.U.Leuven) Tom Schrijvers (K.U.Leuven) Bart Demoen (K.U.Leuven) Memory reuse for CHR Two Constraint Handling Rules compiler optimizations that drastically reduce the memory footprint of CHR programs are introduced. The reduction is the result of reusing suspension terms, the internal CHR constraint representation, and avoiding the overhead of constraint removal followed by insertion. The optimizations are defined formally and their correctness is proved. Both optimizations were implemented in the K.U.Leuven CHR system. Significant memory savings and speedups were measured on realistic benchmarks.
14:30‑15:00	Sergio Antoy (Portland State University) Michael Hanus (Christian-Albrechts-Universität zu Kiel) Overlapping Rules and Logic Variables in Functional Logic Programs Functional logic languages extend purely functional languages with two features: operations defined by overlapping rules and logic variables in both defining rules and expressions to evaluate. In this paper, we show that only one of these features is sufficient in a core language. On the one hand, overlapping rules can be eliminated by introducing logic variables in rules. On the other hand, logic variables can be eliminated by introducing operations defined by overlapping rules. The proposed transformations between different classes of programs not only give a better understanding of the features of functional logic programs but also may simplify implementations of functional logic languages.
15:00‑15:30	Sebastian Brand (National ICT Australia) Roland H.C. Yap (National University of Singapore) Towards "Propagation = Logic + Control" Constraint propagation algorithms implement logical inference. For efficiency, it is essential to control whether and in what order basic inference steps take place. We provide a high-level framework that clearly differentiates between information needed for controlling propagation versus that needed for the logical semantics of complex constraints composed from primitive ones. We argue for the appropriateness of our controlled propagation framework by showing that it captures the underlying principles of manually designed propagation algorithms, such as literal watching for unit clause propagation and the lexicographic ordering constraint. We provide an implementation and benchmark results that demonstrate the practicality and efficiency of our framework.
15:30‑16:00	Gregory James Duck (NICTA) Sebastian Brand (NICTA) Peter Stuckey (Melbourne University) ACD Term Rewriting In this paper we introduce Associative Commutative Distributive (ACD) term rewriting, a rewriting language for rewriting logical formulae. ACD term rewriting extends AC term rewriting by adding distribution of conjunction over other operators. Conjunction is vital for expressive term rewriting systems since it allows us to require that multiple conditions hold for a term rewriting rule to be used. ACD term rewriting uses the notion of a "conjunctive context", which is the conjunction of constraints that must hold in the context of a term, to enable the programmer to write very expressive and targeted rewriting rules. ACD term rewriting can be seen as a general logical programming language that extends Constraint Handling Rules and AC term rewriting. In this paper we define the semantics of ACD term rewriting and describe our prototype implementation.

Break (16:00‑16:30)

Prolog Contest (16:30‑19:00)
Location: Cirrus