Faster Smarter Proof by Induction in Isabelle/HOL
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Main Track. Pages 1981-1988.
https://doi.org/10.24963/ijcai.2021/273
Keywords
- Multidisciplinary Topics and Applications: Validation and Verification
- Knowledge Representation and Reasoning: Logics for Knowledge Representation
- Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving
- Heuristic Search and Game Playing: Meta-Reasoning and Meta-Heuristics
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.
@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 = {Prof. 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},
}
TY - CPAPER TI - Faster Smarter Proof by Induction in Isabelle/HOL AU - Nagashima, Yutaka T2 - Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21 PB - International Joint Conferences on Artificial Intelligence Organization PY - 2021 SP - 1981 EP - 1988 DO - 10.24963/ijcai.2021/273 UR - https://doi.org/10.24963/ijcai.2021/273 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
