This year, I presented my domain-specific language, SeLFiE, and the concept it implements at TAP2022. Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users’ knowledge on how to apply the induct tactic …
Continue reading Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction