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

## TL;DR

LiFtEr is a domain-specific language that encodes induction heuristics for Isabelle/HOL, enabling automated checking and transfer of expert knowledge to broader users in theorem proving.

## Contribution

The paper introduces LiFtEr, a novel language that formalizes and automates the application of induction heuristics in Isabelle/HOL.

## Key findings

- LiFtEr successfully encodes various induction heuristics.
- Automated checking of heuristics improves proof automation.
- LiFtEr enhances knowledge transfer among Isabelle users.

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