The Vampire Approach to Induction

EasyChair Preprint 9217

Abstract

We 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

@booklet{EasyChair:9217,
  author    = {Marton Hajdu and Laura Kovacs and Michael Rawson and Andrei Voronkov},
  title     = {The Vampire Approach to Induction},
  howpublished = {EasyChair Preprint 9217},
  year      = {EasyChair, 2022}}