SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL

Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. We address this problem with SeLFiE, a domain-specific language to encode experienced users' expertise on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the SeLFiE interpreter examines both the syntactic structure of the problem and semantics of the relevant constants to judge whether the arguments to the induct tactic are plausible for that problem according to the heuristic.