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

arXiv: https://arxiv.org/abs/1606.02941 · HTML: https://mlsanity.com/paper/1606.02941/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Jun 2016.

## Built on by (most cited first, 5 of 5)

- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Genetic Algorithm for Program Synthesis](https://mlsanity.com/paper/2211.11937/) (2022)
- [Abduction Prover in Isabelle/HOL](https://mlsanity.com/paper/2606.04877/) (2026)

## Abstract (arXiv)

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.