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

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of applied logic 2006-09, Vol.4 (3), p.305-330
Main Authors: Goranko, V., Montanari, A., Sala, P., Sciavicco, G.
Format: Article
Language:English
Subjects:
Interval temporal logics
Proof systems
Tableau methods
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 ( BCDT + 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.
ISSN:1570-8683
1570-8691
DOI:10.1016/j.jal.2005.06.012