Title: Coinductive Reasoning in Isabelle/HOL

Speaker: Prof. Dmitriy Traytel from the University of Copenhagen

Abstract: Coinductive methods are used to reason about the infinitary behavior of systems, e.g., manifested in traces of useful (potentially) non-terminating programs. Examples of such programs range from semi-decision procedures for automated theorem proving to web servers interacting with clients. In this presentation, I will survey the coinductive capabilities of the Isabelle proof assistant, with a focus on defining and reasoning about corecursive functions. In particular, I will highlight challenges for proof automation that arise in this setting.

Isabelle file used in the demo: here

Isabelle file (full): here

Title: Gauging the strength of inductive theorem provers

Speaker: Dr. Stefan Hetzl from the Vienna University of Technology

Abstract:

Due to Gödel’s incompleteness theorems, methods for inductive theorem proving are inherently incomplete. Nevertheless, for improving our understanding of a particular method M it is useful to characterise the set of theorems provable by M (given unlimited time and memory).

Standard notions and techniques from mathematical logic provide an adequate basis for carrying out such analyses and for building on them to obtain additional results about M. More concretely, we try to find a theory T that is closely related to M in the sense that T proves exactly the same theorems as M or, more realistically, every theorem provable by M is provable by T (but T does not prove “much more”).

In either case, model-theoretic techniques can then be used to obtain a practically relevant independence result, i.e., a simple and natural true statement unprovable in T, and hence unprovable in M. Such statements are suitable challenge problems for the improvement of inductive theorem provers.

In this talk I will present the analyses of several popular methods and put particular emphasis on the challenge problems obtained from them. This talk is based on joint work with Jannik Vierling.

Slides: here

Title: Induction in Saturation-Based Proving

Speaker: Prof. Andrei Voronkov from the University of Manchester and Ms. Petra Hozzová from the Vienna University of Technology

Abstract:

Induction in saturation-based first-order theorem proving is a new exciting direction in automated reasoning, bringing together inductive reasoning and reasoning with full first-order logic extended with theories.

In this tutorial, we dive into our recent results in this area.

Traditional approaches to inductive theorem proving, based on goal-subgoal reduction, incompatible with saturation algorithms where the search space can simultaneously contain hundreds of thousands of formulas, with no clear notion of a goal.

Rather, our approach applies induction by theory lemma generation: from time to time we add to the search space instances of induction axioms, which are valid in the underlying theory but not valid in first-order predicate logic. To formalise this, we introduce new inference rules adding (clausal forms of) such induction axioms within saturation. Applications of these rules are triggered by recognition of formulas in the search space that can be considered as goals solvable by induction.

We also propose additional reasoning methods for strengthening inductive reasoning, as well as for handling recursive function definitions. We implemented our work in the Vampire theorem prover and demonstrate the practical impact in experiments.

The tutorial will consist of the following parts supported by live demonstrations:

  1. Introduction to saturation-based reasoning and superposition
  2. Integration of induction into saturation [1]
  3. Case studies: integer induction and recursive definitions [2, 3]
  4. How far can we go with induction in saturation?
  5. Future outlooks: using automated inductive proving in proof assistants and beyond

References:

Slides: here