Thursday 28 June
 

Tree Grammars for Induction on Inductive Data Types modulo Equational Theories
Gabriel Ebner
Joint work with Stefan Hetzl
(abstract) (slides)

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.

Finding Loop Invariants with QuickSpec (Work in Progress)
Nicholas Smallbone
(abstract) (slides)

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.

SMT-LIB 3: Bringing Higher-Order Logic to SMT
Pascal Fontaine
Joint work with Clark Barrett and Cesare Tinelli
(abstract) (slides)

I will first present the recent advances in SMT-LIB, and the future directions. I will also review the TIP format, and quickly discuss the features that have been imported into SMT-LIB, and those that aren't yet. We (the SMT-LIB managers) are keen to get input and feedback from the community, so I will be happy if the talk quickly becomes an open discussion about the nice features you want, the restrictions you hate, and get suggestions to make SMT-LIB an even more solid, clean, and clear standard for your problems.

Clark Barrett, Pascal Fontaine and Cesare Tinelli are the current SMT-LIB managers and are co-authors of this presentation (but Pascal will take all the blame for mistakes, e.g. misunderstanding TIP features).

An Induction Principle for Automated Induction
Koen Claessen
Joint work with Linnea Andersson and Andres Wahlström
(abstract) (slides) (link)

We explore alternatives to structural induction for use in automated induction. Our main candidate is a generalization of recursion induction.

Putting Theory Exploration to Work
Moa Johansson
(abstract) (slides)

I will give a brief introduction to the theory exploration system Hipster, which discovers and proves lemmas by induction automatically. There will be a simple demo on some small examples, followed by a more speculative part where I'll invite to discussion on what is needed to make theory exploration tools efficient, stable and general enough to be of real use in e.g. a proof assistant.

Theory Exploration for Coinduction
Sólrún Halla Einarsdóttir
Joint work with Moa Johansson and Johannes Åman Pohjola
(abstract) (slides)

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.

Recursive Proofs for Coinductive Predicates
Henning Basold
(abstract)

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.

Mechanically Certifying Formula-Based Noetherian Induction Reasoning
Sorin Stratulat
(abstract) (slides)

I describe general formal tools for certifying formula-based Noetherian induction proofs by Coq, then show how to apply them to certify cyclic proofs of conjectures about conditional specifications. The certification methodology can be easily adapted to automatically certify proofs built with a reductive rewrite-based inference system and, more generally, any formula-based Noetherian induction reasoning.

What Are the Suitable Data Types for Syntax with Bindings?
Andrei Popescu
Joint work with Jasmin Blanchette, Lorenzo Gheri, and Dmitriy Traytel
(abstract) (slides)

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.

Wrap-up

Friday 29 June
 

Towards Coinductive Theory Exploration in Horn Clause Logic
Ekaterina Komendantskaya
(abstract) (slides)

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.

09:45 – 10:30

Finite and Infinite Traces, Inductively and Coinductively
Jurriaan Rot
(abstract) (slides)

It is a well-known fact (used e.g. in model checking) that, on finitely branching transition systems, finite trace equivalence coincides with infinite trace equivalence. I will show how to prove this coinductively, which is arguably nicer than the standard inductive proof.

Cyclic Superposition and Induction
Jannik Vierling
(abstract) (slides)

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.

Superposition with Datatypes and Codatatypes
Simon Robillard
Joint work with Jasmin Blanchette and Nicolas Peltier
(abstract) (slides)

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.

Friendly Corecursion in Isabelle/HOL
Andrei Popescu
Joint work with Jasmin Blanchette, Aymeric Bouzy, Andreas Lochbihler, and Dmitriy Traytel
(abstract) (slides)

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.

Discussion