A Tableau Proof System with Names for Modal Mu-calculus
A Tableau Proof System with Names for Modal Mu-calculus
复制标题
具有模态 Mu 演算名称的 Tableau 证明系统
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
C. Stirling
中科院分区：
文献类型：
--
作者：
C. Stirling
霍华德·巴林杰（Howard Barringer）是研究具有不动点的时间逻辑的先驱。它们的加入增加了相当大的表现力。一个普遍的问题是如何为这样的逻辑定义证明系统。这里我们研究具有不动点的模态逻辑的证明系统。我们提出了一个表格证明系统来检查公式的有效性，该系统使用名称来跟踪[8]中设计的不动点变量的展开。
Howard Barringer was a pioneer in the study of temporal logics with fixpoints [1]. Their addition adds considerable expressive power. One general issue is how to define proof systems for such logics. Here we examine proof systems for modal logic with fixpoints. We present a tableau proof system for checking validity of formulas which uses names to keep track of unfoldings of fixpoint variables as devised in [8].