Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar

TL;DR
Lassie is a framework for HOL4 that enables users to define custom tactics by example, simplifying proof construction without requiring low-level tactic implementation knowledge.
Contribution
Lassie introduces an extensible semantic parser allowing users to create and extend tactics interactively, improving usability and accessibility in HOL4 proof development.
Findings
Enables user-defined tactics without custom implementation
Facilitates easier learning curve for HOL4 users
Proven effective in small and large proof scenarios
Abstract
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. We present Lassie, a tactic framework for the HOL4 theorem prover that allows individual users to define their own tactic language by example and give frequently used tactics or tactic combinations easier-to-remember names. The core of Lassie is an extensible semantic parser, which allows the user to interactively extend the tactic language through a process of definitional generalization. Defining…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
