Proof assistants, such as Isabelle HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring experienced users' expertise to new Isabelle users.
To determine induction variables automatically, Nagashima al developed a proof strategy language |PSL| and its default proof strategy, |try_hard| for Isabelle HOL @cite_9 . |PSL| tries to identify useful arguments for the |induct| method by conducting a depth-first search. Sometimes it is not enough to pass arguments to the |induct| method, but users have to specify necessary auxiliary lemmas before applying induction. To automate such labor-intensive work, @cite_10 , a new extension to , produces many lemmas by transforming the given proof goal while trying to identify a useful one in a goal-oriented manner.
@cite_9 @cite_10
2962820807 2951079127
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. We present PGT, a Proof Goal Transformer for Isabelle HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle's strong automation to identify and prove such conjectures.