IJCAR on Saturday, August 19th

Herbrand Award: Wolfgang Bibel (08:45‑09:30)
Chair: Franz Baader
Location: Grand Ballroom B

Session 6: System Description 2 (09:30‑10:30)
Chair: Bernhard Beckert
Location: Grand Ballroom B

09:30‑09:45	Juergen Giesl (RWTH Aachen) Peter Schneider-Kamp (RWTH Aachen) Rene Thiemann (RWTH Aachen) AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework AProVE 1.2 is one of the most powerful systems for automated termination proofs of term rewrite systems (TRSs). It is the first tool which automates the new dependency pair framework and therefore permits a completely flexible combination of different termination proof techniques. Due to this framework, AProVE 1.2 is also the first termination prover which can be fully configured by the user.
09:45‑10:00	Boontawee Suntisrivaraporn (Dresden University of Technology) Franz Baader (TU Dresden) Carsten Lutz (Institute for Theoretical Computer Science, TU Dresden) CEL---A Practical Reasoner for Life Science Ontologies CEL (Classifier for EL) is a reasoner for the small description logic EL+, supporting as its main reasoning task the computation of the subsumption hierarchy induced by EL+ ontologies. The most distinguishing feature of CEL is that, unlike other modern DL reasoners, it is based on a polynomial-time subsumption algorithm, which allows it to process very large ontologies in reasonable time. In spite of its restricted expressive power, EL+ is well-suited for formulating life science ontologies.
10:00‑10:15	Dmitry Tsarkov (The University of Manchester) Ian Horrocks (The University of Manchester) FaCT++ Description Logic Reasoner: System Description This is a system description of the Description Logic reasoner FaCT++. The reasoner implements a tableaux decision procedure for the well known SHOIQ description logic, with additional support for datatypes, including strings and integers. The system employs a wide range of performance enhancing optimisations, including both standard techniques (such as absorption and model merging) and newly developed ones (such as ordering heuristics and taxonomic classification). FaCT++ can, via the standard DIG interface, be used to provide reasoning services for ontology engineering tools supporting the OWL DL ontology language.
10:15‑10:30	Steven Obua (Technische Universität München) Sebastian Skalberg (OneSpin Solutions GmbH) Importing HOL into Isabelle/HOL We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Isabelle/HOL that have been recorded in HOL 4 or HOL-light and is therefore completely safe. Concepts in the source HOL system, that is types and constants, can be mapped to concepts in Isabelle/HOL; this facilitates a true integration of imported theorems and theorems that are already available in Isabelle/HOL. The importer is part of the standard Isabelle distribution.

Break (10:30‑11:00)

Session 7: Search (11:00‑12:30)
Chair: Chris Lynch
Location: Willow A

11:00‑11:30	Hans de Nivelle (Max-Planck Institut fuer Informatik) Jia Meng (National ICT of Australia) Geometric Resolution: A Proof Procedure Based on Finite Model Search We present a proof search procedure which is complete for first-order logic, but which also can be used when searching for finite models. The procedure uses a normal form that is closely related to geometric formulas. For this reason, we call the procedure geometric resolution. We expect that the procedure can be used as an efficient proof search procedure for first-order logic. We will point out how the procedure can be implemented in such a way that it is complete for finite models without loosing completeness for unsatisfiability. We will also discuss two refinements of the initial procedure, namely subsumption and functional reduction, and prove their completeness. Finally, we will discuss how the calculus can be implemented.
11:30‑12:00	Xiang Xue Jia (Institute of Software,Chinese Academy of Sciences) Jian Zhang (Institute of Software, Chinese Academy of Sciences) A Powerful Technique to Eliminate Isomorphism in Finite Model Search This paper proposes a general-purpose technique, DASH (stands for decision assignment scheme heuristic), to eliminate isomorphic subspaces during generating finite models. Like LNH, DASH is based on inherent isomorphism in first order clauses on finite domain. Unlike other methods, DASH can completely eliminate isomorphism during search. Therefore, we can generate all the models in which there aren't any two isomorphic models. One key issue here is to cut the branch of searching tree which is isomorphic to the branch that has been searched. We implement this technique by modifying SEM1.7B, and we call the new tool SEMD. This technique proves to be very efficient on many problems (like generate finite group, ring, field and so on).The experiments show that SEMD is 10 or more times faster than SEM on many problems, especially when we generate all the models and when there is no model. A biggest advantage is that SEMD can generate all the non-isomorphic models with little extra cost, while the other tools like MACE4 can't do this in an acceptable time. In the implementation of DASH, we present a new method which is used to describe the class of isomorphic branches.
12:00‑12:30	Adam Koprowski (Eindhoven University of Technology) Hans Zantema (Technische Universiteit Eindhoven) Recursive Path Ordering for Infinite Labelled Rewrite Systems Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far in tools for automatic termination proving and variants with infinite sets of labels were believed not to be suitable for automation. We show that such automation can be achieved for semantic labelling with natural numbers, in combination with recursive path ordering (RPO). In order to do so we developed algorithms to deal with recursive path ordering for these infinite labelled systems. Using these techniques, our tool, TPA, is the only current tool that can prove termination of the SUBST system automatically.

