Kovács, L., Hozzová, P., Hajdu, M., & Voronkov, A. (2024). Induction in Saturation. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 21–29). Springer. https://doi.org/10.1007/978-3-031-63498-7_2
Proof by induction is commonplace in modern mathematics and computational logic. This paper overviews and discusses our recent results in turning saturation-based first-order theorem proving into a powerful framework for automating inductive reasoning. We formalize applications of induction as new inference rules of the saturation process, add instances of appropriate induction schemata to the search space, and use these rules and instances immediately upon their addition for the purpose of guiding induction. Our results show, for example, that many problems from formal verification and mathematical theories can now be solved completely automatically using a first-order theorem prover.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds)
CC BY 4.0
