Matryoshka 2018

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 in the OZW building of the Vrije Universiteit Amsterdam, room 6A04 and 6B04. 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 25 June in the afternoon. It is expected to end on 27 June in the early afternoon.

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).

Superposition for Lambda-Free Higher-Order Logic
Alexander Bentkamp
Joint work with Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann

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.

Pragmatic Higher-Order Theorem Proving via Embedding a Lambda Calculus in First-Order Logic Utilising De Bruijn Indices
Ahmed Bhayat

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.

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Jasmin Blanchette
Joint work with Anders Schlichtkrull, Dmitriy Traytel, and Uwe Waldmann

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.

Dependently Typed Superposition in Lean
Gabriel Ebner

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.

A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury
Joint work with Jasmin Blanchette and Peter Lammich

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.

Revisiting Enumerative Instantiation
Pascal Fontaine
Joint work with Andrew Reynolds and Haniel Barbosa

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.

Encoding First-Order Horn Formulas in Equational Logic
Nicholas Smallbone
Joint work with Koen Claessen

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.

The Higher-Order Prover Leo-III
Alexander Steen
Joint work with Christoph Benzmüller and Max Wisniewski

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.

Alexander Bentkamp (VU Amsterdam)
Jasmin Christian Blanchette (VU Amsterdam)

Alexander Bentkamp* (VU Amsterdam)
Ahmed Bhayat* (U. Manchester)
Jasmin Christian Blanchette* (VU Amsterdam)
Sander Dahmen (VU Amsterdam)
Gabriel Ebner* (TU Wien)
Daniel El Ouraoui* (U. Lorraine and Inria Nancy)
Mathias Fleury* (MPII Saarbrücken)
Pascal Fontaine* (U. Lorraine)
Johannes Hölzl* (VU Amsterdam)
Robert Y. Lewis* (VU Amsterdam)
Andrei Popescu (Middlesex U.)
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)
Sophie Tourret* (MPII Saarbrücken)
Petar Vukmirović* (VU Amsterdam)
Uwe Waldmann* (MPII Saarbrücken)

* confirmed speakers

This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No. 713999). We also want to thank Mojca Lovrencak and Caroline Waij for helping with the local organization.

      This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.