关键词 定理证明；证明信息；Isabelle；关系数据库
【Abstract】 Proof steps and proof states in the theorem prover Isabelle are very referable proof information ， but now there is no tool that can manage them efficiently. This paper presents a design of a proof information system based on Isabelle. By using an implementation of the system， users can extract， save and search for the two kinds of proof information.
【Key words】Theorem Proving；Proof Information; Isabelle; Relational Database
Isabelle[1]是一种著名的交互式定理证明器，目前已被应用于数学形式化、逻辑研究、计算机软、硬件以及安全协议的验证等多个领域。使用Isabelle时面临的主要困难是编写定理的证明过程，这一般需要专家级的用户才能完成，这也因此限制了Isabelle进一步的普及。
Isabelle包含许多有重要参考价值的证明信息，例如含有证明方法的证明步骤（proof step），反映当前证明形势和效果的证明状态 (proof state)。这些信息都有助于用户开发新的证明文档，然而目前Isabelle并不提供查询这些信息的功能。
目前已经出现了一些专门为Isabelle构建信息数据库方面的工作与研究。Suzuki[2]为Isabelle建立了一个证明状态数据库，但其中的数据来源于Isabelle的显示，包含的信息较少且数据的提取比较受限。另外，网络上存在一个Isabelle的理论文件(theory file)库[3]，其中收集了大量的在不同领域应用Isabelle开发的证明脚本。要浏览这些文档的具体证明过程，必须用Isabelle载入并执行文档。这一过程是比较耗时并且需要用户具有运行Isabelle的环境。
本文提出了一个证明信息系统。该系统以关系数据库为基础，并提供可分别提取证明步骤和证明状态的工具，目标是为用户提供一个简易的证明信息搜索平台。该系统面向的用户主要是用Isabelle来编写证明文档的专家，也可被一般用户用来作为学习了解Isabelle证明过程以及一般数学逻辑知识理论的一个工具。
2 Isabelle
Isabelle采用的编程语言是函数式编程语言ML[4]（Meta Language）。Isar是Isabelle中专门用于书写证明过程的语言，用这种语言编写的证明脚本具有一定的可读性。
以下是与Isabelle相关的重要术语及其定义:
（1）证明脚本：为了证明定理而由用户用Isar语言编写的证明文本。
（2）证明行：一行证明脚本。
（2）理论文件：主要是为证明某一个理论中部分或所有定理编写的证明脚本文件。除定理及其证明之外，文件中还有相关的常数和操作符定义、注释等。
（3）证明步骤：完成一步证明的证明脚本。定理的所有证明步骤组成一个定理的完整证明脚本。以下是HOL（高阶逻辑）中与函数相关的理论文件Fun.thy中的引理expand_fun_eq的证明步骤：
0) lemma expand_fun_eq: “f = g” = (! X. f(x) = g(x))”
1) apply (rule iffI)
2) apply (simp (no_asm_simp))
3) apply (rule ext， simp (no_asm_simp))
4) done
其中，apply和done是Isabelle的两个证明关键字，apply表示应用；done表示结束当前证明；apply后面的语句表示应用的具体证明策略入规则、方法等。
（4）证明状态：证明时产生的状态，主要信息是当前剩余的子目标。图1是证明引理expand_fun_eq时执行到第1步时的证明状态显示。
图1 Isabelle的证明状态显示
由上图可知，原引理已被化成两个子目标并等待下一步的证明。
3 系统设计
该信息系统的设计目标是利用Isabelle提取证明步骤和证明状态，并用标准的数据库技术加以处理，为用户提供一个网络界面可以迅速查找和浏览这两种证明信息。
3.1 结构设计
按照系统数据处理和功能的相关性，可以将此系统分为3个模块: 提取界面、数据库和搜索界面，如图2所示：
图2：系统模型
其中，提取界面用于提取所需数据；数据库用来存储提取来的纪录数据；搜索界面用于客户端对数据库的访问。
系统的工作流程为：首先，用Isabelle载入理论文件并启动证明过程。这时Isabelle会按从上到下的顺序对文件中的每个定理进行证明，可逐步进行，也可成批处理。无论是用何种方式，都可用提取界面提取所有的证明步骤和历史证明状态数据。将二者的记录数据插入到数据库后，便可以在客户端利用搜索界面访问数据库，从而最终实现对这两种信息的查找。
根据上面介绍的结构模型及其工作流程，此系统的设计可分为三个部分：提取界面设计、数据库设计及搜索界面的设计。
3.2 提取界面设计
按照提取数据的种类，此界面可进行：
（1） 证明步骤提取
要从理论文件中提取出每一个证明步骤，可以利用以下算法，共有六个步骤：
1） 去注释：注释可以位于理论文件的任何位置，形式为（*… *）并可以嵌套使用。去除这些注释的目的是避免它们对提取过程造成干扰，因为注释中和证明关键字相同的词语很容易被误认为是证明步骤的开始而导致证明步骤的错误识别；
2） 证明行获取：按字符串行来分离去注释后的证明文档，得一长的证明行序列；
3） 分块：按照证明行所属的定理将2）中得到的长序列分成多个子序列，其中可能会涉及到步骤分离的操作；
4） 步骤连接：在每一个字序列中处理多行长步的情况。多行长步是指一个占用了两个或更多证明行的长的证明步骤。所谓的连接就是将这种证明行连成一个完整证明步骤字符串。完成此步，每个子序列就可以正确包含一个定理的所有证明步骤；
5） 结果输出：每一个证明步骤连同理论名，步骤序号、所在定理名作成记录，一同输出到文件。
此算法中第3步中的步骤分离用于处理一行多步的情况。一行多步指的是一行语句中含有2 个或多个证明步骤。例如，引理expand_fun_eq的第1步和第2步可以记在一个证明行中：