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

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

谓词逻辑以及模型检验都具有比命题逻辑更强的表达能力，是人工智能领域中的核心研究课题之一。基于赋值集上的均匀概率测度建立的命题逻辑的计量化理论是本项目申请时概率与逻辑交叉领域中具有代表性的研究成果。本项目以提高命题型计量逻辑的语言表达能力和逻辑推理能力为出发点，将在命题逻辑框架下成功建立起的计量化方法推广到一阶谓词逻辑，线性时态逻辑及计算树逻辑中，利用有限模型上的均匀概率测度建立相应的计量逻辑理论。首先，在不含函数符号的一阶谓词逻辑中，建立了系统的公理化真度理论；证明了该真度相对于解释域的独立性和可计算性；讨论了全体真度值在单位闭区间[0,1]中的分布；引入了公式之间相似度和伪距离的计算方法；提出了逻辑形式理论的相容度理论；特别是证明了逻辑闭公式的真度之集与二值命题逻辑中的计算结果相一致,并且所有闭文字的真度都等于1/2；作为应用，给出了估计Horn 子句型数据库相容度的一种方法；在更为精细的指标下讨论了三 I 算法的鲁棒性，从而较为系统地构建了谓词逻辑的计量化理论。其次，针对若干重要的谓词逻辑片段，建立了模态逻辑和线性时态逻辑的满足度理论；研究了其逻辑公式的范式表示和计数问题，指出存在特征的LTL公式在模型检验中总可以在有限步内判断其有效性，即使相应的迁移系统含有无限多个状态也是如此；构造了线性时序逻辑基于DTMC的计量化方法；更进一步将计量逻辑中的逻辑度量空间方法推广到模糊集上，为模糊推理建立了逻辑基础，从而较细致地建立了模型检验的计量化理论。.本项目已顺利完成当初拟定的研究计划，项目组在科学出版社出版专著1部，系统总结和论述了命题型计量逻辑的概率随机化及其应用方面的研究成果；正式发表标注该基金资助的研究论文32篇，其中SCI收录8篇，EI收录4篇，会议论文6篇。项目组成员1人晋升教授职称，3人晋升副教授或副研究员，1人考取博士，目前在读；培养博士生4人(含新招收博士2人)，其中3人已取得博士学位，1人已通过博士答辩，学位正在公示中。