Download PDFOpen PDF in browser

The Vampire Approach to Induction

EasyChair Preprint 9217

11 pagesDate: November 1, 2022

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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}}
Download PDFOpen PDF in browser