-
题名支持索引式的PPTL定理证明器的实现
- 1
-
-
作者
王小兵
寇蒙莎
李春奕
赵亮
-
机构
西安电子科技大学计算机科学与技术学院
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第6期2172-2188,共17页
-
基金
国家自然科学基金(61672403,61972301)
陕西省重点研发计划(2020GY-043,2020GY-210)。
-
文摘
定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表达能力,并且包含LTL的时序逻辑,具有较强的建模和性质描述能力.目前,一个可靠完备的含索引式的PPTL公理系统已被构建,然而基于该公理系统的定理证明尚未得到良好工具的支持,存在证明自动化程度较低以及证明冗长易错的问题.鉴于此,首先设计了支持索引式的PPTL定理证明器的实现框架,包括公理系统的形式化与交互式定理证明;然后,在Coq中形式化定义了含索引式的PPTL公式、公理与推理规则,完成了框架中公理系统的实现;最后,通过两个实例的交互式证明验证了该定理证明器的可用性.
-
关键词
定理证明
COQ
索引式
命题投影时序逻辑
公理系统
-
Keywords
theorem proving
Coq
indexed expressions
PPTL
axiom system
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
