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

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