First European Workshop on
HigherOrder Automated Reasoning
25–27 June 2018, Amsterdam, The Netherlands
Colocated with WAIT 2018
This workshop brings together researchers working on automated deductive techniques for higherorder logics (especially simple type theory and dependent type theory). There has been much progress in recent years with the higherorder automatic theorem provers LeoIII 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 higherorder automatic theorem provers based on stateoftheart firstorder provers, including E, veriT, and CVC4, and to integrate them in popular proof assistants. We believe that firstorder 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 matryoshkadevel mailing list, and join forces.
The workshop is a successor of the LPAR05 workshop on Empirically Successful Automated Reasoning in HigherOrder 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  Welcome 
14:05 – 14:40 
Encoding FirstOrder Horn Formulas in Equational Logic
I will show you how to translate a firstorder 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 
Superposition for LambdaFree HigherOrder Logic I will present refutationally complete superposition calculi for λfree higherorder 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 higherorder logic. 
15:10 – 15:35 
Yet Another Nice and Accurate Interactive Theorem Prover 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. 
Coffee break  
Session 2 (chair: Nicholas Smallbone)  
16:00 – 16:45 
The HigherOrder Prover LeoIII The automated theorem prover LeoIII for classical higherorder logic with Henkin semantics and choice is presented. LeoIII is based on extensional higherorder paramodulation and accepts every common TPTP dialect (FOF, TFF, THF), including their recent extensions to rank1 polymorphism (TF1, TH1). In addition, the prover natively supports reasoning in almost every normal higherorder modal logic. 
16:45 – 17:15 
Pragmatic HigherOrder Theorem Proving via Embedding a Lambda Calculus in
FirstOrder Logic Utilising De Bruijn Indices As pointed out by Gilles Dowek, it is possible to treat higherorder logic as a firstorder 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 higherorder logic. The translation allows for the heuristically guided use of higherorder reasoning steps, which is discussed. 
17:15 – 17:45 
Extending a Brainiac Prover to LambdaFree HigherOrder Logic Instead of developing a new higherorder prover from the ground up, we propose to start with a stateoftheart superpositionbased prover, E, and gradually enrich it with higherorder features. In this talk, I will explain how to extend the prover's core data structures, algorithms, and heuristics to λfree higherorder logic. Our extension clearly outperforms the traditional encodingbased approach. 


Session 3 (chair: Uwe Waldmann)  
09:00 – 09:45 
SGGS: ConflictDriven FirstOrder Reasoning Conflictdriven 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 conflictdriven inferences. SGGS, for SemanticallyGuided GoalSensitive reasoning, extends this paradigm from decision procedures for satisfiability (e.g., SAT, SMT, SMA) to semidecision procedures for firstorder 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 firstorder clausal propagation possible. SGGS extends the partial model by instance generation and literal selection. When a conflict arises, SGGS explains it by conflictdriven resolution and solves it by fixing the model. SGGS is refutationally complete and modelcomplete in the limit. 
09:45 – 10:30 
Revisiting Enumerative Instantiation SMT solvers handle quantified formulas using incomplete heuristic techniques like Ematching, and often resort to modelbased 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. 
Coffee break  
Session 4 (chair: Maria Paola Bonacina)  
11:00 – 11:45 
HigherOrder SMT Solving (Work in Progress) Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full firstorder logic modulo theories. Nevertheless, higherorder logic within SMT (HOSMT) is still little explored. In this presentation, we discuss how to extend SMT solvers to natively support higherorder reasoning without compromising their performances on FO problems. 
11:45 – 12:30 
Investigating HigherOrder Simplification for SMT Solving (Work in Progress) 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. 
Lunch break  
Session 5 (chair: Pascal Fontaine)  
14:00 – 14:45 
Unification with Abstraction and Theory Instantiation in SaturationBased Reasoning 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 firstorder 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 
A Verified SAT Solver with Watched Literals Using Imperative HOL Based on our earlier formalization of conflictdriven 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. 
Coffee break  
Session 6 (chair: Robert Lewis)  
16:00 – 16:45 
SLDResolution Reduction of SecondOrder Horn Fragments The derivation reduction problem for SLDresolution is the problem of finding a minimal finite subset S of a theory T such that T can be generated from S using SLDresolution. I will present the results of our study on the reducibility of various secondorder Horn theories with particular applications in Inductive Logic Programming. 
16:45 – 17:15 
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover 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 firstorder 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. 
19:30 –  Workshop dinner 


Session 7 (chair: Sophie Tourret)  
09:00 – 09:45 
Dependently Typed Superposition in Lean 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 Avatarlike 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 
A Heuristic Method for Formally Verifying Real Inequalities We describe a general method for verifying inequalities between realvalued 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. 
Coffee break  
Session 8 (chair: Alexander Bentkamp)  
11:00 – 11:30 
Generalising the OnePoint Rule The pointrule "(∃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 saturationbased 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 higherorder superposition. We use our result to give an alternative proof of the refutational completeness of Bachmair and Ganzinger's resolution prover RP. 
Lunch break  
Session 9  
13:30 – 15:00 
Discussion 
Coffee break 
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)
HansDieter 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)
HansJö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)
* speakers
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.
713999)
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
publications.)
This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999. 