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.
@cite_0: Many proof tools use ‘tactic languages’ as programs to direct their proofs. We present a simplified idealised tactic language, and describe its denotational semantics. The language has many applications outside theorem-proving activities. The semantics is parametrised by a monad (plus additional structure). By instantiating this in various ways, the core semantics of a number of different tactic languages is obtained.
Martin al first discussed a monadic interpretation of tactics for their language, , in an unpublished draft @cite_0 . We independently developed |interp| with the features discussed above, lifting the framework from the tactic level to the strategy level to traverse larger search spaces. The two interpreters for different ITPs turned out to be similar to each other, suggesting our approach is not specific to Isabelle but can be used for other ITPs.