Date: Thursday, March 14th 2024 – 13h00
Place: visio
Title: Conception d’un prouveur automatique basé sur les tableaux analytiques et production de preuves vérifiables La déduction automatique est l’utilisation de programmes informatique afin d’automatiquement prouver des théorèmes mathématiques. Elle trouve son intérêt dans la détection de bogues au sein de systèmes critiques ou encore dans l’aide à la démonstration de preuves mathématiques. Cet exposé se concentre sur la présentation de Goéland, un prouveur de théorèmes automatique concurrent, et sur les principaux défis qu’il rencontre. Ces défis incluent l’implémentation d’une procédure de recherche de preuves équitable basée sur la méthode des tableaux en logique du premier ordre, la prise en compte du raisonnement au sein des certaines théories (l’égalité, la théorie des ensembles, etc), ainsi que la génération de preuves vérifiables par des outils externes (Coq, Lambdapi).
