22.10.2010, 14:15: First talk (Building E1 3, Room 528)
You can find the slides here.

7.1.2011, 14:15: Proposal talk (Building E1 3, Room 528)
You can find the slides here.

6.5.2011, 15:15: Final talk (Building E1 3, Room 528)
You can find the slides here.

Abstract

Satallax is an automated theorem prover for higher-order logic. It works by reducing theorem proving to a sequence of SAT problems, which are checked by Minisat for satisfiability. If Satallax is successful in finding a proof, the result is an unsatisfiable set of clauses and a table assigning higher-order formulas to the propositional literals.
In this thesis we will present an algorithm that takes the output of Satallax and generates a tableau refutation as a proof script for the proof management system Coq to check.
The algorithm requires just an UNSAT-core from the set of clauses and uses it to generate a finite tableau calculus in which we will search for a refutation. A formal proof of a refutation's existence in such a calculus will ensure the success of our algorithm.