Tags:algebraic data types, automated reasoning, first-order theorem proving, induction and superposition
Abstract:
We describe an extension of automating induction in superposition-based reasoning by strengthening inductive properties and generalizing terms over which induction should be applied. We implemented our approach in the first-order theorem prover Vampire and evaluated our work against state-of-the-art reasoners automating induction.We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.
Induction with Generalization in Superposition Reasoning