Induction in Saturation-Based Proof Search

EasyChair Preprint 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},
  doi       = {10.29007/snqj},
  howpublished = {EasyChair Preprint 826},
  year      = {EasyChair, 2019}}