Fourth International Workshop on Automated (Co)inductive Theorem Proving
28–29 June 2018, Amsterdam, The Netherlands
Inductive and coinductive theorem proving is a topic of growing interest in the automated reasoning community. The Fourth International Workshop on Automated (Co)inductive Theorem Proving (WAIT 2018) focuses on all relevant aspects of (co)inductive reasoning.
The workshop is an informal event and aims to give researchers interested in the topic a chance to meet, exchange ideas, and have a platform for discussions.
We invite talks featuring demonstrations and tutorials of (co)inductive theorem provers, challenge problems, new directions of research, or anything else of interest to the (co)inductive theorem proving community.
Please send an email to the organizers if you would like to give a talk, demonstrate a tool, or otherwise participate.
The workshop will take place on 28 and 29 June 2018 in the main building of the Vrije Universiteit Amsterdam, room Agora 3. The VU is easily accessible on foot from the Amsterdam Zuid station, a short train ride away from Amsterdam Airport Schiphol. The workshop will start on 28 June in the morning. It is expected to end in the early afternoon on 29 June.
WAIT 2018 will take place the same week as the First European Workshop on Higher-Order Automated Reasoning (Matryoshka 2018).
Hotels in Amsterdam can be very expensive. Even the cheapest options often cost over 100 euros per night. The neighboring city of Amstelveen has more reasonably priced options (e.g., Ibis) and is located close to the VU campus, a few stops away by public transportation (tram line 5 or metro line 51).
Recursive Proofs for Coinductive Predicates
We will discuss in this talk how to extend logics with the so-called later modality, which allows us to construct recursive proofs for arbitrary coinductive predicates. The later modality enables goal-directed proof discovery and the use any up-to technique that is provably compatible in the underlying logic. Often, we find that the resulting proof system also admits induction, either because of the nature of the coinductive predicate or through an up-to technique.
Tree Grammars for Induction on Inductive Data Types modulo Equational Theories
Inductive theorem proving based on tree grammars was introduced by Eberhard and Hetzl in 2015. In this approach, proofs with induction on natural numbers are found by generalizing automatically generated proofs of finite instances on the level of Herbrand disjunctions. We extend this method to support general inductive data types, and reasoning modulo a background theory to abstract from irregularities in automatically generated proofs. We present an experimental implementation of the method and show that it automatically produces non-analytic induction formulas for several examples.
Theory Exploration for Coinduction
Sólrún Halla Einarsdóttir
We have extended theory exploration to discover coinductive lemmas about corecursive (co)datatypes and functions. This required new methods for testing infinite values and for automated coinductive proofs. Our extension has been implemented in the Hipster theory exploration system for the proof assistant Isabelle/HOL.
Towards Coinductive Theory Exploration in Horn Clause Logic
Coinduction occurs in two guises in Horn clause logic: in proofs of self-referencing properties and relations, and in proofs involving construction of infinite data. Both instances of coinductive reasoning appeared in the literature before, but a systematic analysis of these two kinds of proofs and of their relation was lacking. We propose a general proof-theoretic framework for handling both kinds of coinduction arising in Horn clause logic. To this aim, we propose a coinductive extension of Miller et al’s framework of uniform proofs which we then use as a machinery for formulating and proving coinductive invariants required in proofs with first-order Horn clause logic.
Friendly Corecursion in Isabelle/HOL
Joint work with Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, and Dmitriy Traytel
Corecursion is a mechanism for defining functions that produce infinite objects such as streams, lazy lists and infinite-depth trees. Establishing corecursion schemes that are expressive, sound and automatic is a notoriously hard problem. I will discuss an approach, implemented in the proof assistant Isabelle/HOL, for training a logical system to learn stronger and stronger schemes on a sound basis. The central notion is that of a friendly operator (or friend), which constitutes a statically safe context for corecursive calls. The framework relies on the ability to recognize friends quasi-automatically by verifying relational parametricity conditions. I will also discuss some ideas on how to go beyond statically safe contexts with the price of mild dynamic checks.
What Are the Suitable Data Types for Syntax with Bindings?
Joint work with Jasmin Blanchette, Lorenzo Gheri, and Dmitriy Traytel
Syntax with bindings is notoriously difficult to formalize and reason about in proof assistants. A main cause for this is the difficulty to characterize syntax with bindings by means of abstract data types in a useful way, so as to provide high-level structural induction and recursion principles. I will discuss some approaches to address this problem, including a recent line of work pursued in Isabelle/HOL together with colleagues.
Superposition with Datatypes and Codatatypes
Joint work with Jasmin Blanchette and Nicolas Peltier
The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We present two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms.
Finding Loop Invariants with QuickSpec (Work in Progress)
Recently I've been playing with using QuickSpec on imperative programs to discover loop invariants and similar assertions. I will talk about how I do it, as well as a crazy idea you can implement on top of it: psychic property-based testing.
Cyclic Superposition and Induction
In 2013 Kersani and Peltier introduced the n-clause calculus, a superposition calculus enriched with a cycle detection rule realizing a form of reasoning by mathematical induction. Until now it is not known which form of induction is captured by the n-clause calculus. An upper bound in terms of the quantifier complexity of the induction invariant can be obtained by a two step translation: in a first step we encode cyclic refutations in a cyclic sequent calculus introduced by Brotherston and Simpson in 2010; in a second step we translate cyclic proofs into inductive LK proofs.
Maximilian Algehed* (Chalmers Gothenburg)
Henning Basold* (ENS Lyon)
Alexander Bentkamp (VU Amsterdam)
Jasmin Christian Blanchette* (VU Amsterdam)
Koen Claessen* (Chalmers Gothenburg)
Gabriel Ebner* (TU Wien)
Sólrún Halla Einarsdóttir* (Chalmers Gothenburg)
Daniel El Ouraoui (U. Lorraine and Inria Nancy)
Pascal Fontaine* (U. Lorraine)
Stefan Hetzl (TU Wien)
Johannes Hölzl (VU Amsterdam)
Moa Johansson* (Chalmers Gothenburg)
Ekaterina Komendantskaya* (Heriot-Watt U.)
Robert Y. Lewis (VU Amsterdam)
Andrei Popescu** (Middlesex U.)
Martin Riener (U. Manchester)
Simon Robillard* (Chalmers Gothenburg)
Hans-Jörg Schurr (U. Lorraine and Inria Nancy)
Nicholas Smallbone (Chalmers Gothenburg)
Jannik Vierling* (TU Wien)
Petar Vukmirović (VU Amsterdam)
* confirmed speakers
|This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.|