Le Loria est extrêmement fier d’accueillir Laura Kovács, figure majeure de la recherche dans le domaine du raisonnement automatisé et du calcul symbolique et professeure à la Faculté d’Informatique de l’Université de Technologie de Vienne (Autriche).

Ce lundi 26 janvier 2026 à 11:00, Laura Kovács présentera un exposé en anglais intitulé :
« Induction and synthesis in saturation-based theorem proving ».

Résumé :

La démonstration par induction est courante en mathématiques, en logique, en vérification formelle, en cybersécurité et dans de nombreux autres domaines. Cette conférence présente les progrès récents en matière d’automatisation du raisonnement inductif dans la démonstration de théorèmes du premier ordre par saturation. Nous formalisons les applications de l’induction sous forme de nouvelles règles d’inférence du processus de saturation, ajoutons des instances de schémas d’induction appropriés à l’espace de recherche et utilisons ces règles et instances dès leur ajout afin de guider l’induction. Nous synthétisons également du code qui satisfait une spécification logique (inductive) donnée, tout en démontrant cette spécification dans un cadre basé sur la saturation.

Les personnes extérieures au Loria doivent s’inscrire en envoyant un mail à Annabelle Chapron  –  annabelle.chapron (at) loria.fr  –  avant le 25 janvier.
Les visiteurs devront se munir de leur pièce d’identité.

Laura Kovács is a professor at the Faculty of Informatics of Vienna University of Technology (Vienna, Austria) and a leading researcher in the field of automated reasoning and symbolic computation.

Abstract:
Proof by induction is commonplace in mathematics. logic, formal verification, cybersecurity, and many more areas. This talk overviews recent progress in automating inductive reasoning in saturation-based first-order theorem proving 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. We also synthesize code that satisfies a given (inductive) logical specification, while proving the specification in a saturation-based framework.

People from outside the Loria must register by sending an email to Annabelle Chapron  –  annabelle.chapron (at) loria.fr  –  before January 25th.
Les visiteurs devront se munir de leur pièce d’identité.