Colloquium du Loria : Laura Kovács
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.
