Smart Induction for Isabelle/HOL (Tool Paper)
Yutaka Nagashima · reposiTUm (TU Wien) · 2020
Proof assistants offer tactics to facilitate inductive proofs; however, deciding what arguments to pass to these tactics still requires human ingenuity.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 in-depth evaluation demonstrate that smart_induct produces valuable recommendations across problem domains.Currently, smart_induct is an interactive tool; however, we expect that smart_induct can be used to narrow the search space of automatic inductive provers.