Publication details

Saarland University Computer Science

Correctness of Tableau-Based Decision Procedures with Backjumping

Tobias Tebbi

B.Sc. Thesis, Programming Systems Lab, Department of Informatics, Saarland University, April 2011

Implementations of tableau-based decision procedures often use an optimization called backjumping. The goal of this thesis is to prove the correctness of the backjumping optimization. To do so, we define an abstract class of terminating tableau systems and show the correctness of a concomitant decision procedure performing depth-first search with backjumping. Based on this framework we obtain the correctness of a backjumping decision procedure for modal logic. To the best of our knowledge, this is the first rigorous correctness proof for such a procedure.

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy