Lassie: HOL4 tactics by example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulová, Rupak Majumdar · 2021
Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requirement that the domain expert is also an expert in the low-level details in constructing the proof in a theorem prover. In particular, the user needs to select a sequence of tactics that lead to a successful proof, a task that in general requires knowledge of the exact names and use of a large set of tactics.