Download PDFOpen PDF in browserThe Vampire Approach to InductionEasyChair Preprint 921711 pages•Date: November 1, 2022AbstractWe discuss practical aspects of automating inductive reasoning in the first-order superposition prover Vampire. We explore solutions for reasoning over inductively defined dataypes; generating, storing and applying induction schema instances; and directly integrating inductive reasoning into the saturation reasoning loop of Vampire. Our techniques significantly improve the performance of Vampire despite the inherent difficulty of automated induction. We expect our exposition to be useful when implementing induction in saturation-style provers, and to stimulate further discussion and advances in the area. Keyphrases: first-order theorem proving, induction, saturation, superposition
|