IJCAI 2021poster8 citations
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.
Knowledge Representation and Reasoning: Automated Reasoning and Theorem ProvingMultidisciplinary Topics and Applications: Validation and VerificationHeuristic Search and Game Playing: Meta-Reasoning and Meta-HeuristicsKnowledge Representation and Reasoning: Logics for Knowledge Representation
BibTeX
@inproceedings{ijcai2021p273,
title = {Faster Smarter Proof by Induction in Isabelle/HOL},
author = {Nagashima, Yutaka},
booktitle = {Proceedings of the Thirtieth International Joint Conference on
Artificial Intelligence, {IJCAI-21}},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
editor = {Zhi-Hua Zhou},
pages = {1981--1988},
year = {2021},
month = {8},
note = {Main Track},
doi = {10.24963/ijcai.2021/273},
url = {https://doi.org/10.24963/ijcai.2021/273},
}