Studia Logica 69 (1):59-96 (2001)
|Abstract||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|
|Keywords||automated deduction modal logics modal theorem proving free-variable tableaux|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Frank Wolter & Michael Zakharyaschev (2001). Decidable Fragments of First-Order Modal Logics. Journal of Symbolic Logic 66 (3):1415-1438.
Roman Kontchakov, Agi Kurucz & Michael Zakharyaschev (2005). Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables. Bulletin of Symbolic Logic 11 (3):428-438.
Dorota Leszczyńska-Jasion (2008). The Method of Socratic Proofs for Modal Propositional Logics: K5, S4.2, S4.3, S4f, S4r, S4m and G. Studia Logica 89 (3):365 - 399.
Rajeev Goré (1994). Cut-Free Sequent and Tableau Systems for Propositional Diodorean Modal Logics. Studia Logica 53 (3):433 - 457.
Walter A. Carnielli (1987). Systematization of Finite Many-Valued Logics Through the Method of Tableaux. Journal of Symbolic Logic 52 (2):473-493.
Dorota Leszczyńska-Jasion (2009). A Loop-Free Decision Procedure for Modal Propositional Logics K4, S4 and S. Journal of Philosophical Logic 38 (2):151 - 177.
Added to index2009-01-28
Total downloads9 ( #122,297 of 722,700 )
Recent downloads (6 months)0
How can I increase my downloads?