First European Workshop on
Higher-Order Automated Reasoning
25–27 June 2018, Amsterdam, The Netherlands
Co-located with WAIT 2018
This workshop brings together researchers working on automated deductive techniques for higher-order logics (especially simple type theory and dependent type theory). There has been much progress in recent years with the higher-order automatic theorem provers Leo-III and Satallax, the Lean proof assistant, and metaprovers such as HOLyHammer and Sledgehammer.
With the Matryoshka project, we aim at designing a new generation of higher-order automatic theorem provers based on state-of-the-art first-order provers, including E, veriT, and CVC4, and to integrate them in popular proof assistants. We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. We encourage researchers motivated by the same goals to get in touch with us, subscribe to the matryoshka-devel mailing list, and join forces.
The workshop is a successor of the LPAR-05 workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), held in Montego Bay, Jamaica. The Matryoshka workshop series is conceived to be a meeting point for the Matryoshka team and colleagues working on the same challenge. It is an informal event. We expect to hold it at least once a year until the project's completion in 2022.
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 25, 26, and 27 June 2018 on the 6th floor of the OZW building of the Vrije Universiteit Amsterdam, room 6A04 (Tuesday) and 6B04 (Monday and Wednesday). The VU is easily accessible on foot from the Amsterdam Zuid station, a short train ride away from Amsterdam Airport Schiphol. There are also parking spaces. See How to get to VU Amsterdam for details. The workshop will start on 25 June at 14:00 and end on 27 June at 15:00.
Matryoshka 2018 will take place the same week as the Fourth Workshop on Automated Inductive Theorem Proving (WAIT 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).
Monday 25 June (Room 6B04)
Session 1 (chair: Jasmin Blanchette)
|14:00 – 14:05
|14:05 – 14:40
I will show you how to translate a first-order Horn problem into a unit
equality problem. This sounds like an excellent way to make the problem harder
to solve, but in fact is quite useful, because it turns any equational theorem
prover into a Horn prover. The technique (perhaps unsurprisingly) works well
for Horn problems that involve heavy equational reasoning.
|14:40 – 15:10
I will present refutationally complete superposition calculi for λ-free higher-order logic, a formalism that allows partial application and applied variables. We implemented the calculi in the Zipperposition prover and evaluated them on TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.
|15:10 – 15:35
I will outline plans for an interactive theorem prover that I would like to develop. It will be based on FOL (with schemes) and ZFC, it will be typed with (soft) dependent types, and for this reason it will have to take partiality seriously. It might become slow and hard to use, but I still would like to explore this corner of the design space of interactive theorem proving.
Session 2 (chair: Nicholas Smallbone)
|16:00 – 16:45
The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF, TFF, THF), including their recent extensions to rank-1 polymorphism (TF1, TH1). In addition, the prover natively supports reasoning in almost every normal higher-order modal logic.
|16:45 – 17:15
Pragmatic Higher-Order Theorem Proving via Embedding a Lambda Calculus in
First-Order Logic Utilising De Bruijn Indices
As pointed out by Gilles Dowek, it is possible to treat higher-order logic as a first-order theory by converting lambda expressions to De Bruijn notation and treating the lambda as a unary function. We have implemented this translation and begun to explore its potential for proving theorems in an unspecified fragment of higher-order logic. The translation allows for the heuristically guided use of higher-order reasoning steps, which is discussed.
|17:15 – 17:45
Instead of developing a new higher-order prover from the ground up, we propose to start with a state-of-the-art superposition-based prover, E, and gradually enrich it with higher-order features. In this talk, I will explain how to extend the prover's core data structures, algorithms, and heuristics to λ-free higher-order logic. Our extension clearly outperforms the traditional encoding-based approach.
Session 3 (chair: Uwe Waldmann)
|09:00 – 09:45
Conflict-driven reasoning procedures search simultaneously for a model or a refutation of the input formula by proposing candidate models, deriving new formulae implied by the input, detecting conflicts between model and formulae, and repairing the model by conflict-driven inferences. SGGS, for Semantically-Guided Goal-Sensitive reasoning, extends this paradigm from decision procedures for satisfiability (e.g., SAT, SMT, SMA) to semidecision procedures for first-order theorem proving. SGGS uses a sequence of constrained clauses with selected literals to represent a partial model. A given interpretation provides semantic guidance and makes first-order clausal propagation possible. SGGS extends the partial model by instance generation and literal selection. When a conflict arises, SGGS explains it by conflict-driven resolution and solves it by fixing the model. SGGS is refutationally complete and model-complete in the limit.
09:45 – 10:30
SMT solvers handle quantified formulas using incomplete heuristic techniques like E-matching, and often resort to model-based quantifier instantiation (MBQI) when these techniques fail. We revisit enumerative instantiation, which considers instantiations based on exhaustive enumeration of ground terms. Enumerative instantiation can supplement other instantiation techniques and be a viable alternative to MBQI for valid proof obligations. We first present a stronger Herbrand Theorem, better suited as a basis for the instantiation loop used in SMT solvers; it furthermore requires considering less instances than classical Herbrand instantiation. Based on this, we present different strategies for combining enumerative instantiation with other instantiation techniques. The experimental evaluation shows that the implementation of these new techniques in CVC4 leads to significant improvements in several benchmark libraries.
Session 4 (chair: Maria Paola Bonacina)
|11:00 – 11:45
Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT (HOSMT) is still little explored. In this presentation, we discuss how to extend SMT solvers to natively support higher-order reasoning without compromising their performances on FO problems.
|11:45 – 12:30
During proof construction with interactive systems such as Isabelle/HOL simplification tactics provide a straightforward and basic form of automatization. These tactics rewrite a proof goal with a user defined set of rewrite rules. In the case of Isabelle/HOL the simplifier is often able to solve proof goals which Sledgehammer can not. In this talk I discuss how Isabelle's simplifier works, how simplification is currently applied in SMT solvers, and possible work to extend this.
Session 5 (chair: Pascal Fontaine)
|14:00 – 14:45
In Vampire we’ve been looking at combining reasoning with quantifiers and reasoning with theories for a few years. In this talk I will present our most recent work which is a different way of utilising SMT solvers in first-order provers (different from the approaches taken by e.g. AVATAR modulo theories and hierarchic superposition). This consists of two ideas. The first idea is to find useful instances of a clause where some theory part becomes false, e.g. X > 0 ∨ p(X) has an instance p(1), by passing the negation of the pure theory literals to a SMT solver. The second idea is to extend unification to produce `theory constraints` under which inferences may happen. Such constraints can be handled by the previously introduced instantiation method. This is our first step in this direction and we have many more steps planned.
|14:45 – 15:30
Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.
Session 6 (chair: Robert Lewis)
|16:00 – 16:45
The derivation reduction problem for SLD-resolution is the problem of finding a minimal finite subset S of a theory T such that T can be generated from S using SLD-resolution. I will present the results of our study on the reducibility of various second-order Horn theories with particular applications in Inductive Logic Programming.
|16:45 – 17:15
I will present a formalization of the first half of Bachmair and Ganzinger's chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We developed general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies several of the fine points in the chapter's text.
Session 7 (chair: Sophie Tourret)
09:00 – 09:45
In Lean 3, tactics are defined in the object language and can be efficiently executed using a bytecode interpreter. The super tactic implements a superposition prover for Lean with Avatar-like splitting. The whole prover, including a toy SAT solver, is written in Lean without any changes to the C++ code. The prover supports dependent types, and produces intuitionistic proofs in many cases.
09:45 – 10:30
We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method is heuristic and establishes claims that require heterogeneous forms of reasoning. It is also able to create proof "sketches" or "explanations" that can be inspected by the user. Our method is implemented in Lean, using its metaprogramming framework.
Session 8 (chair: Alexander Bentkamp)
11:00 – 11:30
The point-rule "(∃x, p x ∧ x = t) ↔ p t" is a simple but powerful rule implemented in Isabelle's simplifier. For implementing it in Lean, I want the generalisations "monotone p → (∃x, p x ∧ x ≤ t) ↔ p t". Also I thought about applying Galois connections to focus the variable.
11:30 – 12:00
Redundancy and Subsumption: The Generic Way
Deletion of subsumed clauses is a fundamental operation in any saturation-based theorem prover, but its treatment in formal presentations of proof calculi is usually clumsy. The main reason for this is the fact that in general deletion is permitted only for redundant clauses, but using a standard notion of redundancy, subsumed clauses are not necessarily redundant. We show that any redundancy criterion that is obtained by lifting a ground redundancy criterion to general formulas and inferences can be extended to a redundancy criterion that also permits the deletion of subsumed clauses. We prove this in a fully abstract framework that can not only be applied to ordered resolution or standard superposition, but also to constraint superposition, theory superposition, hierarchic superposition, or higher-order superposition. We use our result to give an alternative proof of the refutational completeness of Bachmair and Ganzinger's resolution prover RP.
13:30 – 15:00
Alexander Bentkamp* (VU Amsterdam)
Ahmed Bhayat* (U. Manchester)
Jasmin Blanchette* (VU Amsterdam)
Maria Paola Bonacina* (U. Verona)
Sander Dahmen (VU Amsterdam)
Martin Desharnais (LMU München)
Gabriel Ebner* (TU Wien)
Daniel El Ouraoui* (U. Lorraine and Inria Nancy)
Mathias Fleury* (MPII Saarbrücken)
Pascal Fontaine* (U. Lorraine)
Shilpi Goel (U. Texas Austin)
Hans-Dieter Hiep (VU Amsterdam)
Marijn Heule (U. Texas Austin)
Johannes Hölzl* (VU Amsterdam)
Joey van Langen (VU Amsterdam)
Pablo Le Hénaff (École Polytechnique Paris)
Robert Y. Lewis* (VU Amsterdam)
Casper Putz (VU Amsterdam)
Giles Reger* (U. Manchester)
Martin Riener (U. Manchester)
Simon Robillard (Chalmers Gothenburg)
Hans-Jörg Schurr* (U. Lorraine and Inria Nancy)
Nicholas Smallbone* (Chalmers Gothenburg)
Alexander Steen* (FU Berlin)
Sorin Stratulat (U. Lorraine)
Sophie Tourret* (MPII Saarbrücken)
Petar Vukmirović* (VU Amsterdam)
Uwe Waldmann* (MPII Saarbrücken)
Freek Wiedijk* (RU Nijmegen)
Wan Fokkink (VU Amsterdam)
Acknowledgment: We want to thank Pascal Fontaine, Mojca Lovrencak,
and Caroline Waij for helping with the organization.
This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No.
and by the NWO incidentele steun scheme.
We kindly ask participants to mention the support from the ERC and the NWO
in publications or in other kinds of scientific output that directly follows
from the workshop. (The NWO would also like to receive a copy of the relevant
|This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.