基于Isabelle的证明信息系统设计(1)(2)
2014-10-26 01:26
导读：图1 Isabelle的证明状态显示 由上图可知，原引理已被化成两个子目标并等待下一步的证明。 3 系统设计 该信息系统的设计目标是利用Isabelle提取证明步骤和
图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步可以记在一个证明行中：共2页: 1 [2] 下一页 论文出处(作者):
（科教论文网 Lw.nsEAc.com编辑整理） 系统发生足迹技术在巴西固氮螺菌基因组特征搜寻上的应用
基于隐式反馈的个性化信息过滤方法
