A general tableau method for propositional interval temporal logics: Theory and implementation

Journal of Applied Logic 4 (3):305-330 (2006)
Download Edit this record How to cite View on PhilPapers
Abstract
In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted over partial orders (\nsbcdt\ for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented.
PhilPapers/Archive ID
GORAGT-2
Revision history
Archival date: 2018-04-21
View upload history
References found in this work BETA
Temporalising Tableaux.Kontchakov, Roman; Lutz, Carsten; Wolter, Frank & Zakharyaschev, Michael
Free-Variable Tableaux for Propositional Modal Logics.Beckert, Bernhard & GorÉ, Rajeev

Add more references

Citations of this work BETA
Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions.Bresolin, Davide; Goranko, Valentin; Montanari, Angelo & Sciavicco, Guido
Relational Dual Tableaux for Interval Temporal Logics.Bresolin, David; Golinska-Pilarek, Joanna & Orlowska, Ewa
Back From the Future.Masini, Andrea; ViganĂ², Luca & Volpe, Marco

Add more citations

Added to PP index
2016-06-30

Total views
16 ( #38,488 of 39,921 )

Recent downloads (6 months)
3 ( #39,460 of 39,921 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.