Monday 25 June (Room 6B04)
 

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

Superposition for Lambda-Free Higher-Order Logic
Alexander Bentkamp
Joint work with Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann
(abstract) (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.

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

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

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

Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
Petar Vukmirović
Joint work with Jasmin Blanchette, Simon Cruanes, and Stephan Schulz
(abstract) (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)
 

SGGS: Conflict-Driven First-Order Reasoning
Maria Paola Bonacina
Joint work with David A. Plaisted
(abstract) (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
(abstract) (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.

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

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.

Investigating Higher-Order Simplification for SMT Solving (Work in Progress)
Hans-Jörg Schurr
Joint work with with Pascal Fontaine and Jasmin Blanchette
(abstract) (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.

Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning
Giles Reger
Joint work with Martin Suda and Andrei Voronkov
(abstract) (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.

A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury
Joint work with Jasmin Blanchette and Peter Lammich
(abstract) (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.

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

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.

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Jasmin Blanchette
Joint work with Anders Schlichtkrull, Dmitriy Traytel, and Uwe Waldmann
(abstract) (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.

Wednesday 27 June (Room 6B04)
 

09:00 – 09:45

Dependently Typed Superposition in Lean
Gabriel Ebner
(abstract) (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
(abstract) (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.

11:00 – 11:30

Generalising the One-Point Rule
Johannes Hölzl
Joint work with Pablo Le Hénaff
(abstract) (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
(abstract)

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

Discussion