Download PDFOpen PDF in browserCurrent version

Induction with Generalization in Superposition Reasoning

EasyChair Preprint 2468, version 1

Versions: 12history
6 pagesDate: January 27, 2020

Abstract

We describe an extension of automating induction in superposition-based reasoning by strengthening inductive properties and generalizing terms over which induction should be applied. We implemented our approach in the first-order theorem prover Vampire and evaluated our work against state-of-the-art reasoners automating induction.

We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.

Keyphrases: AVATAR architecture, Vampire, automated reasoning, first-order theorem proving, induction, induction with generalization, saturation based proof search, structural induction, superposition reasoning, term algebra

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:2468,
  author    = {Petra Hozzová and Laura Kovács and Johannes Schoisswohl and Andrei Voronkov},
  title     = {Induction with Generalization in Superposition Reasoning},
  howpublished = {EasyChair Preprint 2468},
  year      = {EasyChair, 2020}}
Download PDFOpen PDF in browserCurrent version