A Proof Strategy Language and Proof Script Generation for Isabelle/HOL

TL;DR

This paper presents PSL, a language for high-level proof strategies in Isabelle/HOL, which efficiently generates proof scripts by exploring large search spaces with low memory usage.

Contribution

Introduction of PSL, a novel language for capturing proof strategies and generating proof scripts in Isabelle/HOL, with a transferable monadic interpreter.

Findings

PSL effectively explores large proof search spaces.

Generated proof scripts bypass extensive proof search.

PSL's approach is adaptable to other interactive theorem provers.

Abstract

We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL's monadic interpreter to show that the underlying idea of PSL is transferable to other ITPs.