Cut-free sequent and tableau systems for propositional diodorean modal logics
Studia Logica 53 (3):433 - 457 (1994)
| Abstract | We present sound, (weakly) complete and cut-free tableau systems for the propositional normal modal logicsS4.3, S4.3.1 andS4.14. When the modality is given a temporal interpretation, these logics respectively model time as a linear dense sequence of points; as a linear discrete sequence of points; and as a branching tree where each branch is a linear discrete sequence of points.Although cut-free, the last two systems do not possess the subformula property. But for any given finite set of formulaeX the superformulae involved are always bounded by a finite set of formulaeX* L depending only onX and the logicL. Thus each system gives a nondeterministic decision procedure for the logic in question. The completeness proofs yield deterministic decision procedures for each logic because each proof is constructive. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,653 |
| External links |
|
| Through your library | Configure |
Melvin Fitting (1995). Tableaus for Many-Valued Modal Logic. Studia Logica 55 (1):63 - 87.
Brian Hill & Francesca Poggiolesi (2010). A Contraction-Free and Cut-Free Sequent Calculus for Propositional Dynamic Logic. Studia Logica 94 (1).
Gerald J. Massey (1965). Four Simple Systems of Modal Propositional Logic. Philosophy of Science 32 (3/4):342-355.
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.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Mauro Ferrari (1997). Cut-Free Tableau Calculi for Some Intuitionistic Modal Logics. Studia Logica 59 (3):303-330.
Linh Anh Nguyen (2001). Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD. Studia Logica 69 (1):41-57.
Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.
Monthly downloads |
Added to index2009-01-28Total downloads7 ( #133,343 of 548,984 )Recent downloads (6 months)1 ( #63,327 of 548,984 )How can I increase my downloads? |

