理论计算机科学电子笔记103（2004）121-138www.elsevier.com/locate/entcs着色证明：一种为证明添加形式结构的轻量级方法LaurentT h'ery1Dipartimento diInformaticaUniversit`adiL摘要在本文中，我们提出了一个证明格式写正式的证明动机的形式化的浮点数。这种校样格式的目的是要充分的证明和机械化的校对。我们还提出了一个简单的图形界面来支持这种证明格式。关键词：机械化校对，校对演示，XML1介绍本文中的工作来自于长期合作[8]，应用定理证明技术来机械地验证新的浮点数算法。在计算机算术界，研究人员经常发表他们新算法正确性的详细证明。大多数时候，这些证明是错综复杂的，需要大量的繁琐检查，为持怀疑态度的读者。这种证明的一个例子是[10]中给出的19页证明。开创性的工作[14，19，22]已经展示了有效的定理证明系统如何在我们的例子中，证明在CO q证明器中被编码和形式化验证[15]。在像CO q这样的系统中，证明是由证明脚本表示的。脚本由一组称为策略的基本命令组成策略指导证明者寻找形式证明。在这方面，证明脚本与通常的纸上证明非常不同1Email：Laurent. Ther@ di. 我问你。It1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.07.002122L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121我们在CO q中机械地检查证明的工作方式从一开始就几乎保持不变证明首先要仔细地写然后，将此文档用作生成证明系统脚本的指南。在这个阶段，纸上的证明和脚本通常采取不同的道路。在纸上的证明是重新加工，主要是缩短，以便插入到一些技术报告。剧本也被修改了。良好的实践建议重新组织它，以提高可重用性和健壮性。在已发布的证明和它的证明脚本之间没有直接联系的事实至少有三个令人不快的后果。首先，发表的证明不能声称已经被机械地检查过了。所检验的是证明的结论成立。例如，没有什么可以确保发布的证明不包含错误。基本错误最有可能在检查过程中被发现。尽管如此，在发表的证明中有一个微小的错误是非常令人讨厌的，特别是当论文的主要主张是所有的结果都经过了机械检查时。第二个后果是，出版的证明是有限的利益，以维持正式的发展。由于证明器在不断发展，保持脚本最新是一个真正的问题。已发布的证明很少说明相应的证明脚本是如何构造的。能够快速找出脚本的特定子部分应该做什么是维护脚本时真正需要的。与第二个后果密切相关的第三个后果是缺乏灵活性。通常的情况是，当某些东西在特定的假设下得到证明时，人们希望看到稍微修改它们的效果。通常在浮点运算中，可以尝试更改运算的基数或舍入模式。用机械化的证明做这样的实验是非常简单的。人们只需要改变假设并修改脚本。当策略的应用失败时，证明不再有效的事实被检测到。在纸上证明中找出相应的步骤不是立即的，需要一些不平凡的专业知识。在本文中，我们提出了一个证明格式，强制执行纸上的证明和其机械化版本之间的直接联系。本文件的结构如下。格式在第2节中介绍。在我们的格式证明的一个例子是在第3节。在第4节中，我们提出了一个图形界面来构建我们格式最后，我们将我们的格式与其他方法在第5节结束之前，在第6节结束之前。L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）1211232证明格式为了找到一种适当的证明格式，以减少纸上证明结构和证明脚本结构之间的差距，我们有三个灵感来源。第一个是Leslie Lamport的论文[17]，描述了形式证明应该如何编写。 读了这篇论文，它很明显，形式证明的主要特征是结构。一个正式的证明应该明确地揭示初始问题是如何分解成基本子问题的，直到得到明显的陈述。形式证明格式的主要要求之一是突出证明结构。第二个灵感来源来自于阅读不同的算术证明。因为它们主要是处理变换不等式，证明往往可以通过阅读公式而忘记周围的文字来理解在我们的格式中，我们将这种观察推向极端，并假设只有公式才重要。最后一个灵感来源来自验证条件生成器，如WHY[11]。这些系统用于证明程序的正确性。它们接受一个用逻辑断言注释的程序作为输入，并输出一个条件列表。证明所有这些条件可以确保程序中的注释是有效的。我们希望有一个类似的机制，证明在纸上。在证明上运行该工具应该生成一个需要检查的形式条件列表，以确保证明中所写的内容是正确的。实际证明格式的定义直接来自这些考虑。几十年来，证明的适当表示突出了它们的结构。这是Prawitz提出的自然演绎风格[21]。在下文中，我们使用自然演绎的一些规则来说明我们的格式是如何工作的。对于格式的实际描述，我们使用标记语言a`la X ML[4]。2.1公式的格式在我们的格式中，公式以类型化的一阶逻辑表示。该语法直接受到语言的启发，可以用WHY编写逻辑断言。这种语言包含通常的逻辑连接符：合取和，析取或，蕴涵->，否定not。例如，公式<$（xy）<$xy以我们的格式编写为124L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121not（x or y）-> not（x）and not（y）逻辑连接器的优先级是通常的优先级。任意n元谓词由以下表示：predicateName（term1，...，术语n）等式、不等式和区间谓词有其常用的固定语法。例如，区间谓词的一个基本属性写为（x = y = z and x> y and y> z）-> xy z一个公式可以用关键字forall和exists来进行泛量化或存在量化。被量化绑定的变量需要类型化。例如，公式对于所有x：int. exists y：int. x y表示有无穷多个整数。术语是变量、数值常量和任意n元函数应用，语法为functionName（term1，...，术语n）infix语法也可用于常见的算术运算+，-，*，/，%。 例如，公式对于所有x、y、z、n：nat.exp（x，n）= exp（y，n）+ exp（z，n）->n = 2或x * y * z = 0是一个著名的前猜想我们的公式格式有两个方面值得评论。首先，我们可以选择CO q语法的公式，但已决定使用一种语言，是独立于一个特定的证明。我们认为，这种独立性是长期保持大型正式开发的关键问题第二，我们选择了一个文本表示。一个自然的替代方案是使用MATH ML[5]。事实上，我们的证明格式的早期版本[26]确实使用了精简版的MATH ML。例如，公式表示为<进口><负><$（xy）<$xy<或> v> n>x/n>/v> v> n>y/n>/v>/或><联系我们<和>
v> n>x/n>/v>/not> v> n>y/n>/v>/not>L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121125<联系我们这一选择的不幸后果是，不能再要求用户直接键入公式。 应提供一些支持。由于我们无法找到任何令人满意的免费组件来编辑MATH ML，我们决定后退一步，用更简洁的文本表示来表示我们的公式。2.2证明的格式在我们的格式中，我们使用标记来描述证明结构。校样和子校样用标记p标记.可以给证明一个名称与标签n.结论由标记c表示。例如，自然演绎中A BA组B组在我们的格式中表示为介绍/n>A/c>B/c>A和B/c>
缩进仅用于可读性。 格式不要求特定的布局。子目标和结论的相对位置也是自由的。把结论放在第一位会给证明提供一个目标导向的支持。被证明的东西在解释它为什么成立之前就已经给出了。把结论放在最后给出了更常见的前瞻性风格。大多数情况下，纸上的证明是用向前的方式进行的，但对于关键步骤，如应用归纳原理，结论可能会首先给出。我们的格式很容易适应这两种风格。假设由标记h表示。标记包含假定的公式。并以案例分析为例说明了这一[A]...[B]...及其编码ABC CC126L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121或Elim/n>A或B/c>A/h>C/c>B/h>C/c>C/c>
一个证明可以包含的假设和子证明的数量没有限制局部变量用标签v表示。 由于我们的语言是类型化的，标记所包含的文本必须具有形式名称：type。我们说明了使用此标签与通用介绍规则P（n）你好P（x）在我们的语言中，x必须键入。如果我们考虑整数上的谓词，引入规则的表示如下：forall Intro/n>n：int/v>P（n）/c>forallx：int. P（x）
一个证明可以有任意多的局部变量。还增加了两个额外的机制。第一个让用户命名假设。例如，通过组合标记h和n，A n>H1/n>/h>但是，将名称放在假设的文本中并不是一个好主意。它给出了一个非常有限的命名模式，不能添加额外的文本。为了得到更一般的一个，额外的标签f用于指示假设的值。命名的假设应该写为 f>A/f> n>H1/n>/h>第二种机制使得解释为什么证明的结论成立成为可能，即给出一个证明。这是用一个额外的标记j完成的。法律有名字。比如说，L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121127 j> n>exp_plus/n>/j> c>C/c>/p>表明结论是定理exp_plus的一个推论。一个证明中的名称既可以引用其他证明，也可以引用局部假设。总而言之，我们的证明格式由七个标签组成：p表示证明，c表示结论，h表示假设，v表示变量，n表示名称，f表示公式，j表示证明。我们格式的证明结构如下：- 有一个top tagp。- 证明中的每个标签p都有一个子标签c，最多一个子标签n，最多一个子标签j和一些（可能是零个）子标签v，h和p。- 证明中的每个标签h最多有一个子标签f和一个标签n。- 证明中的每个标签j只有子标签n。2.3产生举证义务在程序验证中，为了生成条件，需要使用复杂的技术，例如计算最弱的先决条件。对于我们的格式，生成要简单得多。该算法在这里说明的CO q，但可以很容易地适应于其他系统。 它包括从上到下和从左到右遍历标记的结构。 每次遇到一个证明标签时，它的子证明首先被递归处理，然后生成与标签相关联的条件每个条件都由一个引理表示。还添加了一段脚本来进行必要的簿记并获得适当的假设。为了给出一个更具体的例子，考虑下面的证明
f>A/f> n>h1/n>/h>
...p1/n>B/c>p2/n> f>C/f> n>h2/n>/h>D/c>生成的第一个条件对应于p1，并由引理c_p1表示。条件具有以下形式：引理c_p1：A-> B。证据介绍h1。应用OK。128L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121⇒⇒ ⇒⇒Qed。子证明p1已经在假设A可见的上下文中声明。其结论是B.所以它证明的实际陈述是A B。 添加的脚本片段介绍h1。应用OK。首先介绍假设。在CO q中，假设可以被命名。文件中给出的名称可以在CO q中忠实地反映。策略Intros h1引入了第一个假设A，命名为h1。生成最终策略Apply ok，使得证明总是被证明者2接受。这个简单的技巧提供了免费的类型检查：在处理生成的文件时，证明器会自动检测初始文档中的任何错误。由于每个引理代表证明中的一个步骤，因此跟踪初始文档中错误的起源很容易。形式检验证明的实际任务在于用适当的策略来代替公理ok的所有应用对于第二子证明p2，条件具有以下形式：引理c_p2：A-> C-> D。证据介绍h1。概括（c_p1 h1）;介绍p1。介绍h2。应用OK。Qed。在引理的陈述中有两个假设：A来自上下文，C是p2的局部假设。对于证明脚本，策略Intros h1引入了名为h1的引理的第一个假设A。第二种策略更为复杂。它表示p1从p2可见的事实。为了引入p1，引理c_p1首先需要用p1和p2之间共同的上下文实例化，即假设A，其名称为h1。表达式（c_p1h1）恰好做到了这一点，并且对应于B的证明。在应用策略Generalize（c_p1 h1）之前，目标是C D，之后是B C D。下一个策略Intros p1引入了名为p1的B。这两种策略的结果是预期的结果：B为真的事实可以与在证明P2中命名P1。[2]这种策略代表了一个预先定义的公理ok的应用，它声明一切都是真的。L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121129第三种策略简单地在假设列表中引入名称为h2的C。请注意，生成器在以正确的顺序引入假设时特别小心。最后介绍的假设显示在结论旁边。在我们的例子中，最接近的假设是h2，然后是p1，然后是h1。最后，当所有的介绍都完成后，假设的顺序可能会重新安排，以考虑到司法机构给出的参考资料。这提高了自动策略的性能，这些策略通常优先考虑最后引入的假设。在生成过程中，主自由度涉及不同子证明的可见性。在自然演绎中，如果一个证明P有n个子证明p1，p2，. p n，这些子证明被认为是独立的。例如，不能在不复制整个证明的情况下在证明p2中使用p1在文本证明中，证明p1在证明p2之前被读取。因此，采取限制较少的政策似乎更为自然。由于这个原因，我们在我们这一代人中实现的可见性规则是，pi的结论对于ij在pj内部可见，而在P外部不可见。Richard Bornat [3]采用了类似的方法，用于Fitch在[12]中提出的箱形风格。3例到目前为止，我们已经介绍了我们的格式，并展示了条件是如何生成的。我们仍然需要展示如何将纸上的证明转换为我们的格式。我们的格式背后的想法是，这可以通过向证明文本添加标签来完成。我们用整数上指数函数的一个初等性质房产exp_pos：设x和y是两个整数，如果0x，为了证明exp（x，y）>0，我们有三种情况：如果0y，则exp（x，y）>=x<<如果0 = y，则exp（x，y）= 1如果0 > y，则exp（x，y）=1/exp（x，-y）我们将逐步将标签整合到文本中。最容易添加的标签是名称标签。在这里的证明只有一个名称exp_pos：属性n>exp_pos/n>：设x和y是两个整数，如果0x，为了证明exp（x，y）>0，我们有三种情况：如果0y，则exp（x，y）>=x<<如果0 = y，则exp（x，y）= 1如果0 > y，则exp（x，y）=1/exp（x，-y）第二步是标记所有局部变量，这里有两个变量：属性n>exp_pos/n>：设v>x/v>和v>y/v>是两个整数，130L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121如果0x，为了证明exp（x，y）>0，我们有三种情况：如果0y，则exp（x，y）>=x<<如果0 = y，则exp（x，y）= 1如果0 > y，则exp（x，y）=1/exp（x，-y）下一步是在证明中采用每个公式，并确定它是假设还是结论。在我们的例子中，我们有四个假设和四个结论：属性n>exp_pos/n>：设v>x/v>和v>y/v>是两个整数，如果0x/h>，为了证明c>exp（x，y）>0/c>，我们有三种情况：如果0y/h>，则c>exp（x，y）>=x/c>如果0 = y/h>，则c>exp（x，y）= 1/c>如果0 > y/h>，则c>exp（x，y）= 1/exp（x，-y）/c>最后一步是最微妙的一步。它包括确定每个结论的范围。在我们的例子中，有一个证明有三个子证明。属性n>exp_pos/n>：设v>x/v>和v>y/v>是两个整数，如果0x/h>，为了证明c>exp（x，y）>0/c>，我们有三种情况：如果h>0 y/h>则c>exp（x，y）>= x/c>/p>
如果h>0 = y/h>则c>exp（x，y）= 1/c>/p><如果h>0 > y/h>，则c>exp（x，y）= 1/exp（x，-y）/c>/p>
我们就快完成了。在我们的语言中，变量必须有类型。变量的类型信息实际上应该在添加标记v时放置。所以证明的最终版本是：属性n>exp_pos/n>：设v>x：int/v>和v>y：int/v>是两个整数，如果0x/h>，为了证明c>exp（x，y）>0/c>，我们有三种情况：如果h>0 y/h>则c>exp（x，y）>= x/c>/p>
如果h>0 = y/h>则c>exp（x，y）= 1/c>/p><如果h>0 > y/h>，则c>exp（x，y）= 1/exp（x，-y）/c>/p>
生成的条件在附录A中给出。请注意，由于子证明和假设没有命名，系统自动生成了专门的名称。4Cyp图形界面一个图形界面已经开发，以建立我们的格式3证明。界面由单个窗口组成任何文本都可以在此窗口中阅读例如，阅读第3节的初始无标记校样文本可以得到：3在ftp：//ftp-sop中输入格式是非常有用的。因里阿。fr/l em me/c yp/i nd ex. H TM L.L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121131颜色你的证明文件选择工具物业exppos：设x：int和y：int是两个整数，如果0 x，为了证明exp（x，y）>0，我们有三种情况：如果0 y，则exp（x，y）>= x<<如果0 = y，则exp（x，y）= 1如果0> y，则exp（x，y）= 1/exp（x，-y）彩色TaggedCoq颜色你的证明文件选择工具物业exppos：设x：int和y：int是两个整数，如果0 x，为了证明exp（x，y）>0，我们有三种情况：如果0 y，则exp（x，y）>= x<<如果0 = y，则exp（x，y）= 1如果0> y，则exp（x，y）= 1/exp（x，-y）彩色TaggedCoq要设置标签，用户只需使用鼠标选择区域，然后按下菜单选择中的相应项。例如，选择文本颜色用于指示标签的存在，这里红色用于名称。按照与第3节相同的步骤，然后我们需要选择每个变量并按下项目v：132L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121颜色你的证明文件选择工具物业exppos：设x：int和y：int是两个整数，如果0x，为了证明exp（x，y）>0，我们有三种情况：如果0y，则exp（x，y）>= x<<如果0 = y，则exp（x，y）= 1如果0>y，则exp（x，y）= 1/exp（x，-y）彩色TaggedCoq颜色你的证明文件选择工具物业exppos：设x：int和y：int是两个整数，如果0 x，为了证明exp（x，y）>0，我们有三种情况：如果0 y，则exp（x，y）>= x<<如果0 = y，则exp（x，y）= 1如果0> y，则exp（x，y）= 1/exp（x，-y）彩色TaggedCoq再一次地，通过颜色的变化来指示修改。这给出了一个很好的比喻，它意味着把一个证明转化为我们的格式：它只是在于给证明着色。如果我们继续这个过程，完整的彩色校样如下：结论用蓝色表示，假设用绿色表示。为了保持颜色的数量尽可能少，我们决定对变量和假设使用相同的颜色。就像这样，我们只有三种颜色：红色代表名字，绿色代表假设，蓝色代表证明。还请注意，在上图中看不到校样标签。这是因为证明可以嵌套。 所以给一个证明着色会自动隐藏它的子证明的颜色。我们的解决方案是一次最多给一个子证明着色：最小的子证明，如果它存在的话，它包含了当前的选择。例如，如果在最后一个彩色证明中选择了第二子证明的假设，则整个第二子证明都是灰色的：L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121133颜色你的证明文件选择工具物业exppos：设x：int和y：int是两个整数，如果0x，为了证明exp（x，y）>0，我们有三种情况：如果0y，则exp（x，y）>= x<<如果0>y，则exp（x，y）= 1/exp（x，-y）彩色TaggedCoq则exp（x，y）=10 = y如最后，窗口底部的标签Colored、Tagged和Coq允许用户选择他/她想要的输出。到目前为止，我们一直在使用彩色输出。按下标记标签给出文本的标记版本。它是保存在磁盘上的文件。Coq标签给出了生成条件的列表。5相关作品我们知道，在纸上证明和相应的机械化版本在CO q之间的差距主要是由于这样一个事实，即CO q的战术语言已被认为是一个小的编程语言，其目标是建立证明。就像在编程中一样，证明脚本的简洁性和通用性是有特权的。这不是CO q所特有的，而是所有基于策略的证明者所共有的。在这种证明器中，通常只包含很少的公式。如[18]中所创造的，在脚本中添加公式会增加脚本的粘度。这意味着它降低了脚本的可重用性，并使它们对修改的鲁棒性降低。公式通常不出现在证明脚本中，这一简单事实表明，脚本不足以反映通常的证明。人们一直在尝试用更自然的语言与证明者进行交互。第一个也是最令人印象深刻的是Mizar项目[20]。其他有趣的尝试包括[1，24，27，30]。遵循[13]中使用的术语，这些系统提出了一种声明式的证明风格，而像CO qo声明式脚本通常包含大量公式，因此更接近于纸上的证明不幸的是，这些系统对证明的编写方式施加了一些严格的限制例如，在Mizar中由于系统自动化程度很低，证明脚本通常太134L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121为人类读者详细介绍。最近的一项建议[28]旨在放松这一限制。在Isar [27]中，一些基本结构是硬连线的。一个例子是案例分析证明，其中文档中不同案例的呈现必须遵循对象声明的确切顺序其他有趣的方法包括尝试同时适应过程式和声明式风格[9，16，29]，从策略中提取证明文本[6]，从证明对象中提取证明文本[2，7，23]。请注意，当证明器有证明对象时，可以自动将证明对象转换为我们的格式，方法与[2，7]非常相似。结果恐怕太详细了。然而，通过在保持证明脚本一致的同时改进演示的一些支持，这种逆向工程活动可能是获得可读证明的有效方法。6结论在本文中，我们提出了一个非常简单和灵活的格式编写形式证明。此格式独立于特定的证明器。写证明是为了尽可能自然。 按照通常的方式在写作证明时，作者只被要求明确地指出证明结构。 在每一步中，我们都可以清楚地看到假设是什么，结论是什么。我们还提供了一个非常简单的用户界面，以帮助编写这种格式的证明。有了这个接口，证明是翻译成我们的格式通过一个简单的着色过程。我们的方法是通用的，但考虑到一个特殊的应用程序，即在计算机算术的证明。它的有效性强烈地依赖于这样一种认识，即只看证明中的项几乎足以理解整个证明。这是计算机算术证明的情况，主要是操纵不等式，但它显然不是任何铅笔和纸的证明。一个有趣的问题是，在证明中用标签显式添加的信息是否可以合成。要做到这一点，需要一些非平凡的自然语言分析。一种可能性是使用特殊的关键字或强加一些预定义的布局风格，但这正是我们想要避免使用标签的。使证明可机械检查的信息应该尽可能少地干扰证明的呈现方式证明写作活动与证明检查活动的分离是由我们自己的实验所激发的。我们并不主张这种分离应该永远是规则。 在我们的情况下， 为了调和以人类可读的形式发布证明的必要性与机械检查所有低级证明的繁琐任务，L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121135续费在这方面，我们认为证明的机械检查只是一种增加证明的置信度的方法，而不是在任何情况下取代裁判过程的方法。在引言中，我们已经描述了三个缺点，通常松散的连接之间的出版证明和它的机器检查的版本。第一个缺点是，计算机证明通常只检查已发布证明的最终在我们的框架中，我们得到了更紧密的连接。已发表的证明的每一步都经过检查，并且对于每一步，在形式发展中都有相应的引理第二个缺点是维护证据的困难。为了便于维护，一个好的做法是总是把大的校样分成小的部分。我们的生成过程加强了这种做法，因为每个引理只覆盖了纸上证明的一个步骤。最后一个缺点是很难尝试稍微不同的最终声明版本。在我们的例子中，通过改变陈述，可以直接在已发表的证明上进行变化当重新运行证明脚本时，证明者未能重新建立的引理直接对应于在已发布的证明中需要修复的步骤。为了把我们的实验变成现实的方法，还需要做更多的工作。首先，格式必须针对大型验证开发进行密集测试。我们计划用它来重新设计我们的形式化的浮动点数[8]。其次，生成的条件很少能被CO q自动证明。即使完全自动化不是我们的主要目标，也需要开发更多的策略，以获得自动证明的合理比例。最后，我们正在研究直接使用科学编辑器（如TeXmacs [25]）来编写证明的可能性。这将免费为我们提供通常的数学表达式显示与作为文本表示，已知用于积分的符号或用于矩阵的符号难以呈现。引用[1] Andreas Abel，Bor-Yuh Evan Chang和Frank Pfenning。人类可读的机器可验证的证明，用于教学建设性逻辑。PTP'01，锡耶纳，意大利，2001年[2] Andrea Rupti，Luca Padovani，Claudio Sacerdoti Coen，and Irene Schena. HELM和语义数学网。在TPHOLs[3] 理查德·博纳特渲染 树 证明 盒子的形式。在 2003年 第46http://www.informatik.uni-bremen.de/uitp03/proceedings.pdf网站。[4] Tim Bray、Jean Paoli和C.迈克尔·斯珀伯格-麦奎因可扩展标记语言（XML）1.0. W3C推荐。[5] 大卫·卡莱尔，帕特里克·扬，罗伯特·迈纳，和尼科·波佩利耶。数学标记语言（MathML）2.0版。W3C推荐。136L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121[6] 阿芙拉·科恩 在HOL的证明帐户。1988年未出版的草稿[7] 是的，吉尔是KAHN，LAURNTHY。从打印机打印文本。 在TLC A，number902，LNCS，第109-123页， E d i n b u r g h ， S c o t l a n d ， 1 9 9 5 中 。[8] MarcDaumas，L aur enceR id eau，andL aur entTh'ery. 浮点数的一种通用逻辑及其在精确计算中的应用。在TPHOLs[9] 大卫·德拉哈耶。自由式定理证明。在TPHOLs[10] James Demmel和Yozo Hida准确 划点求和。提供http://www.cs.berkeley.edu/~ demmel/AccurateSummation.ps.[11] Jean-C是菲利普·菲力的朋友。在T类型T或Y中执行ImpeivProgramms。IinTYPES '9 8 ， n u m b e r 1 6 5 7 i n L N C S ， E i n d h o v e n ， N e t h e r l a n d s ， 1 9 9 8 .[12] 弗雷德里克湾费奇 符号逻辑：导论。 罗纳德出版社，1952年。[13] 约翰·哈里森。证明风格。在TYPES[14] 约翰·哈里森。浮点运算的机器学习理论在TPHOLs[15] Grard Huet，Gilles Kahn，and Christine Paulin-Mohring.Coq Proof Assistant：A Proof：版本6.1。技术报告204，INRIA，1997年。[16] 格奥尔吉岛Jojgov，Rob P. Nederpelt，and Mark Scheeper. 将非形式数学证明的结构忠实地反映到形式类型理论中。2003年，苏格兰爱丁堡，ENTCS，MKM Symposium[17] 莱斯利·兰波特如何写证明American Mathematical Monthly，102（7）：600[18] 尼古拉斯·梅里亚姆和迈克尔·哈里森。 定理证明器的GUI有什么问题？在UITP’97[19] 保罗·S矿工。在PVS中定义IEEE-854浮点标准技术备忘录110167，美国宇航局，兰利研究中心，1995年。[20] 开泽 形式化数学杂志。 http://mizar.org/JFM/。[21] 达格·普拉维茨 自然演绎。 阿尔姆奎斯特·维克塞尔，乌普萨拉，1965年。[22] David M. Russino AMD K5浮点平方根微代码符合IEEE的机械验证。系统设计中的形式化方法，14（1）：75[23] JorgH. Siekmannn，ChristophBenzmüller，ArminFiedler，AndreasMeier，andMartinPollet. 使用OMEGA：Sqrt 2进行验证开发是不合理的。在LPAR[24] 唐·赛姆三个策略定理的证明在TPHOLs[25] TeXmacs 一个免费的科学文本编辑器。http://www.texmacs.org/网站。[26] 我不是你。 适用范围：一个Ex periment。 在UITP' 03中，第143-159页，罗马，意大利，2003年。[27] 马库斯·温泽尔可读形式证明文档的一般解释方法在TPHOLs[28] 弗里克·韦迪克 正式的证明草图。可查阅http://www.cs.kun.nl/~ freek/notes/sketches2.ps.gz。L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121137[29] 弗里克·韦迪克Mizar Light为HOL Light。在TPHOLs[30] 文森特·扎米特。一种可扩展的声明式证明语言的实现在TPHOLs138L. Theory/Electronic Notes in Theoretical Computer Science 103（2004）121A生成条件引理c_gp_1：（x：Z）（y：Z）（Zlt ZERO x）->（ZltZERO y）->（Zge（exp x y）x）。证据介绍x y gh_1。介绍gh_1_1。应用OK。Qed。引理c_gp_2：（x：Z）（y：Z）（ZltZEROx）->证据介绍x y gh_1。泛化（c_gp_1 x y gh_1）;导入gp_1。介绍gh_2_1。应用OK。Qed。引理c_gp_3：（x：Z）（y：Z）（Zlt ZERO x）->（ZgtZEROy）->（exp x y）=（Zdiv '1'（exp x（Zoppy）。证据介绍x y gh_1。泛化（c_gp_1 x y gh_1）;导入gp_1。泛化（c_gp_2 x y gh_1）;导入gp_2。介绍gh_3_1。应用OK。Qed。引理exp_pos：（x：Z）（y：Z）（ZltZEROx）->（Zgt（exp xy）证据介绍x y gh_1。泛化（c_gp_1 x y gh_1）;导入gp_1。泛化（ c_gp_2 x y gh_1 ） ; 导 入 gp_2 。 泛 化（c_gp_3 x y gh_1）;导入gp_3。应用OK。Qed。
我的内容管理
展开
