典型文献
支持索引式的PPTL定理证明器的实现
文献摘要：
定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.
文献关键词：
定理证明;Coq;索引式;命题投影时序逻辑;公理系统
中图分类号：
作者姓名：
王小兵;寇蒙莎;李春奕;赵亮
作者机构：
西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071
文献出处：
引用格式：
[1]王小兵;寇蒙莎;李春奕;赵亮-.支持索引式的PPTL定理证明器的实现)[J].软件学报,2022(06):2172-2188
A类：
索引式,PPTL,命题投影时序逻辑,Coq
B类：
定理证明,明器,形式化验证,验证方法,逻辑表达,表达能力,存在状态,状态空间,空间爆炸,有穷,无穷,全自动化,数学知识,正则,LTL,公理系统,存在证明,冗长,易错,交互式,推理规则,可用性
AB值：
0.22852
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
