IJCAR 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: Proofs (10:30‑12:30)
Chair: Dieter Hutter
Location: Metropolitan B

10:30‑11:00	Tobias Nipkow (TU Muenchen) Gertrud Bauer (TUM) Flyspeck I: Tame Graphs We present a verified enumeration of tame graphs as defined in Hales' proof of the Kepler Conjecture and confirm the completeness of Hales' list of all tame graphs while reducing it from 5128 to 2771 graphs.
11:00‑11:30	Volker Sorge (University of Birmingham) Andreas Meier (DFKI) Roy McCasland (University of Edinburgh) Simon Colton (Imperial College London) The Automatic Construction of Isotopy Invariants The automatic construction of mathematical theorems is a challenging task for automated reasoning systems, which has the potential to greatly add to mathematical research areas, particularly with respect to classification tasks. We have developed a bootstrapping algorithm for the construction of classification theorems in finite algebraic domains. While it is largely generic, its power relies upon the automatic discovery of algebraic invariants which are able to discriminate between members of different classes defined by the equivalence relation under consideration. When considering isomorphism equivalences, we were able to employ machine learning techniques to generate the invariants, and this led to novel theorems which achieve classifications up to isomorphism of quasigroups and loops of small order. In our current work, we have applied the bootstrapping algorithm to produce classification theorems up to \emph{isotopism}, an equivalence relation which is of greater importance in certain domains, in particular algebraic loop theory. Unfortunately, the machine learning approach did not suffice for this application, as finding isotopy invariants is a much more complex task. We describe here new methods for generating isotopy invariants. Firstly, by drawing on details of isotopy invariants from the literature, we describe how we can obtain invariants using an intricate interplay of model generation and theorem proving. We also present a new set of invariants which are derived from systematically examining substructures of loops. These are constructed using symbolic computation techniques. In addition to describing how the invariants are constructed, we elaborate on techniques to verify the constructed isotopy classification theorems. These methods involve simplifying the proof problems with computer algebra, before providing proof via a satisfiability solver. We demonstrate the effectiveness of this approach by generating novel isotopy classification theorems, which have so far been beyond the reach of automated reasoning systems.
11:30‑12:00	Sylvie Boldo (INRIA) Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms Some floating-point algorithms have been used for decades and proved decades ago in radix-2 and providing neither Underflow, nor Overflow occurs. This includes Veltkamp algorithm, used to split a float into an upper part and a lower part and Dekker algorithm, used to compute the exact error of a floating-point multiplication. The aim of this article is to show the difficulties of a strong justification of the validity of these algorithms for a generic radix radix and even when Underflow or Overflow occurs. These cases are usually dismissed even if they should not: the main argument in radix 2 of the first algorithm fails in other radices. Nevertheless here, all results still hold under mild assumptions. The proof path is interesting as these cases are hardly looked into and new methods and results had to be developed.
12:00‑12:30	Geoff Sutcliffe (University of Miami) Stephan Schulz (Technical University of Munich) Koen Claessen (Chalmers Technical University) Allen Van Gelder (University of California, Santa Cruz) Using the TPTP Language for Writing Derivations and Finite Interpretations One of the keys to the success of the TPTP and related projects is their consistent use of the TPTP language. The ability of the TPTP language to express solutions as well as problems, in conjunction with the simplicity of the syntax, sets it apart from other languages used in ATP. This paper provides a complete definition of the TPTP language, and describes how the language should be used to write derivations and finite interpretations.

Lunch break (12:30‑14:00)

Session 2: Search (14:00‑16:00)
Chair: Deepak Kapur
Location: Metropolitan B

