Domain-Specific Language to Encode Induction Heuristics
Abstract
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a systematic way to encode their expertise. 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 specified by experienced users, thus systematically transferring experienced users' expertise to new Isabelle users.
Keywords
Cite
@article{arxiv.1907.02594,
title = {Domain-Specific Language to Encode Induction Heuristics},
author = {Yutaka Nagashima},
journal= {arXiv preprint arXiv:1907.02594},
year = {2019}
}
Comments
Accepted at ICFP2019-SRC (International Conference on Functional Programming Student Research Competition). Our draft, "LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL" (arXiv:1906.08084), gives further details of this domain specific language. arXiv admin note: substantial text overlap with arXiv:1906.08084