Session 8: Proof Theory (11:00‑12:30)
Chair: Jason Hickey
Location: Grand Ballroom B

11:00‑11:30	Roy Dyckhoff (School of Computer Science, University of St Andrews) Delia Kesner (PPS, Université Paris 7) Stephane Lengrand (School of Computer Science, University of St Andrews, PPS, Université Paris 7) Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic Inspired by the Curry-Howard correspondence, we study normalisation procedures in the depth-bounded intuitionistic sequent calculus of Hudelmaier (1988) for the implicational case, thus strengthening existing approaches to Cut-admissibility. We decorate proofs with proof-terms and introduce various term-reduction systems representing proof transformations. In contrast to previous papers which gave different arguments for Cut-admissibility suggesting weakly normalising procedures for Cut-elimination, our main reduction system and all its variations are strongly normalising, with the variations corresponding to different optimisations, some of them with good properties such as confluence.
11:30‑12:00	Brigitte Pientka (McGill University) Eliminating redundancy in higher-order unification:a lightweight approach In this paper, we discuss a lightweight approach to eliminate the overhead due to implicit type arguments during higher-order unification of dependently-typed terms. First, we show that some implicit type information is uniquely determined, and can therefore be safely skipped during higher-order unification. Second, we discuss its impact in practice during type reconstruction and during proof search within the logical framework Twelf. Our experimental results show that implicit type arguments are numerous and large in size, but their impact on run-time is between 10\% and 20\%. On the other hand optimizations such as eliminating the occurs are shown to be crucial to achieve significant performance improvements.
12:00‑12:30	Florian Rabe (CMU) First-Order Logic with Dependent Types We present DFOL, an extension of classical first-order logic with dependent types, i.e., as in Martin-Lof type theory, signatures may contain type-valued function symbols. A model theory for the logic is given that stays close to the established first-order model theory. The logic is presented as an institution, and the logical framework LF is used to define signatures, terms and formulas. We show that free models over Horn theories exist, which allows its use as an algebraic specification language, and show that the classical first-order axiomatization is complete for DFOL, too, which implies that existing first-order theorem provers can be extended. In particular, the axiomatization can be encoded in LF.

Lunch (in hotel) (12:30‑14:00)
Location: Grand Ballroom D

Session 9: Proof Checking (14:00‑16:00)
Chair: John Harrison
Location: Willow A

14:00‑14:30	Dexter Kozen (Cornell University) Christoph Kreitz (Cornell University / University of Potsdam) Eva Richter (University of Potsdam) Automating Proofs in Category Theory We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of categories, functors and natural transformations as well as a small set of proof tactics that automate proof search in this calculus. We demonstrate our approach by automating the proof that the functor categories FunCxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic.
14:30‑15:00	Roland Zumkeller (Ecole Polytechnique) Formal Global Optimisation with Taylor Models Formal proofs and global optimisation are two research areas that have been heavily influenced by the arrival of computers. This article aims to bring both further together by formalising a global optimisation method, namely Taylor models: a set of functions is represented by a polynomial together with an error bound. The algorithms are implemented in the proof assistant Coq's term language, with the ultimate goal to obtain formally proven bounds for any multi-variate smooth function in an efficient way. To this end we make use of constructive real numbers, interval arithmetic, and polynomial bounding techniques.
15:00‑15:30	Benjamin Grégoire (INRIA) Laurent Théry (INRIA) A purely functional library for modular arithmetic and its application to certifying large prime numbers Computing efficiently with numbers can be crucial for some theorem proving applications. In this paper, we present a library of modular arithmetic that has been developed within the Coq proof assistant. The library proposes the usual operations that have all been proved correct. The library is purely functional but can also be used on top of some native modular arithmetic. With this library, we have been capable of certifying the primality of numbers with more than 13000 digits.
15:30‑16:00	Assia Mahboubi (INRIA Sophia Antipolis) Proving formally the implementation of an efficient gcd algorithm for polynomials We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correction of our implementation of the subresultants algorithm. Up to our knowledge it is the first mechanized proof of this result.

