Smart Induction for Isabelle/HOL (Tool Paper)

• Venue: The 20th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2020)
• Location: Online
• Author: Yutaka Nagashima
• Paper: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_32
• Video: https://youtu.be/iaH0Mx926CU

Abstract

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.

Video

Project Dependency Graph

Mindmap