支持索引式的PPTL定理证明器的实现

Implementation of Theorem Prover for PPTL with Indexed Expressions

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

Theorem proving is a mainstream formal verification method, with a strong ability of abstraction and logical expression. It does not suffer from state space explosion and can be used to verify finite and infinite systems. Nevertheless, it cannot be fully automated and requires users to have deep mathematical knowledge. Propositional projection temporal logic with indexed expressions is a temporal logic with full regular expressiveness and subsumes LTL, having strong modeling and property describing ability. At present, a sound and complete axiom system for PPTL with indexed expressions is presented while the theorem proving based on it is not yet well supported by tools, which leads to the low automaticity, redundancy, and fallibility of theorem proving. Therefore, firstly, the implementation framework of the theorem prover for PPTL with indexed expressions is designed, including two parts, the formalization of the PPTL axiom system and interactive theorem proving. Then the formulas, axioms, and inference rules are formally defined in Coq, implementing the axiom system of the framework. Finally, the availability of the theorem prover is proved by the interactive proving of two proof examples.