命题投影时序逻辑的判定性和表达性

论文摘要

本文在研究了命题投影时序逻辑PPTL(Propositional Projection Temporal Logic)的语义和语法的基础上,详细阐述了它的判定过程和表达性。首先介绍了命题投影时序逻辑,包括基本的语法、语义和一些派生公式及常用逻辑等式,该逻辑除了包含有常用的逻辑操作符∨(或)和?(非)外,还包含了两个时序操作符○(next)和prj(投影操作符)。其次,本文定义了命题投影时序逻辑公式的正则形(normal form),根据公式的结构采用归纳的方法证明了任意PPTL公式都可以转换为正则形定理的正确性并且给出了相应的转换算法。该算法将所有逻辑公式都归结为一种统一的形式,这是采用Tableau方法进行判定的前提和基础。再次,为了找到给定公式的模型,本文介绍了正则图(normal form graph)的概念,给出了为PPTL公式构造正则图的算法和命题投影时序逻辑的判定过程,该方法简单实用。最后,本文介绍和比较了区间时序逻辑中两个版本的投影结构并研究了这两个投影结构的表达性,结果表明prj投影结构比原始的投影结构proj的表达性更强。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 引言
• 1.2 时序逻辑
• 1.3 相关工作
• 1.4 论文的研究意义和目的
• 1.5 论文的主要工作
• 第二章 命题投影时序逻辑
• 2.1 语法
• 2.2 语义
• 2.2.1 状态
• 2.2.2 区间
• 2.2.3 解释
• 2.3 联结词的扩充
• 2.4 可满足性和有效性
• 2.4.1 可满足性和有效性
• 2.4.2 特殊模型
• 2.5 优先级
• 2.6 逻辑定理
• 2.7 本章小结
• 第三章 命题投影时序逻辑的正则形
• 3.1 命题投影时序逻辑的正则形
• 3.2 命题投影时序逻辑公式转换为正则形的算法
• 3.3 本章小结
• 第四章 命题投影时序逻辑的可判定性
• 4.1 正则图
• 4.2 判定算法
• 4.3 判定算法优越性的讨论和比较
• 4.4 本章小结
• 第五章 命题投影时序逻辑的表达性
• 5.1 两个投影结构
• 5.1.1 投影结构prj
• 5.1.2 投影结构proj
• 5.2 两个投影结构的比较
• 5.2.1 使用新投影结构prj 表示原始投影结构proj
• 5.2.2 使用投影结构proj 和chop 结构;来推导投影结构prj
• 5.2.3 投影结构proj 和chop 结构的关系
• 5.3 本章小结
• 第六章 结论
• 6.1 总结
• 6.2 展望
• 致谢
• 参考文献
• 作者在读期间的研究成果