Cut-free sequent and tableau systems for propositional Diodorean modal logics |
| |
Authors: | Rajeev Goré |
| |
Affiliation: | (1) Department of Computer Science, University of Manchester, M13 9PL Manchester, England |
| |
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.Each tableau system has a cut-free sequent analogue proving that Gentzen's cut-elimination theorem holds for these latter systems. The techniques are due to Hintikka and Rautenberg.Presented byDov M. Gabbay |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|