Paraconsistent computation tree logic
Paraconsistent computation tree logic
复制标题
并行一致计算树逻辑
DOI：
10.1007/s00354-009-0116-6
复制
发表时间：
2011
影响因子：
2.6
通讯作者：
Norihiro Kamide
中科院分区：
文献类型：
--
作者：
Ken Kaneiwa;Norihiro Kamide
亚协调逻辑系统比其他类型的逻辑系统更适合于不一致容忍和不确定性推理。本文通过在标准计算树逻辑CTL的基础上增加次协调否定，得到了一种次协调计算树逻辑PCTL。PCTL可以用来适当地形式化不一致容忍时态推理。证明了将PCTL嵌入CTL的一个定理。PCTL的有效性，可满足性和模型检查问题被证明是可判定的。嵌入和可判定性的结果表明，我们可以重用现有的基于CTL的算法的有效性，可满足性和模型检查。一个说明性的例子，涉及使用PCTL的医学推理。
It is known that paraconsistent logical systems are more appropriate for inconsistency-tolerant and uncertainty reasoning than other types of logical systems. In this paper, a paraconsistent computation tree logic, PCTL, is obtained by adding paraconsistent negation to the standard computation tree logic CTL. PCTL can be used to appropriately formalize inconsistency-tolerant temporal reasoning. A theorem for embedding PCTL into CTL is proved. The validity, satisfiability, and model-checking problems of PCTL are shown to be decidable. The embedding and decidability results indicate that we can reuse the existing CTL-based algorithms for validity, satisfiability, and model-checking. An illustrative example of medical reasoning involving the use of PCTL is presented.