Andreas Teucke: Bachelor's Thesis: Translating a Satallax Refutation to a Tableau Refutation Encoded in Coq

Andreas Teucke: Bachelor's Thesis: Translating a Satallax Refutation to a Tableau Refutation Encoded in Coq

Saarland University Computer Science
Author: Andreas Teucke
Advisor: Chad E. Brown
Supervisor: Gert Smolka

Current State

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.

Downloads

Thesis

You can find the finished thesis here.


Andreas Teucke, Thu May 8 21:46:01 2011