A general tableau method for propositional interval temporal logics

Logics for time intervals provide a natural framework for representing and reasoning about timing proper-ties in various 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 temporal logics. In this paper, we introduce a new, very expressive propositional interval temporal logic, called (Non-Strict) Branching CDT (BCDT+) which extends most of the propositional interval temporal logics proposed in the literature. Then, we provide BCDT+ with a generic tableau method which combines features of explicit tableau methods for modal logics with constraint label management and the classical tableau method for first-order logic, and we prove its soundness and completeness.