# LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL

arXiv: https://arxiv.org/abs/1906.08084 · HTML: https://mlsanity.com/paper/1906.08084/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Jun 2019.

## Built on by (most cited first, 3 of 3)

- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [Genetic Algorithm for Program Synthesis](https://mlsanity.com/paper/2211.11937/) (2022)
- [Learning Rules Explaining Interactive Theorem Proving Tactic Prediction](https://mlsanity.com/paper/2411.01188/) (2024)

## Abstract (arXiv)

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.