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_20: We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [ 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs.
offers a framework for encoding and applying common patterns of reasoning in Isabelle, following the style of proof planning @cite_20 . addresses the performance issue by memoization technique, on the other hand try strips off backtracked steps while searching for a proof, which Isabelle can check later without try . While works on its own data structure , managed to minimize the deviation from Isabelle's standard execution model using constructor classes.