Induction in saturation-based first-order theorem proving is a new exciting
direction in the automation of inductive reasoning. In this talk, I describe our recent results on integrating induction directly into saturation. We do so by turning applications of induction into inference rules of the saturation process and
adding instances of appropriate induction schemata. We propose additional reasoning methods for strengthening inductive reasoning, as well as for handling recursive function definitions. Our work is implemented within the Vampire prover and our experimental results demonstrate the practical impact of our work.
The work described in this talk is based on joint work with Marton Hajdu (TU Wien), Petra Hozzova (TU Wien), Giles Reger (Amazon), and Andrei Voronkov (U. Manchester, EasyChair, and TU Wien).
BIO: Laura Kovacs is a full professor of computer science at the TU Wien, leading the automated program reasoning (APRe) group of the Formal Methods in Systems Engineering division. Her research focuses on the design and development of new theories, technologies, and tools for program analysis, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She is the co-developer of the Vampire theorem prover and a Wallenberg Academy Fellow of Sweden. Her research has also been awarded with a ERC Starting Grant 2014, an ERC Proof of Concept Grant 2018, an ERC Consolidator Grant 2020, and an Amazon Research Award 2020.
Web: lkovacs.com
Copyright. All Rights Reserved.