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

14:40 – 15:10

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

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

Yet Another Nice and Accurate Interactive Theorem Prover
Freek Wiedijk
(slides)

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 Higher-Order Prover Leo-III
Alexander Steen
Joint work with Christoph Benzmüller and Max Wisniewski
(slides)

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
Ahmed Bhayat
Joint work with Giles Reger and Andrei Voronkov
(slides)

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

Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
Petar Vukmirović
Joint work with Jasmin Blanchette, Simon Cruanes, and Stephan Schulz
(slides)

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.


Tuesday 26 June (Room 6A04)
 

Session 3 (chair: Uwe Waldmann)

09:00 – 09:45

SGGS: Conflict-Driven First-Order Reasoning
Maria Paola Bonacina
Joint work with David A. Plaisted
(slides)

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

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

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.

Coffee break

Session 4 (chair: Maria Paola Bonacina)

11:00 – 11:45

Higher-Order SMT Solving (Work in Progress)
Daniel El Ouraoui
Joint work with Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, and Cesare Tinelli

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

Investigating Higher-Order Simplification for SMT Solving (Work in Progress)
Hans-Jörg Schurr
Joint work with with Pascal Fontaine and Jasmin Blanchette
(slides)

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 Saturation-Based Reasoning
Giles Reger
Joint work with Martin Suda and Andrei Voronkov
(slides)

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

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

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.

Coffee break

Session 6 (chair: Robert Lewis)

16:00 – 16:45

SLD-Resolution Reduction of Second-Order Horn Fragments
Sophie Tourret
Joint work with Andrew Cropper

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

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

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.

19:30 –

Workshop dinner
Sama Sebo (Indonesian cuisine)


Wednesday 27 June (Room 6B04)
 

Session 7 (chair: Sophie Tourret)

09:00 – 09:45

Dependently Typed Superposition in Lean
Gabriel Ebner
(slides)

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

A Heuristic Method for Formally Verifying Real Inequalities
Robert Lewis
Joint work with Jeremy Avigad
(slides)

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.

Coffee break

Session 8 (chair: Alexander Bentkamp)

11:00 – 11:30

Generalising the One-Point Rule
Johannes Hölzl
Joint work with Pablo Le Hénaff
(slides)

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
Uwe Waldmann

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.

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

* speakers

Alexander Bentkamp (VU Amsterdam)
Jasmin Blanchette (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. 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.