轻量级验证系统的用户友好界面

可在www.sciencedirect.com在线获取理论计算机科学电子笔记285（2012）29-41www.elsevier.com/locate/entcs轻量级验证系统的用户友好界面1Andrei Lapets2 Assaf Kfoury3波士顿大学美国波士顿摘要用户友好的界面可以发挥重要作用，将机器可读的正式参数表示的好处带给更广泛的受众。AARTIFACT系统是一个易于使用的轻量级验证器，用于涉及常见数学概念的逻辑和代数操作的形式参数。该系统通过利用支配普通数学概念的命题数据库来提供验证能力。AARTIFACT系统的多面交互式用户界面结合了几种用户友好界面设计方法：（1）基于现有约定的熟悉和自然的在数学实践中，（2）一种基于关键字的实时查找机制，用于在系统的命题数据库中发现的句法习惯用法和语义概念的(3)以重新格式化的原始输入形式的即时验证反馈。该系统的自然语法和命题数据库允许它满足用户在形式推理场景中的期望，这是故意的。 基于关键字的实时查找机制和验证反馈允许系统以即时、交互和上下文感知的方式教导用户其能力和局限性。关键词：形式验证，用户界面1引言用户友好的界面可以发挥重要作用，使更多的受众受益于在数学教学和涉及数学严谨性的研究工作中，都存在许多这样的好处。这些包括可重用性、示例的自动评估以及使用机器验证的机会。机器验证可以避免任何事情，从检测基本错误，例如1本材料部分基于国家科学基金会资助的工作，资助号为0820138和0720604。本材料中表达的任何意见，发现，结论或建议都是作者的意见，不一定反映国家科学基金会的观点。2电子邮件：lapets@bu.edu3电子邮件：kfoury@bu.edu1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.06.00430A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）29未绑定的变量或类型不匹配，在参数中完全可信，因为它始终使用特定数学逻辑的基本原理构造。存在各种各样的机器验证系统，其中一些已经被调查并沿着各种维度进行比较[33]。然而，直到最近，用户界面设计还没有成为正式验证社区的主要焦点早期的研究声称，验证系统允许然而，即使是一些基本的和普遍存在的形式结构（例如，表示向量连接或表示图形的符号）的具体语法的约定也是不一致的。 此外，为了实用，验证系统必须包含非常庞大的定义和命题库。因此，即使一个验证系统有一个简单的核心语法，一个希望使用它的专家用户必须首先熟悉任何可能与手头任务相关的库。这样，即使是专家用户也无法理解这些系统的真正语法（由与库内容相对应的语法习惯用法组成）。交互式地教导用户系统能力和限制（包括用户可能需要使用的结果库）的问题还没有得到很好的解决用户界面的目的是双重的。首先，它必须通过提供与用户的直觉和经验相对应的系统抽象来满足用户的期望。其次，它必须以一种即时的、交互的和上下文感知的方式明确用户的期望。我们提出了我们的用户界面设计的AARTIFACT系统，4一个轻量级的验证系统的正式参数，涉及常见的数学概念的操作。该界面具有多方面的设计，旨在满足这两个用户友好界面的标准。它包括三种方法：基于形式推理实践中现有惯例的熟悉和自然的语法，用于发现支持的语法习惯用法和语义概念的基于关键字的查找机制，以及以重新格式化的原始输入形式的反馈。2动机和背景即使考虑的是一小部分数学概念，一个有实践经验的数学家也可能会使用大量和各种各样的语法习惯用法来指代与之相关的谓词和运算符。为了说明这一点，图1给出了一个非常简短的素数无穷大的证明。这个证明包含了对有限集合、自然数、素数、乘积和因子的明确引用。它还包含许多对这些概念的属性以及它们之间关系的隐式引用为了接受以这种方式编写的参数作为输入，用户界面必须既灵活又健壮。在本节中，我们简要回顾了在设计这样的接口时可能有用的相关方法（其中一些方法是基于相关工作中采用的方法第3节描述了如何在AARTIFACT的用户界面设计中使用这些方法4可在www.example.com上查阅http://www.aartifact.org。A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）2931介绍一下P，M。设对所有n∈N，如果n是素数，则n∈P。假设P是一个有限集合，P是非空的，且P≠N。假设m = P0·. ·P|P|-1。设m∈N。对于任意p∈N，如果p是m+1的素因子，则p不是m的因数，p是素数，p是m的因数，有一个矛盾。p∈P，图1.一、一个使用AARTIFACT系统证明素数个数的例子系统为了便于讨论，我们采用以下术语：用户以某种形式构造参数（可能在用户界面的帮助下），然后界面向用户提供参数有效性的反馈2.1自然意象与具象表现任何旨在支持用户在构建证明（如图1所示）时所采用的形式推理活动的系统，都必须至少提供一种符合目标社区中流行的约定的自然语法的用户。Scunak数学助手[5]的设计者们在一个系统的具体表示中提出了对“自然性”的需求。系统必须至少提供一些熟悉但简单的语法结构来组装逻辑论点（即合取，析取，量化）。此外，即使系统结合了包含用户可能想要采用的许多概念、属性和关系的广泛库，系统也必须允许用户采用其中的许多而不显式地引用它们（即，当用户希望使用结果时，它不需要Scunak系统的设计者[5]将其称为而不是名字”类似地，Tutch系统的设计者认为，“对[人类]的[推理规则]的32A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）292.2句法习语的检索与关键词自动识别语法是一种通信手段，一个简单自然的形式语法是有用的，因为它提供了一种可以快速学习的方法来编码形式参数。然而，这个简单的语法必须用来表示一个庞大的操作符、谓词甚至语法习惯用法库。有必要将所有这些约定存储在某种数据库中，并将它们公开给用户，而不需要他们花费时间和精力阅读文档或浏览库。因此，虽然语法习惯用法（或者更一般地说，类型化术语[20]，或逻辑定义和定理[8]）的索引数据库是一个自然的起点，但用于编程环境的实时基于关键字的查找技术[10，18]建议进一步提高系统可用性的方法。该系统2.3关于逻辑有效性的反馈提供给用户的关于参数有效性的反馈这种反馈有三个重要特征，有助于系统的可用性和灵活性：反馈的易读性和可理解性（例如，错误位置的精确指示），用户希望轻松选择反馈类型的选项（例如，用户希望采用的验证技术[30]或逻辑系统），以及提供反馈的速度（可能取决于验证程序的选择）。3轻量级验证器我们更详细地描述了AARTIFACT轻量级验证系统接口的整体设计和各个组件。图2和图3从用户的角度示出了用户界面用户提交一个使用具体语法表示的形式参数。如果选择了“library”或“syntax”选项卡，则会根据用户键入时光标周围的文本提供所支持语法的实时提示。用户还可以选择一个逻辑系统，然后单击“verify”以生成反馈，该反馈将输入复制为HTML，并使用颜色突出显示参数的有效和无效部分（分别使用蓝色和红色）。图4说明了系统的各个组件的总体组织，以及它们在实践中的行为。 专家管理的数据库包含一个句法结构和命题库。该数据库被编译为客户端JavaScript应用程序以进行语法查找，以及服务器端可执行文件以执行正式验证。这确保了只有服务器必须被信任才能正确地执行验证，而提供者的计算负担A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）2933图二、“库”模式下用户界面的屏幕截图语法查找由客户机执行。当图2和图3所示的Web界面首次加载时，服务器将JavaScript应用程序发送到客户端。然后，用户可以在JavaScript应用程序的帮助下在自己的浏览器中编写参数，并可以随时单击按钮将参数提交给服务器进行验证3.1具体论据参数的具体语法（部分列在图5中）由英语短语、LATEX标记和MediaWiki标记组成。 我们用yx表示逗号分隔变量标识符的序列。一个参数由一系列的状态组成.只有三种语句，其中两种（Assume和Assert）从用户的角度来看非常相似。每个语句要么引入全局变量，要么引入一个假设，要么表示一个关于用户认为是真的东西的断言。逻辑表达式的语法对应于高阶逻辑中逻辑运算符的典型英语表示。逻辑表达式的两个基本情况是LATEXsyntax中的数学表达式和英语短语谓词。充当谓语的英语短语可以有零个或多个参数。英语短语谓词在抽象语法中表示（未在34A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）29图三. “验证”模式下用户界面的屏幕截图图四、系统组件和操作概述这篇论文，但在相关报告中发现[14]）使用单词列表（没有标点符号或空格的字符串字面量）和占位符（我们表示[]）。如果英语短语包含任何数学参数，则将英语短语谓词应用于表示参数的表达式元组。例如，表达式中的pred-icate \l{$p$isapathin$G$}使用列表表示{[]， is， a， path， in， []}，A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）2935.报表S：：=假设E|断言E|介绍x逻辑表达式E：：=$e$|\l{w1w2. . . wn}|E1iE2|E1隐含E2|e1和e2|E1或E2|这并不是说E|对于所有$x$，e|exists$x$，e文字或数学表达式W：：=英语 词|$e$数学表达式e：：=1|2| ...|X|e一 e二|（五）|\空集|{e}|e1，.，en|e1+e2..图五. 具体语法概述。整个表达式表示为{[]，is，a，path，in，[]}（p，G）.数学表达式是用许多典型的LATEX语法结构来表示的.支持一组常量和运算符（与现有LATEXpackages中可能存在的基本命令一致）。直接支持一些有限的用户扩展性：用户可以定义自己的infix操作器。对所支持语法的更复杂的扩展需要系统的自定义构建。解析器的任务是处理这是一个需要考虑验证的论点。具体语法的解析器在Haskell中使用Parsec解析器组合子库[17]构建，该库具有足够的表达能力，可以为一般上下文敏感语法构建有限的前瞻解析器。这个库易于使用，并允许简洁的解析器实现。AARTIFACT解析器在所有测试输入上的执行没有明显的延迟（无限前瞻能力仅在解析器定义中的几个点使用，例如允许专家用户定义自己的in fix运算符）。使用上下文相关解析器处理语法习惯用法的总体方法类似于Fortress编程语言[26]的解析器设计中所采用的方法。36A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）293.2库访问当前AARTIFACT库支持的命题和定义包含数百个条目的集合。每个命题都涉及语义概念，它们可能具有的属性以及它们之间可能存在的关系。下面的命题是一个非常简单的例子：“for anyx∈R，y∈ R，z∈ R，xy，yz<<意味着x z这些命题中的许多只是简单地陈述了两种形式的记法或句法之间的等价性它们可以被看作是建立一个范式来表示某些概念或其属性。例如，下面的命题将有限范围内的一组整数的典型符号转换为“{ x，.，y}“，转化为一个谓词，然后用于其他关于有限范围内整数集合的性质的命题：“for anyx∈Z，y∈ Z，x≤y意味着{x，.， y}是从x到y“的整数的集合。该库目前的目的是支持算术和朴素集合论中常见的代数操作和概念。特别是，它包括：许多常见的一元和二元运算符的数字，集，和向量;一些常见的一元，二元和三元关系对应的属性和之间的关系的数字，集，和向量;和命题，规范如何运营商保持或删除这些属性和关系。因此，目前的库还没有足够的广度和深度来支持在广泛的正式领域中对复杂概念的推理。我们打算继续扩大这一图书馆，以满足该系统应用的需要。对于用户来说，学习当前库支持的常见概念的所有可能的语法结构和习惯用法 因此，在本发明中，实时关键字查找系统被集成到用户界面中以促进该过程。每当用户键入参数时，用户光标周围的文本立即图2显示了这些建议的外观。如果选择了“library”选项卡，右边的面板会列出各种对应于常量和谓词的受支持的语法习惯用法。 如果某些关键字集合产生大量结果，则用户可以键入更多关键字以缩小这些结果。 作为正在进行的工作的一部分，正在开发向用户提供相关关键词A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）2937使用这些特征，系统能够以上下文敏感的方式通知用户预期的内容，并且在这样做时建立与可能已经知道她希望采用的概念但可能还不熟悉系统的语法或库的当用户希望使用社区内不一定一致的概念和符号时，这是必不可少的例如，支持的闭实数区间的表示形式可能是{x|0 ≤x≤ 10}和[0，10]，集差运算符的符号可能是\或−，向量连接的符号可能是·或。在用户考虑这些约定的上下文中通知用户这些约定节省了时间，并提供了在相关上下文中学习系统语法的机会。即使用户不熟悉任何语法约定，她也可以临时将与所讨论的概念相关的关键字直接输入到参数中，以便接收关于该概念的支持的标记的信息。这个特性是作为一个JavaScript应用程序实现的，它是从库的内容编译而来的。每当加载Web界面页面时，都会将JavaScript应用程序发送到用户3.3确认反馈AARTIFACTweb界面提供了一种方法，用于选择验证技术（目前非常小）的集合之一。如图3所示，当请求验证时，参数的原始ASCII文本被处理并转换为HTML反馈，其中颜色用于指示错误（例如，未绑定的变量，断言中不可验证的子表达式）和可验证的断言。 这通过在解析器内维护将抽象语法与原始具体语法耦合的数据结构来实现。 值得注意的是，虽然目前只使用了AARTIFACT验证可执行文件，但任何其他具有命令行界面的验证工具都可以接受ASCII输入并生成 可以使用此接口调用文本或HTML输出4可用性评估我们已经利用了[16]AARTIFACT系统来定义和推理类型化领域特定语言的组合形式[4]。隐式地调用处理集合代数的命题的能力对于使这个过程易于管理和使所得到的证明清晰易懂是必不可少的这一练习也导致了一些小错误的发现，并简化了组成形式主义中的一些定义。该系统还被部署在两个本科课程中的几个正式推理作业：5关于函数的高级本科课程[5]这些课程是：2009年秋季的38A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）29函数编程[15]和线性代数的介绍性本科课程。函数式编程课程的部署范围有限，仅构成“试运行”，而线性代数课程的部署构成了一个小的初始实验。计划进行更广泛的未来实验;这将需要开发云计算基础设施，以确保系统在有许多学生的课程中的可靠性能。在线性代数课程中，第一个家庭作业是给学生八个简单的陈述来证明（这些构成了证明R2是向量空间，因为R是向量空间）。他们只得到了一个经过验证的证明的例子，以指导他们使用AARTIFACT系统。没有提供解释该系统功能的教程。学生可以查阅课堂笔记和教科书，这些都是以传统的方式编写的，没有考虑自动验证。一些学生使用邮件列表提出了问题，这些问题属于可管理的范围，并通过示例或澄清来回答。分配#1#2#3经核实完全正确的提交材料7713≤20%不可验证/缺失公式的提交431>20%不可验证/缺失公式的提交221提交材料总数（来自16名学生）131215关于使用AARTIFACT的邮件列表问题数量532见图6。学生在线性代数本科课程中要求自动验证证明的作业中的表现。这门课有16名不同年级的学生（1 - 4年级的本科生），在第一次作业中，13名学生试图提交用人工制品验证的证明。作业完成时，有2名学生犯了重大错误，4名学生犯了一些小错误，其余7名学生没有错误。随后的任务具有类似的范围，并导致类似的结果，如图6所示。学生能够以最小的指导（超出讲座和阅读中提供的传统定义）使用该系统，这证明了在自然语法和可以隐式调用结果的底层库的帮助下满足学生期望的可用性优势。学生能够获得不完整证明的部分学分，这表明了采用轻量级验证方法的一个潜在有用的方面。5相关和未来的工作AARTIFACT语法反映了其他形式化验证系统的设计原则，如Tutch[1]和Scunak[5]。机器中对自然接口的需求2010年春季迭代的“几何算法”。 两者都是计算机科学必修课程为波士顿大学文理学院计算机科学系的本科生提供。A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）2939一般来说，验证已经被Tutch证明检查器[1]，Scunak数学辅助系统[5]，ForTheL语言和SAD证明助手[30]，EPGY定理证明环境[19]，ΩMEGA证明验证器 [28] ， ProveEasy 系统 [6] 的设 计者 ，Sieg 和 Cittadini [27] 的工 作以 及Hallgren和Ranta [9]的工作所认可。 为了更好地服务于工程、数学和应用科学领域的用户，Fortress编程语言[2]将常见的数学符号和语法结构纳入其语法中，设计者正在努力组装一个可扩展的解析器，以简化语言语法的用户导向扩展[26]。更广泛地说，还有其他的努力来创建接口和系统的实际形式化的数学。MathLang项目[12]是一个广泛的长期项目，旨在使自然语言成为数学论证和证明的输入方法。AARTIFACT系统的具体语法和解析器可以通过增加对额外语法结构和习惯用法的支持，以及通过在HTML反馈中提供更多信息（例如，关于可验证断言的为MathML等标准引入输入和输出支持也是值得的。在Haskell的上下文中，已经完成了为example库提供搜索功能的一些相关工作。已经开发了搜索工具，允许用户在上下文中按类型检索和浏览表达式[13]，并且存在一个名为Haskell的在线搜索工具，用于探索Haskell库[20]。Hallgren和Ranta [9]的工作提出了一个证明编辑器，它使用自然语言解析框架与类型检查相结合，以交互方式帮助用户在创作可验证证明时利用支持的形式和自然语言语法结构。Matita [3]是一个证明助手，其自动化主要基于集成的搜索引擎。也有关于库函数检索的工作，甚至使用关键字集合自动构建编程语言代码片段[10，18]。这项工作表明，我们自己未来的努力可以更好地集成实时查找功能与验证功能。例如，实时查找提示实际上可以为有效表达式提供建议，这些表达式由参数中断言范围内的变量组成。更一般地，可以将一些简单的验证技术（例如，未绑定变量检测）整体表示为JavaScript应用。我们的工作包括创建一个使用HTML和JavaScript实现的Web界面。这种策略类似于相关工作中所采用的策略[11]，尽管该工作专注于交付（仅使用Web浏览器）现有证明助手的外观，感觉和功能。还有许多其他工具用于证明的形式化表示和机器验证，例如Coq [22]，PVS [21]和Isabelle [23，24]。其中许多已被调查和比较沿尺寸有关的可用性[33]。这些系统通常要求用户对逻辑有一定的理解，40A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）29在她能够验证甚至是基本的数学论证之前，旨在支持我们的工作。像Coq这样的系统的接口通常需要用户在一个严格的交互式框架内工作，并组装证明脚本，不一定反映数学教科书所采用的演示风格。更具体地说，形式化表示和验证系统的设计与我们的工作有一些共同的动机，包括Isabelle/Isar [31]和Mizar[29]。 特别地，Isabelle/Isar被设计为相对独立于任何特定的底层逻辑，并且两个系统都是在考虑人类阅读能力的情况下设计的。Mizar [8]在基于关键字的查找方面有一些工作，但它不涉及为用户提供实时的语法和语义提示，并且可搜索库没有隐式地与验证过程集成引用[1] Abel ， A. ， B. Chang 和 F. Pfenning ， Human-readable machine-verifiable proofs for teachingconstructive logic，in：U. Egly，A.菲德勒，H。Horacek和S. Schmitt，编辑，PTP[2] Allen，E.，D. Chase，J. Hallett，V. Luchangco，J. W. Maessen，S.柳湾，澳-地L. S. Jr.和S. Tobin-Hochstadt，The Fortress Language Specification Version 1.0（2008）。URLhttp://research.sun.com/projects/plrg/fortress.pdf[3] Alberti，A.，C. Sacerdoti Coen，E. Tassi和S. Zacchiroli，用户与martita证明助理的交互，J。自动原因的39（2007），pp.109比139[4] Bestavros ， A. ， A. Kfoury ， A. Lapets 和 M. Ocean ， Safe Compositional Network Sketches ： TheFormal Framework，in：HSCC231-241。[5] 布朗角，澳-地E、使用Scunak的错误和无效教科书证明，在：MKM110-123[6]伯斯托尔河 M.， Proveeasy：Helping People Learn to Do Proofs，电子笔记理论。 Comput. Sci. 31（2000），pp. 16比32[7] Buswell，S.，S. 德维特A.Diaz，P.扬河Miner，N.波佩利耶湾史密斯，N。索伊埃泽尔河苏特和S. Watt，Mathematical Markup Language（MathML）1.01 Specification（Abstract）（1999）。网址http://www.w3.org/TR/REC-MathML[8] Cairns，P.和J. Gow，在mizar中集成搜索和创作，J. Autom。原因的39（2007），pp. 141-160[9] Hallgren，T.和A. LPAR70比84[10] 汉，S.，D. R. Wallace和R. C. Miller，Code completion from abbreviated input，in：ASE332-343.[11] Kaliszyk，C.，网络接口的证明助理，电子笔记理论。 Comput. Sci. 174（2007），pp. 49比61[12] Kamareddine，F.和J. B. 用MathLang计算机化数学文本，电子笔记理论。Comput. Sci. 205（2008），pp.5-30[13] Katayama，S.，系统搜索表达式的库，见：AIC381-387.[14] Lapets，A.，提高轻量级正式验证系统的可访问性，技术报告BUCS-TR-2009-015，计算机科学系，波士顿大学（2009）。[15] Lapets，A.，轻量级形式验证在功能代码推理课堂教学中的应用，技术报告BUCS-TR-2009-032，CS部门，波士顿大学（2009年）。A. Lapets，A.Kfoury/电子笔记理论计算机科学285（2012）2941[16] Lapets，A.和A. Kfoury，自然背景验证：安全组成网络草图，技术报告BUCS-TR-2009-030，CS部门，波士顿大学（2009年）。URLhttp://www.cs.bu.edu/techreports/2009-030-verified-netsketch-soundness.ps.Z[17] Leijen，D.和E. Meijer，Parsec：Direct Style Monadic Parser Combinators for the Real World，Technical Report UU-CS-2001-27，计算机科学出版社，乌得勒支大学（2001）.[18] 利特尔，G。和R. C. Miller，Keyword Programming inJava，ASE84比93[19] McMath ， D. ， M. Rozenfeld 和 R. Sommer ， A Computer Environment for Writing OrdinaryMathematical Proofs，in：LPAR507-516[20] 米切尔，N.，Hoomble overview，The Monad.Reader12（2008），pp.27比35[21] Owre ， S. ， J. M. Rushby 和 N. Shankar ， PVS ： A prototype verification system ， in ： D. Kapur ，editor ， CADE ： Proceedings of the 11th International Conference on Automated Deduction ，Lecture Notes in Arti Official Intelligence607（1992），pp.748-752[22] Parent-Vigouroux，C.，归纳构造演算中的程序，Formal Aspects of Computing9（1997），pp. 484-517[23] 保尔森湖“Isabelle: A Generic Theorem Prover,” Springer,[24] 保尔森湖C.的方法，通用自动证明工具，在：自动推理及其应用：纪念拉里·沃斯的论文，麻省理工学院出版社，剑桥，MA，美国，1997页。23比47[25] Rudnicki，P.，Mizar项目的概述，在：1992年程序的类型和证明研讨会的会议记录，1992年，pp。311-332.[26] Ryu，S.，Parsing fortress syntax，in：PPPJ七十六比八十四[27] Sieg，W.和S.Cittadini，正规自然演绎证明（在非经典逻辑中），在：D。哈特和W. Stephan，编辑，机械化数学推理，计算机科学讲义2605（2005年），第页。169-191。[28] Siekmann，J. H、C. Benz müller，A. Fiedler，A. Meier和M. Pollet，ProofDevelopment withOMEGA：sqrt（2）Is Irrational，in：LPAR，2002，pp. 367-387.[29] Trybulec， A.和 H.Blair， Computer Assisted Reasoning with MIZAR ， in ： Proceedings of the 9thIJCAI，Los Angeles，CA，USA，1985，pp.26比28[30] Verchinine，K.，A. Lyaletski，A. Paskevich和A. Anisimov，从逻辑和实践的角度来看数学文本的正确性，在：第9届AISC国际会议，第15届微积分研讨会和第7届智能计算机数学国际MKM会议（2008年）的会议记录。583-598.[31] Wenzel，M.和L. C. Paulson，Isabelle/Isar，in：F. Wiedijk，editor，The Seventeen Provers of theWorld，Lecture Notes in Computer Science3600（2006），pp.41比49[32] Wenzel ， M. M. ， “Isabelle/Isar - 一 个 人 类 可 读 的 正 式 证 明 文 档 的 通 用 环 境 ， ” 博 士 。 论 文 ，InstitutfurInformatik，Te c hnis cheUni versit？atMu？n chen（2002）。[33] Wiedijk，F.，比较数学证明器，在：MKM188-202.