Faster Smarter Induction in Isabelle/HOL

09/19/2020
by   Yutaka Nagashima, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset