Correctness of Tableau-Based Decision Procedures with Backjumping
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.