软件学报

作者：王小兵，寇蒙莎，李春奕，赵亮

单位：王小兵，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007111,寇蒙莎，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007102,李春奕，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007103,赵亮，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007104

关键词：定理证明;Coq;索引式;命题投影时序逻辑;公理系统

基金：国家自然科学基金(61672403,61972301);陕西省重点研发计划(2020GY-043,2020GY-210)

定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.

来源：2022年第6期

《软件学报》期刊编辑部

查看软件学报杂志2022年第6期