张 杰，毛丹雯，关 永，施智平

（1.北京化工大学 信息科学与技术学院，北京100029；2.首都师范大学 信息工程学院，北京100048）

0 引 言

交互式高阶逻辑定理证明系统HOL是由英国剑桥大学开发的一种基于定理证明方法的形式化验证系统，其最新的版本为HOL4。形式化验证是在二十世纪60年代末出现的一种用于系统设计正确性检验的方法，而定理证明方法是形式化验证的传统三种方法之一，近年来在计算机网络协议、安全协议等各类协议，各种硬件电路，以及Viper微处理器、DSP处理器等硬件系统的分析与验证中取得了较为广泛的应用［1－6］。

在定理证明系统中进行形式化验证离不开对定理的形式化证明。HOL4系统中最常用的形式化证明方法是目标制导法，这种方法在使用时很大程度上依赖于一种叫做对策的证明工具的应用，而重写对策是HOL4系统所有对策中极为重要的一类对策。为了更好地在HOL4系统中完成定理的形式化证明，本文对重写对策在基于HOL4系统的形式化证明过程中的应用进行了重点讨论，并以几个典型的重写对策为例，进一步说明如何在HOL4系统中利用重写对策实现证明目标的化简与证明。

1 形式化证明与对策

HOL4系统中定理的形式化证明的实现方法是用户在高层次做引导，而将推理的过程交给系统自动完成［7］。在定理证明系统发展的初期，定理的形式化证明方法为正向证明法。这种方法从欲证定理的假设条件出发，利用系统中的公理、定理和推理规则等逐步推导出欲证定理；……