Download PDFOpen PDF in browser

Integer Induction in Saturation

EasyChair Preprint 5176

16 pagesDate: March 18, 2021

Abstract

Integers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the Vampire theorem prover and evaluated our work against comparable state-of-the-art reasoners. Our results demonstrate the strength of our approach by solving new problems inspired by program analysis and mathematical properties of integers.

Keyphrases: automated reasoning, first-order theorem proving, induction, integer induction, saturation, saturation-based theorem proving, superposition theorem prover, theorem proving

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:5176,
  author    = {Petra Hozzová and Laura Kovács and Andrei Voronkov},
  title     = {Integer Induction in Saturation},
  howpublished = {EasyChair Preprint 5176},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser