Faster Smarter Proof by Induction in Isabelle/HOL

Faster Smarter Proof by Induction in Isabelle/HOL

Yutaka Nagashima

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence
Main Track. Pages 1981-1988. https://doi.org/10.24963/ijcai.2021/273

We present sem_ind, a recommendation tool for proof by induction in Isabelle/HOL. Given an inductive problem, sem_ind produces candidate arguments for proof by induction, and selects promising ones using heuristics. Our evaluation based on 1,095 inductive problems from 22 source files shows that sem_ind improves the accuracy of recommendation from 20.1% to 38.2% for the most promising candidates within 5.0 seconds of timeout compared to its predecessor while decreasing the median value of execution time from 2.79 seconds to 1.06 seconds.
Keywords:
Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving
Multidisciplinary Topics and Applications: Validation and Verification
Heuristic Search and Game Playing: Meta-Reasoning and Meta-Heuristics
Knowledge Representation and Reasoning: Logics for Knowledge Representation