LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Abstract
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little tool support for transferring this expert knowledge to a wider user audience. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus automating the knowledge transfer loop.
Keywords
Cite
@article{arxiv.1906.08084,
title = {LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL},
author = {Yutaka Nagashima},
journal= {arXiv preprint arXiv:1906.08084},
year = {2020}
}
Comments
This is the pre-print of our paper of the same title accepted at APLAS2019 (https://doi.org/10.1007/978-3-030-34175-6_14). We updated the draft after fixing the errata found by Kenji Miyamoto