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) |
Reprint years | 2004 |
DOI | 10.1023/A:1013886427723 |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
Grafting Modalities Onto Substructural Implication Systems.Marcello D'agostino, Dov M. Gabbay & Alessandra Russo - 1997 - Studia Logica 59 (1):65-102.
Citations of this work BETA
A General Tableau Method for Propositional Interval Temporal Logics: Theory and Implementation.V. Goranko, A. Montanari, P. Sala & G. Sciavicco - 2006 - Journal of Applied Logic 4 (3):305-330.
Theorem Proving for Conditional Logics: CondLean and GOALD U CK.Nicola Olivetti & Gian Luca Pozzato - 2008 - Journal of Applied Non-Classical Logics 18 (4):427-473.
2005 Annual Conference of the Australasian Association for Logic.Hartley Slater - 2006 - Bulletin of Symbolic Logic 12 (3):517-523.
Labelled Modal Tableaux.Guido Governatori - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 87-110.
Similar books and articles
Decidable Fragments of First-Order Modal Logics.Frank Wolter & Michael Zakharyaschev - 2001 - Journal of Symbolic Logic 66 (3):1415-1438.
A Loop-Free Decision Procedure for Modal Propositional Logics K4, S4 and S.Dorota Leszczyńska-Jasion - 2009 - Journal of Philosophical Logic 38 (2):151 - 177.
Systematization of Finite Many-Valued Logics Through the Method of Tableaux.Walter A. Carnielli - 1987 - Journal of Symbolic Logic 52 (2):473-493.
Cut-Free Sequent and Tableau Systems for Propositional Diodorean Modal Logics.Rajeev Goré - 1994 - Studia Logica 53 (3):433 - 457.
Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables.Roman Kontchakov, Agi Kurucz & Michael Zakharyaschev - 2005 - Bulletin of Symbolic Logic 11 (3):428-438.
Ground and Free-Variable Tableaux for Variants of Quantified Modal Logics.Marta Cialdea Mayer & Serenella Cerrito - 2001 - Studia Logica 69 (1):97-131.
Analytics
Added to PP index
2009-01-28
Total views
57 ( #201,627 of 2,520,400 )
Recent downloads (6 months)
1 ( #405,718 of 2,520,400 )
2009-01-28
Total views
57 ( #201,627 of 2,520,400 )
Recent downloads (6 months)
1 ( #405,718 of 2,520,400 )
How can I increase my downloads?
Downloads