Abstract:
Induction in saturation-based first-order theorem proving is a new exciting direction in automated reasoning, bringing together inductive reasoning and reasoning with full first-order logic extended with theories. In this tutorial, we dive into our recent results in this area.
Traditional approaches to inductive theorem proving, based on goal-subgoal reduction, are incompatible with saturation algorithms where the search space can simultaneously contain hundreds of thousands of formulas, with no clear notion of a goal. Rather, our approach applies induction by theory lemma generation: from time to time we add to the search space instances of induction axioms, which are valid in the underlying theory but not valid in first-order predicate logic. To formalize this, we introduce new inference rules adding (clausal forms of) such induction axioms within saturation. Applications of these rules are triggered by recognition of formulas in the search space that can be considered as goals solvable by induction.
We also propose additional reasoning methods for strengthening inductive reasoning, as well as for handling recursive function definitions. We implemented our work in the Vampire theorem prover and will demonstrate the practical impact in experiments.
The tutorial will consist of the following parts supported by live demonstrations:
- Introduction to saturation-based reasoning and superposition
- Integration of induction into saturation [1]
- Case studies: integer induction and recursive definitions [2, 3]
- How far can we go with induction in saturation?
- Future outlooks: using automated inductive proving in proof assistants and beyond
The tutorial is based on work made with several co-authors and the tutorial content was jointly created with Petra Hozzova.
References:
[1] Induction in Saturation-Based Proof Search (2019), G. Reger and A. Voronkov, in Proc. of CADE https://doi.org/10.1007/978-3-030-29436-6_28
[2] Integer Induction in Saturation (2021), P. Hozzová, L. Kovács, and A. Voronkov, in Proc. of CADE https://doi.org/10.1007/978-3-030-79876-5_21
[3] Induction with Recursive Definitions in Superposition (2021), M. Hajdu, P. Hozzová, L. Kovács, and A. Voronkov, in Proc. of FMCAD https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
For a survey, also see: Getting Saturated with Induction (2022), M. Hajdu, P. Hozzová, L. Kovács, G. Reger, and A. Voronkov, in Principles of Systems Design https://doi.org/10.1007/978-3-031-22337-2_15
Short Bio:
Andrei Voronkov is Professor of Formal Methods at the University of Manchester and Visiting Professor at Vienna University of Technology. He is best known for the Vampire automated theorem prover, the EasyChair conference management software, the Handbook of Automated Reasoning, and as organiser of the Alan Turing Centenary Conference 2012. In 2015, his contributions to the field of automated reasoning were recognized with the Herbrand Award. He has won 25 division titles in the CADE ATP System Competition (CASC) at the Conference on Automated Deduction (CADE) since 1999.