Session 10: Combination (14:00‑16:00)
Chair: Aaron Stump
Location: Grand Ballroom B

14:00‑14:30	Erik Reeber (University of Texas at Austin) Warren A. Hunt, Jr. (University of Texas at Austin) A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) We define the Subclass of Unrollable List Formulas in ACL2 (SULFA). SULFA is a subclass of ACL2 formulas based on list structures that is sufficiently expressive to include invariants of finite state machines (FSMs). We present an efficient method for recognizing these formulas within the ACL2 theorem prover. Furthermore, we present a SAT-based decision procedure for SULFA formulas. When this decision procedure is successful, a theorem is added to the ACL2 system database as a lemma for use in future proof attempts. When unsuccessful, a counter-example to the SULFA property is output. We are using SULFA and its SAT-based decision procedure as part of a larger system to verify components of the TRIPS processor. Our verification system translates Verilog designs automatically into ACL2 models. These models are written such that their invariants are SULFA properties, which can be verified by our SAT-based decision procedure, traditional theorem proving, or a mixture of both. We show how this technique is used to verify the implementation of a communication protocol used in the Load Store Queue (LSQ).
14:30‑15:00	Shuvendu Lahiri (Microsoft Research) Madanlal Musuvathi (Microsoft Research) Solving Sparse Linear Constraints Linear arithmetic decision procedures form an important part of theorem provers for program verification. In most verification benchmarks, the linear arithmetic constraints are dominated by simple difference constraints of the form x <= y + c. Sparse linear arithmetic (SLA) denotes a set of linear arithmetic constraints with a very few non-difference constraints. In this paper, we propose an efficient decision procedure for SLA constraints, by combining a solver for difference constraints with a solver for general linear constraints. For SLA constraints, the space and time complexity of the resulting algorithm is dominated solely by the complexity for solving the difference constraints. The decision procedure generates models for satisfiable formulas. We show how this combination can be extended to generate implied equalities. We instantiate this framework with an equality generating Simplex as the linear arithmetic solver, and present preliminary experimental evaluation of our implementation on a set of linear arithmetic benchmarks.
15:00‑15:30	Olga Grinchtein (Uppsala University) Martin Leucker (TU Munich) Nir Piterman (EPFL) Inferring Network Invariants Automatically Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is a system that abstracts the composition of every number of copies of P running in parallel. If there is such a network invariant, by reasoning about it, uniform verification with respect to the family P[1] || ... || P[n] can be carried out. In this paper, we propose a procedure searching systematically for a network invariant satisfying a given safety property. The search is optimized using a combination of Angluin's and Biermann's learning/inference algorithms for improving successively possible invariants. We also show how to reduce the learning problem to SAT, allowing efficient SAT solvers to be used, which turns out to yield a very competitive learning algorithm. The overall search procedure finds a minimal such invariant, if it exists.
15:30‑16:00	Christian Urban (Technical University of Munich) Stefan Berghofer (Technische Universität München) A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL The nominal datatype package provides for Isabelle/HOL an infrastructure for defining languages involving binders and for reasoning conveniently about alpha-equivalence classes. Pitts stated some general conditions under which functions over alpha-equivalence classes can be defined by a form of structural recursion and gave a clever, but very difficult, proof for the existence of a primitive-recursion combinator. We give a version of this proof that works directly over alpha-equivalence classes and does not use auxiliary constructions. This allows us to state our primitive-recursion combinator directly over the constructors with which an alpha-equivalence class is constructed. We further introduce proving tools and heuristics that made the automation of our proof tractable. This is one important prerequisite for the nominal datatype package to become useful.

Break (16:00‑16:30)

Keynote Session (16:30‑17:30)
Chair: Wolfram Schulte, Moshe Vardi
Location: Grand Ballroom B/C

16:30‑17:30

David Harel (Weizmann Institute) Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt] We concentrate on executing scenario-based, inter-object programs. The basic play-out method for live sequence charts (LSCs), which we proposed several years ago and implemented in the Play-Engine tool, deals with the nondeterminism inherent in such programming like racing conditions. It thus cannot correct unsuccessful choices it makes. The talk discusses three more recent and more sophisticated ways to run LSCs, and by extension to execute scenario-based models and programs in general. Interestingly, and somewhat unusually, these three methods use, respectively, ideas from three quite separate fields of computer science: verification (model-checking), artificial intelligence (planning algorithms) and programming methods (Aspect-oriented programming).

IJCAR Business Meeting (18:00‑20:00)
Location: Grand Ballroom B