A Simple Propositional S5 Tableau System

9 years 2 months ago
A Simple Propositional S5 Tableau System
We give a sound and complete propositional S5 tableau system of a particularly simple sort, having an easy completeness proof. It sheds light on why the satisfiability problem for S5 is less complex than that for most other propositional modal logics. We believe the system remains complete when quantifier rules are added. If so, it would allow us to get partway to an interpolation theorem for first-order S5, a theorem that is known to fail in general.
Melvin Fitting
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 1999
Where APAL
Authors Melvin Fitting
Comments (0)