Download PDFOpen PDF in browserInteger Induction in SaturationEasyChair Preprint 517616 pages•Date: March 18, 2021AbstractIntegers 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
|