Rewriting and Inductive Reasoning

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 miss- ing crucial consequences. We therefore extend the superposition calculus with rewriting- based techniques to generate sufficient consequences for automating induction in satura- tion. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.