Tue 17 Jan 2023 10:08 - 10:30 at Studio 1 - Proof Search Chair(s): Brigitte Pientka

We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules, distinguishing between safe and unsafe rules. It uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean’s simplifier to support equational reasoning. Many details of Aesop’s search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be.

Since we use a best-first search strategy, it is not obvious how to handle metavariables (i.e. variables shared between different goals). We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes very few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows.

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Proof SearchCPP at Studio 1
Chair(s): Brigitte Pientka McGill University
(canceled invited talk)

Aesop: White-Box Best-First Proof Search for Leandistinguished paper
Jannis Limperg Vrije Universiteit Amsterdam, Asta Halkjær From Technical University of Denmark
Link to publication DOI Pre-print