Colloquium du Loria : Laura Kovács
The Loria is proud to announce a colloquium presentation by Laura Kovács on
Induction and synthesis in saturation-based theorem proving.
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 22nd.
——————————————————————————–
Les membres du Loria sont fiers d’accueillir Laura Kovács, qui présentera un exposé intitulé :
Induction and synthesis in saturation-based theorem proving.
Laura Kovács, professeure à la Faculté d’Informatique de l’Université de Technologie de Vienne (Autriche), est une chercheuse de premier plan dans le domaine du raisonnement automatisé et du calcul symbolique.
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 22 janvier.
