Faster Smarter Proof by Induction in Isabelle/HOL
Abstract
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.
Cite
Text
Nagashima. "Faster Smarter Proof by Induction in Isabelle/HOL." International Joint Conference on Artificial Intelligence, 2021. doi:10.24963/IJCAI.2021/273Markdown
[Nagashima. "Faster Smarter Proof by Induction in Isabelle/HOL." International Joint Conference on Artificial Intelligence, 2021.](https://mlanthology.org/ijcai/2021/nagashima2021ijcai-faster/) doi:10.24963/IJCAI.2021/273BibTeX
@inproceedings{nagashima2021ijcai-faster,
title = {{Faster Smarter Proof by Induction in Isabelle/HOL}},
author = {Nagashima, Yutaka},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2021},
pages = {1981-1988},
doi = {10.24963/IJCAI.2021/273},
url = {https://mlanthology.org/ijcai/2021/nagashima2021ijcai-faster/}
}