广义可能性计算树逻辑的两种范式

摘要：

计算树逻辑的范式在模型检测方法中具有重要意义.但广义可能性计算树逻辑的范式尚未有系统研究.在广义可能性计算树逻辑理论的基础上,本文给出了广义可能性计算树逻辑的两种不同的范式PNF(Positive Normal Form)和ENF(Existential Normal Form),并利用归纳假设法证明了任意的广义可能性计算树逻辑公式都有与之等价的PNF公式和ENF公式.

关键词： 计算树逻辑 PNF范式 ENF范式 模型检测

作者: 赵杰 李永明

作者单位: 陕西师范大学计算机科学学院,陕西省西安市710019

会议类型: 国内会议

会议名称: 2015全国理论计算机科学学术年会

会议地点: 金华

会议语种:中文

页码: 1-9

在线出版日期: 2015-10-30（万方平台首次上网日期，不代表论文的发表时间）