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 contribute to 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.
CITATION STYLE
Reger, G., & Voronkov, A. (2019). Induction in saturation-based proof search. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11716 LNAI, pp. 477–494). Springer. https://doi.org/10.1007/978-3-030-29436-6_28
Mendeley helps you to discover research relevant for your work.