Studia Logica

Bernhard Beckert, Rajeev Gore

Free-variable semantic tableaux are a well-established technique for
first-order theorem proving where free variables act as a
meta-linguistic device for tracking the eigenvariables used during proof
search. We present the theoretical foundations to extend this technique
to propositional modal logics, including non-trivial rigorous proofs of
soundness and completeness, and also present various techniques that
improve the efficiency of the basic naive method for such tableaux.