Rewriting and Inductive Reasoning

TL;DR

This work tackles automating induction within saturation-based first-order theorem proving by identifying that standard induction triggering can miss crucial consequences. It introduces a rewriting-based extension to the superposition calculus, encapsulated in the ReC framework and its variants, to generate additional equational consequences while preserving equational derivability and inductive capabilities. The authors implement these ideas in Vampire, apply them to unit-equational induction benchmarks, and demonstrate substantial improvements over traditional superposition, including solving previously intractable inductive problems and reducing the search space via redundancy and chaining techniques. The results show significant impact on inductive reasoning and first-order equational reasoning, with practical implications for automated verification and potential integration with proof assistants.

Abstract

Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

Figures (7)

• Figure 1: Motivating example, conjecturing that the first-order formula $\mathsf{Conj}$ is implied by first-order axioms $\mathsf{Ax}$.
• Figure 2: The superposition calculus $\mathbf{Sup}$ for first-order logic with equality.
• Figure 3: Possible rewrite sequences from a ground clause $C_0$ to a ground clause $D$. The total order between clauses is $C_1\succ C_3\succ C_2\succ C_5\succ C_0\succ D\succ C_6\succ C_4\succ C_7$, as also visualized by the vertical alignment of clauses.
• Figure 4: Possible rewrite sequences to derive clause \ref{['eq:negconj4']} from \ref{['eq:negconj']} in the example of Section \ref{['motivating-example']}.
• Figure 5: Possible parallel rewrites in $\mathbf{ReC}$ given equations $a\simeq c$, $b\simeq d$ with $a\succ c$ and $b\succ d$. Rewrites corresponding to crossed out arrows are not performed in the left-to-right order.

Theorems & Definitions (45)

• Definition 1: Equational derivability (ED)
• Theorem 1: --ED
• Remark 1
• Example 1
• Theorem 2: $\ReC_\lor$--ED
• Theorem 3: $\ReC^\to$--ED
• Theorem 4: $\ReC^\to_\lor$--ED
• Remark 2
• Example 2
• Definition 2: Redundant $\mathsf{Ind}\xspace_G$ inference