SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL
share
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. We address this problem withSeLFiE, 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. SeLFiE facilitates the intricate interaction between syntactic and semantic analyses using semantic constructs while maintaining the modularity of each analysis.
READ FULL TEXT