Design of a Tableau-Based Automated Theorem Prover and Output of Machine-Checkable Proofs


Event details

Date 23.02.2024
Hour 10:3011:30
Location Online
Category Conferences - Seminars
Event Language English

By Julie Cailler, postdoctoral researcher in the University of Regensburg and main author of the Goéland theorem prover

Description: Automated deduction is the use of computer programs to automatically prove mathematical theorems. It can be used to detect bugs in critical systems, or to help demonstrate mathematical proofs. This talk focuses on the presentation of Goéland, a concurrent tableau-based automated theorem prover, and the main challenges it faces. These challenges include the implementation of a fair tableau-based proof search procedure in first-order logic, the handling of theory reasoning (equality, set theory, etc.), and the generation of machine-checkable proofs, i.e., proofs that can be verified by external tools (Coq, Lambdapi).

More information

Practical information

  • General public
  • Free


  • Simon Guilloud

Event broadcasted in