Getting Saturated with Induction

TL;DR

This work integrates induction into saturation-based first-order theorem proving by extending Vampire with dedicated induction inference rules that operate inside the saturation loop. It introduces a suite of mechanisms—Ind, IndMC, IndGen, and IndHRW—for performing induction over term algebras and integers, leveraging structural induction schemas derived from inductively defined data types and recursive definitions. The paper demonstrates how these rules can be instantiated from data-type constructors and function headers, and how generalization and hypothesis rewriting enhance inductive reasoning. Empirical results show that Vampire with induction (Vampire*) solves more problems than the baseline and remains competitive with leading SMT solvers on standard benchmarks, highlighting the practical viability of saturation-based induction and outlining avenues for further refinement.

Abstract

Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire. This is an extended version of a Principles of Systems Design 2022 paper with the same title and the same authors.

Figures (2)

• Figure 1: Motivating example over inductively defined data types.
• Figure 2: The superposition calculus $\mathbb{S}\text{up}$ for first-order logic with equality.