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.
Thu May 8 21:46:01 2011