Faster Smarter Induction in Isabelle/HOL

09/19/2020

∙

by   Yutaka Nagashima, et al.

∙

0

∙

share

We present semantic_induct, an automatic tool to recommend how to apply proof by induction in Isabelle/HOL. Given an inductive problem, semantic_induct produces candidate arguments to the induct tactic and selects promising ones using heuristics. Our evaluation based on 1,095 inductive problems from 22 theory files shows that semantic_induct achieves a 90.0% increase of the coincidence rate for the most promising candidate within 5.0 seconds of timeout compared to an existing tool, smart_induct, while achieving a 62.0% decrease of the median value of execution time.