Induction in Saturation-Based Proof Search

EasyChair Preprint no. 826

Abstract

Many applications of theorem proving, for example program verification and analysis, require first-order reasoning with both quantifiers and theories such as arithmetic and datatypes. There is no complete procedure for reasoning in such theories but the state-of-the-art in automated theorem proving is still able to reason effectively with real-world problems from this rich domain. In this paper we introduce a missing part of the puzzle: automated induction inside a saturation-based theorem prover. Our goal is to incorporate lightweight automated induction in a way that complements the saturation-based approach, allowing us to solve problems requiring a combination of first-order reasoning, theory reasoning, and inductive reasoning. We implement a number of techniques and heuristics and evaluate them within the Vampire theorem prover. Our results show that these new techniques enjoy practical success on real-world problems.

Keyphrases: automated induction, automated reasoning, first-order logic

@Booklet{EasyChair:826,
  author = {Giles Reger and Andrei Voronkov},
  title = {Induction in Saturation-Based Proof Search},
  howpublished = {EasyChair Preprint no. 826},
  doi = {10.29007/snqj},
  year = {EasyChair, 2019}}