基于Isabelle的证明信息系统设计.docx
《基于Isabelle的证明信息系统设计.docx》由会员分享,可在线阅读,更多相关《基于Isabelle的证明信息系统设计.docx(12页珍藏版)》请在咨信网上搜索。
1、基于Isabelle的证明信息系统设计摘 要 Isabelle定理证明器中的证明步骤和证明状态是非常具有参考价值的证明信息。然而目前没有工具可以有效管理这些信息。本文给出一个基于Isabelle的信息系统设计方案。利用该系统的实现,用户可以提取、保存和搜索这两种证明信息。关键词 定理证明;证明信息;Isabelle;关系数据库 【Abstract】 Proof steps and proof states in the theorem prover Isabelle are very referable proof information , but now there is no tool
2、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 Data
3、base 1 引言 Isabelle1是一种着名的交互式定理证明器,目前已被应用于数学形式化、逻辑研究、计算机软、硬件以及安全协议的验证等多个领域。使用Isabelle时面临的主要困难是编写定理的证明过程,这一般需要专家级的用户才能完成,这也因此限制了Isabelle进一步的普及。 Isabelle包含许多有重要参考价值的证明信息,例如含有证明方法的证明步骤,反映当前证明形势和效果的证明状态 (proof state)。这些信息都有助于用户开发新的证明文档,然而目前Isabelle并不提供查询这些信息的功能。 目前已经出现了一些专门为Isabelle构建信息数据库方面的工作与研究。Suzuki
4、为Isabelle建立了一个证明状态数据库,但其中的数据来源于Isabelle的显示,包含的信息较少且数据的提取比较受限。另外,网络上存在一个Isabelle的理论文件(theory file)库,其中收集了大量的在不同领域应用Isabelle开发的证明脚本。要浏览这些文档的具体证明过程,必须用Isabelle载入并执行文档。这一过程是比较耗时并且需要用户具有运行Isabelle的环境。 本文提出了一个证明信息系统。该系统以关系数据库为基础,并提供可分别提取证明步骤和证明状态的工具,目标是为用户提供一个简易的证明信息搜索平台。该系统面向的用户主要是用Isabelle来编写证明文档的专家,也可被
5、一般用户用来作为学习了解Isabelle证明过程以及一般数学逻辑知识理论的一个工具。 2 Isabelle Isabelle采用的编程语言是函数式编程语言ML。Isar是Isabelle中专门用于书写证明过程的语言,用这种语言编写的证明脚本具有一定的可读性。 以下是与Isabelle相关的重要术语及其定义: 证明脚本:为了证明定理而由用户用Isar语言编写的证明文本。 证明行:一行证明脚本。 理论文件:主要是为证明某一个理论中部分或所有定理编写的证明脚本文件。除定理及其证明之外,文件中还有相关的常数和操作符定义、注释等。 证明步骤:完成一步证明的证明脚本。定理的所有证明步骤组成一个定理的完整证
6、明脚本。以下是HOL中与函数相关的理论文件中的引理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后面的语句表示应用的具体证明策略入规则、方法等。 证明状态:证明时产生的状态,主要信息是当前剩余
7、的子目标。图1是证明引理expand_fun_eq时执行到第1步时的证明状态显示。图1 Isabelle的证明状态显示 由上图可知,原引理已被化成两个子目标并等待下一步的证明。 3 系统设计 该信息系统的设计目标是利用Isabelle提取证明步骤和证明状态,并用标准的数据库技术加以处理,为用户提供一个网络界面可以迅速查找和浏览这两种证明信息。 结构设计 按照系统数据处理和功能的相关性,可以将此系统分为3个模块: 提取界面、数据库和搜索界面,如图2所示:图2:系统模型 其中,提取界面用于提取所需数据;数据库用来存储提取来的纪录数据;搜索界面用于客户端对数据库的访问。 系统的工作流程为:首先,用I
8、sabelle载入理论文件并启动证明过程。这时Isabelle会按从上到下的顺序对文件中的每个定理进行证明,可逐步进行,也可成批处理。无论是用何种方式,都可用提取界面提取所有的证明步骤和历史证明状态数据。将二者的记录数据插入到数据库后,便可以在客户端利用搜索界面访问数据库,从而最终实现对这两种信息的查找。 根据上面介绍的结构模型及其工作流程,此系统的设计可分为三个部分:提取界面设计、数据库设计及搜索界面的设计。提取界面设计按照提取数据的种类,此界面可进行: 证明步骤提取 要从理论文件中提取出每一个证明步骤,可以利用以下算法,共有六个步骤:1) 去注释:注释可以位于理论文件的任何位置,形式为并可
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 Isabelle 证明 信息系统 设计
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【天****】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【天****】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。