A general tableau method for propositional interval temporal logics: theory and implementation (Q2506829)

Propositional interval temporal logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. The authors develop a general tableau method for Venema's CDT logic interpreted over partial orders, called non-strict branching CDT, and denoted by BCDT\(^+\). As it is interpreted over partial orders, it is expressive enough to include as subsystems a number of well-known approaches to propositional interval logics. After introducing the syntax and semantics of BCDT\(^+\), its expressive power is compared with that of the main propositional interval logics. Then, a survey of existing tableau methods is presented, followed by the proposed method, which is proved to be sound and complete. The method combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management. Contrarily to other existing tableau methods, the proposed method is only a semi-decision procedure for unsatisfiability. Finally, the description of the most relevant features of an implementation in C of the method concludes the paper.