# Domain-Specific Language to Encode Induction Heuristics

## TL;DR

This paper introduces LiFtEr, a domain-specific language that enables expert Isabelle users to encode and systematically transfer their induction heuristics to less experienced users, improving inductive theorem proving.

## Contribution

The paper presents LiFtEr, a novel language for encoding induction heuristics, facilitating systematic knowledge transfer among Isabelle users.

## Key findings

- LiFtEr successfully encodes induction heuristics.
- The interpreter verifies heuristic application in proofs.
- Enhances knowledge sharing in inductive theorem proving.

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