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_1: This paper describes SEPIA, a tool for automated proof generation in Coq. SEPIA combines model inference with interactive theorem proving. Existing proof corpora are modelled using state-based models inferred from tactic sequences. These can then be traversed automatically to identify proofs. The SEPIA system is described and its performance evaluated on three Coq datasets. Our results show that SEPIA provides a useful complement to existing automated tactics in Coq.
@cite_1 is an automated proof generation tool in Coq. Taking existing Coq theories as input, first produces proof traces, from which it infers an extended finite state machine. Given a conjecture, uses this model to search for its proof. 's search algorithm is based on the breadth-first search (BFS) to return the shortest proof. can also adopt BFS, as BFS is a special case of IDDFS. However, our experience tells that the search tree tends to be very wide and some tactics, such as , need to be followed by other tactics to complete proofs. Therefore, we chose IDDFS for . Both and off-load the construction of proof scripts to search and try to reconstruct efficient proof scripts. Compared to , allows users to specify their own search strategies to utilize the engineer's intuition, which enables to return incomplete proof scripts, as discussed in Section .