A Tableau for Bundled CTL
A Tableau for Bundled CTL
复制标题
捆绑 CTL 的 Tableau
DOI：
--
复制
发表时间：
2006
影响因子：
0.7
通讯作者：
Mark Reynolds
中科院分区：
文献类型：
--
作者：
Mark Reynolds
我们提出了一个健全、完整和相对简单的表法来确定命题版本的捆绑（或后缀和融合封闭）计算树逻辑BCTL*的有效公式。这证明了BCTL*是可决定的。对于具有合理表达能力的分支时间时态逻辑来说，有一个可用的图表也是适度有用的。然而，主要的兴趣应该是，它使我们更接近于能够在重要的全计算树逻辑CTL*中设计一种基于表的定理证明技术。
We present a sound, complete and relatively straightforward tableau method for deciding valid formulas in the propositional version of the bundled (or suffix and fusion closed) computation tree logic BCTL*. This proves that BCTL* is decidable. It is also moderately useful to have a tableau available for a reasonably expressive branchingtime temporal logic. However, the main interest in this should be that it leads us closer to being able to devise a tableau-based technique for theorem-proving in the important full computational tree logic CTL*.