Integer Induction in Saturation

EasyChair Preprint 5176

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

@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}}