Smart Induction for Isabelle/HOL (System Description)
Yutaka Nagashima
TL;DR
This paper introduces smart_induct, a tool for Isabelle/HOL that automatically suggests promising arguments for inductive proofs, reducing the need for human intuition and improving proof automation.
Contribution
It presents a novel approach to automate argument selection for induction tactics in Isabelle/HOL without relying on search methods.
Findings
smart_induct provides valuable inductive argument recommendations
The tool works across various problem domains
It enhances proof automation in Isabelle/HOL
Abstract
Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct lists promising arguments for the induct tactic without relying on a search. Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains.
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.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Logic, programming, and type systems · Numerical Methods and Algorithms