14:00‑14:30	Jordi Levy (IIIA - CSIC) Manfred Schmidt-Schauss (Institut für Informatik, FB Informatik und Mathematik, Johann Wolfgang Goethe-Universität) Mateu Villaret (Informàtica i Matemàtica Aplicada - Universitat de Girona) Stratified Context Unification is NP-complete Context Unification is the problem to decide for a given set of second-order equations $E$ where all second-order variables are unary, whether there exists a unifier, such that for every second-order variable $X$, the abstraction $\lambda x. r$ instantiated for $X$ has exactly one occurrence of the bound variable $x$ in $r$. Stratified Context Unification is a specialization where the nesting of second-order variables in $E$ is restricted. It is already known that Stratified Context Unification is decidable, NP-hard, and in PSPACE, whereas the decidability and the complexity of Context Unification is unknown. We prove that Stratified Context Unification is in \mbox{NP} by proving that a size-minimal solution can be represented in a singleton tree grammar of polynomial size, and then applying a generalization of Plandowski's polynomial algorithm that compares compacted terms in polynomial time. This also demonstrates the high potential of singleton tree grammars for optimizing programs maintaining large terms. A corollary of our result is that solvability of one-step rewrite constraints is NP-complete.
14:30‑15:00	Kaustuv Chaudhuri (Carnegie Mellon University) Frank Pfenning (Carnegie Mellon University) Greg Price (Carnegie Mellon University) A logical characterization of forward and backward chaining in the inverse method The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli's focusing strategy can be adapted for the inverse method in linear logic. In this paper we introduce the notion of focusing bias for atoms and show that it gives rise to forward and backward chaining, generalizing both hyperresolution (forward) and SLD resolution (backward) on the Horn fragment. A key feature of our characterization is the structural,rather than purely operational, explanation for forward and backward chaining. A search procedure like the inverse method is thus able to perform both operations as appropriate, even simultaneously. We also present experimental results and an evaluation of the practical benefits of biased atoms for a number of examples from different problem domains.
15:00‑15:30	Andrei Paskevich (Université Paris-12 "Val de Marne") Connection Tableaux with Lazy Paramodulation It is well-known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tableau calculus for logic with equality. This calculus is based on a lazy form of paramodulation where parts of the unification step become auxiliary subgoals in a tableau and may be subjected to subsequent paramodulations. Our calculus uses ordering constraints and a certain form of the basicness restriction.
15:30‑16:00	Peter Baumgartner (National ICT Australia (NICTA)) Renate Schmidt (The University of Manchester) Blocking and Other Enhancements for Bottom-Up Model Generation Methods In this paper we introduce several new improvements to the bottom-up model generation (BUMG) paradigm. Our techniques are based on non-trivial transformations of first-order problems into a certain implicational form, namely range-restricted clauses. These refine existing transformations to range-restricted form by extending the domain of interpretation with new Skolem terms in a more careful and deliberate way. Our transformations also extend BUMG with a blocking technique for detecting recurrence in models. Blocking is based on a conceptually rather simple encoding together with standard equality theorem proving and redundancy elimination techniques. This provides a general-purpose method for finding small models. The presented techniques are implemented and have been successfully tested with existing theorem provers on the satisfiable problems from the TPTP library.

Break (16:00‑16:30)

Invited Talk (16:30‑17:30)
Chair: John Harrison
Location: Metropolitan B

16:30‑17:30

Bruno Buchberger (Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria) Mathematical Theory Exploration [pdf] Despite the significant advances automated reasoning has seen over the past decades, the impact of automated reasoning on the practice of doing mathematics is small. In this talk we present our view on how the practical process of mathematical theory exploration could and should be supported by reasoning systems. We describe this process as a sequence of proving, solving, and simplifying steps. Consideration will also be given to the computer-support of mathematical invention. We propose formulae schemes as a general bottom-up tool and the analysis of failing proofs as a general top- down tool for mathematical invention. We will also discuss the importance of proving reasoners correct. As a running example, we take the algorithmic algebraic theory of Groebner bases that has found numerous applications in many different areas of mathematics (algebraic geometry, symbolic analysis, algebraic combinatorics etc.). We will show how, by a new algorithm synthesis technique, the main algorithm of Groebner bases theory can be derived from its specification completely automatically.