谓词逻辑与模型检验中的计量化理论

项目名称： 谓词逻辑与模型检验中的计量化理论

项目编号： No.11171200

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 数理科学和化学

项目作者： 周红军

作者单位： 陕西师范大学

项目金额： 46万元

中文摘要： 由项目申请人提出的计量逻辑学已经在包括二值命题逻辑和各种多值命题逻辑中形成了较为完整的理论体系，为在各种逻辑系统中展开近似推理奠定了逻辑基础.在表达能力更强的模态逻辑和谓词逻辑中，申请人团队也已开始了初步的研究，并通过随机化和格值化等方法扩展了计量逻辑学的涵盖范围.在此基础上，本项目提出的研究目标是：第一，在一阶谓词逻辑的框架下建立系统的计量逻辑理论，并用于解决Horn子句型数据库相容性的估计问题；第二，线性时态逻辑（LTL）和计算树逻辑（CTL）有比命题逻辑强的表述能力，也是模型检验理论用来表述规范（Specification）的主要工具.值得注意的是，满足给定规范的迁移系统并不唯一，如何寻求极小的迁移系统以降低计算复杂度有重要意义.本项目将在上述两种时态逻辑中建立起计量化理论，提出一个迁移系统对于给定规范的满足度和冗余度概念，最终找出满足给定规范的最佳迁移系统 。

中文关键词： 谓词逻辑；模型检验；计量逻辑；不确定性推理；

英文摘要：

英文关键词： Predicate logic；Model checking；Quantitative logic；Uncertainty reasoning；