---
title: "Faster Smarter Proof by Induction in Isabelle/HOL"
authors:
  - "Yutaka Nagashima"
doi: "10.24963/ijcai.2021/273"
url: "https://ijcai.org/proceedings/2021/273"
pdf: "https://ijcai.org/proceedings/2021/0273.pdf"
venue: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence"
year: 2021
pages: "1981-1988"
track: "Main Track"
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"
---

# Faster Smarter Proof by Induction in Isabelle/HOL

Yutaka Nagashima

*Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence*, pages 1981-1988. DOI: [10.24963/ijcai.2021/273](https://doi.org/10.24963/ijcai.2021/273)

## 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.