Free Variable Tableaux for Propositional Modal Logics

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.

• Type: Conference
• Year: 1997
• Where: TABLEAUX
• Authors: Bernhard Beckert, Rajeev Goré
• Keywords: Artificial Intelligence, Free-variable Semantic Tableaux, Non-trivial Rigorous Proofs, Propositional Modal Logics, TABLEAUX 1997