Laura Kovács

"Getting Saturated with Induction"

We describe extensions to first-order theorem proving in support of automating inductive reasoning. We integrate induction directly into saturation-based proof search. We do so by turning applications of induction into inference rules of the saturation process and adding instances of appropriate induction schemata. Our inference rules capture the application of induction to inductive formulas to be proved. However, this is insufficient for efficient theorem proving. Modern saturation-based theorem provers are very powerful not just because of the logical calculi they are based on, such as superposition. What makes them powerful and efficient are (i) redundancy criteria and pruning search space, (ii) strategies for directing proof search, mainly by clause and inference selection, and recent results on (iii) theory-specific reasoning, for example with inductive data types. We overview our recent efforts in bringing induction in saturation, in particular in generalizing inductive formulas and handling recursive functions.

Bio: Laura Kovacs is a full professor in 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 anda Wallenberg Academy Fellow of Sweden. Her research has also been awarded with a ERC Starting Grant 2014, an ERC Proof of Concept Grant 2018 and an ERC Consolidator Grant 2020.

Termin als Datei downloaden und in den Kalender importieren.