PLATΩ：文本编辑与辅助证明系统的电子笔记

理论计算机科学电子笔记174（2007）87-107www.elsevier.com/locate/entcsPLAT Ω：文本编辑与辅助证明系统马克·瓦格纳Fac hbe r eich Informatik，U niversitétdesSaarrlandes66041Saarbruécken，Ger many（www. ags.uni-sb. de/Amwagner）塞尔日·奥特谢尔D FKIGmbH&Fac hbe r eich Inforr mat ik，UniversitatdesSaarlandes66041Saarbrucke n，Ger many（www. dfki。de/serge）克里斯托夫·本茨·穆勒Fac hbe r eich Informatik，U niversitétdesSaarrlandes66041Saarbruécken，Ger many（www.ags. uni-sb. de/Escherichris）摘要我们提出了一个通用的调解人，称为P拉特Ω，文本编辑和证明助理之间。PLATΩ aims·以尽可能自然的方式集成支持数学文档的开发，出版，形式化和验证：用户使用他习惯的非正式语言，即自然语言和公式的混合物，用科学的WYSIWYG文本编辑器编写他的数学文档。然后，这些文件的语义注释，保留文本结构，通过使用灵活的，参数化的证明语言，我们提出。 从这个非正式的语义表示PLATΩ自动为证明助手生成相应的形式表示，在我们的例子中是ΩMEGA。PLATΩ的主要任务是在文档的交互式开发过程中维护一致的正式和非正式表示。保留字：文本编辑器，校对辅助系统，用户界面，ΩMEGA，Texmacs1介绍与计算机代数系统不同，数学证明辅助系统在数学实践中尚未获得相当大的认可和相关性。显然，这些系统的功能和优势通常不足以吸引处于研究边缘的数学家。然而，对于电子学习和工程环境中的应用程序，它们的能力通常是足够的。然而，即使在这些应用方面，仍然需要取得重大进展，1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.02488M. Wagner等/理论计算机科学电子笔记174（2007）87特别是关于这些系统的可用性。当前系统的一个显著缺点是它们不能完全集成到标准的数学文本编辑器中或从标准的数学文本编辑器中访问。出于诸如辅导数学、交流或出版数学文档的目的，实际上通常通过采用标准数学文本编辑器使用公共数学表示语言对内容进行编码相反，证明辅助系统需要完全形式化的表示，并且还没有与这些标准的数学文本编辑器充分联系起来。因此，与其为数学辅助系统ΩMEGA [24]，我们提出了一种扩展ΩMEGA的通用方法，以作为科学文本编辑器的数学服务提供者。‘If the mountain won’t come to Mohammed, Mohammed must go to the我们的方法允许用户用他习惯的语言编写他的数学文档，即自然语言和公式的混合。这些文件，然后可以保留文本结构的语义注释，通过使用灵活的参数化证明语言，我们目前。从这个语义表示中，PLATΩ自动地建立起相应的形式表示并进一步关注一致版本的维护。形式表示允许底层证明辅助系统以各种方式支持用户，包括管理数学定义、定理和证明，以及访问自动定理证明器、计算机代数系统和其他数学工具，以便自动验证用户做出的结论和计算，并建议可能的校正。宗教课。这些功能可以通过上下文敏感的服务菜单，以便支持在高抽象级别上的数学文档的交互式开发一方面，这些服务可以包括自动生成部分证明和计算的可能性，以便使用户不必关心繁琐的细节，并让他专注于证明的实质部分。因此，菜单交互可能导致形式表征的变化，而形式表征的变化通过PLATΩ反映在语义表征的变化在文件中另一方面，在文本编辑器中进一步证明导致文档中的变化，这些变化由PLATΩ传播到ΩMEGA中的形式表示的变化。总而言之，这种方法允许数学文档的增量式交互式开发，此外还可以通过ΩMEGA进行形式验证，从而获得经过验证的数学文档。这种方法通常独立于证据辅助系统以及文本编辑器。尽管如此科学所见即所得文本编辑器TE XMACS[27]提供专业的排版并在LATEX中添加了类似于ACI它此外，允许定义自动处理文档的插件，因此特别适合于PLATΩ的集成。本文的结构如下：第二节介绍了Ω mega的基本概念，M. Wagner等/理论计算机科学电子笔记174（2007）8789系统，以便更具体地激励我们的设置。第3节介绍了中介器PLATΩ，重点介绍了文本编辑器和证明辅助系统的接口。第4节中给出了一个工作示例，说明了一体化PLATΩ到一个科学文本编辑器，例如T E X MAc S。的本文最后概述了相关工作（第5节），并总结了第6节的主要结果。2分类：Ωmega、Maya和任务层证明辅助系统ΩMEGA的开发是为工作数学家或软件工程师的正式工作构建一个包罗万象的辅助工具的主要尝试之一它是证明规划范例中的系统的代表，并且结合了交互式和自动化证明为具有丰富和结构良好的数学知识的领域构建（见右图）。ΩMEGA-系统目前正在重新开发中，其中，开发图管理器MAYA对其进行了扩充，底层自然演绎演算被CO RE-演算替换[4]。MAYA系统[8]通过允许用户以结构化的方式指定和验证开发来支持进化的形式化开发，它在采用统一的核查机制-大规模开发规范的结构，并在更改规范时保持已完成的验证工作。像ΩMEGA这样的证明辅助系统依赖于在结构化理论中形式化的数学知识，定义、公理和定理。 MAYA系统是新的ΩMEGA系统通过其OMDOc接口负责管理这些理论的变化[19]。CO RE-演算支持直接在断言处进行证明开发[17]第17节，在定义的应用方面证明步骤是合理的，公理、定理或假设（统称为断言）。它为所谓的TASK层[14]提供了逻辑基础，T ask层[ 14 ]是新的证明数据结构（PDS）[5]的实例。TASK层是ΩMEGA中基于计算机的证明构造的核心组件。它提供了一个统一的证明结构接口对于人类用户和自动证明搜索过程MULTI[21]和ΩANT s [9，26]。PDS的节点用任务来注释，这些任务是通过定义at的多个焦点来增强的Gentzen风格的多结论序列在证明过程中保持的子公式上的注意力。通过以下证明构造步骤之一，每个任务被简化为可能为空的子任务集合(1)引入了一个证明草图[30]1，（2）用于子公式的弱化和分解的深层结构规则，（3）一个引理的应用，该引理可以是正-1 在旧的ΩMEGA系统中，这是通过使用所谓的岛方法来实现的。90M. Wagner等/理论计算机科学电子笔记174（2007）87（4）元变量的替换;（5）推理的应用。推理是TASK L层的基本推理步骤，包括断言应用程序、证明规划方法或调用外部定理证明器或计算机代数系统（有关TASK L层的更多细节，请参见[14，6]）。形式证明需要将抽象证明步骤分解到CO REcalculus级别，将每个抽象步骤替换为一系列演算步骤。这通常有这样一种印象，即对于同一个猜想，一个正式的证明比一个相应的非正式证明包含更多的步骤。因此，如果我们手动构造一个正式的证明，许多交互步骤通常是必要的。相比之下，正式的证明草图[30其基本思想是，用户只写下证明中有趣的部分，这些步骤之间的空白稍后会被填补，理想情况下是完全自动的（参见[24]）。因此，证明草图对于像PLATΩ这样的调解人来说是高度相关的，其任务是支持从数学中的非正式证明过渡到完全正式的表示通过未指定的证明草图的中间表示来记录。3PLATΩ系统中介器PLATΩ被设计为作为特定文本编辑器的插件在本地运行，或者作为文本编辑器可以通过Web访问的数学服务提供者。为了管理不同的文本编辑器客户端以及同一客户端中的不同文档，我们将会话管理集成到PLATΩ中。文本编辑器可以请求唯一的会话密钥，它必须提供该会话密钥作为该特定会话中的任何进一步交互的参数P LATΩ通过一种非正式的表示语言与文本编辑器相连，这种语言可灵活地支持数学文档的通常文本结构。此外，这种语义注释语言，称为证明语言（PL），允许未指定以及替代（子）证明尝试。为了生成PL表示的形式对应物，PLATΩ将理论知识（如定义、公理和定理）与证明分开。理论用开发图语言（DL）形式化，它接近于MAYA系统支持的OMD理论语言，而证明则转化为任务层语言（TL），其描述T任务层的PDS实例。因此，PLATΩ与证明辅助系统ΩMEGA通过形式化的表示接近其内部数据结构。除了完整文档的转换之外，还必须能够将小的更改从非正式的PL表示传播到正式的DL/TL表示以及返回的方式。如果我们总是执行全局转换，我们一方面会在文本编辑器中重写整个文档，这意味着丢失用户编写的大部分自然语言文本另一方面我们将校对辅助系统的数据结构重置为校对草图的抽象级别。例如，任何已经发展到微积分的M. Wagner等/理论计算机科学电子笔记174（2007）8791图1. PLATΩ在自然数学文本和证明助手ΩMEGA级别或任何来自外部系统的计算结果将丢失。因此，我们建议，变化的最重要的方面之一。PLATΩ的架构是传播形式表示最终允许底层的证明辅助系统以各种方式支持用户。 PLATΩ提供了相互作用通过上下文敏感的服务菜单。如果用户选择文档中的对象，则PLATΩ从证明辅助系统请求关于所选对象的正式对应物的服务动作。因此，中介者需要维护非正式语言PL和正式语言DL和TL中的对象之间的映射。特别地，证明辅助系统可以通过针对特定证明情形建议可能的推理应用来支持用户。由于所有推理参数实例化的计算可能需要很长时间，因此需要具有惰性评估可能性PLATΩ支持在服务菜单内执行嵌套操作，这可能会导致更改描述这个菜单。通过服务菜单，用户可以访问自动定理证明器和计算机代数系统，这些系统可以自动验证结论和计算，并提出可能的更正。这些以及更多的功能都得到了PLATΩ的支持，通过其机制来传播更改以及向文本编辑器的用户提供自定义答案的可能性。总而言之，中介PLATΩ旨在支持在高抽象级别上的数学文档的交互式开发。3.1平板ΩPLATΩ提供了文本编辑器和证明辅助系统的抽象接口（另见图1）。①的人。在讨论它们的设计和实现之前，我们首先介绍这些方法的功能是：从文本编辑器的角度来看。PLATΩ's• 初始化会话：plato：init在PLATΩ92M. Wagner等/理论计算机科学电子笔记174（2007）87• 上传一个文档：plato：upload用信息语言PL上传一个完整的文档，从这个文档中，PLATΩ建立了形式化的表示DL和TL。 如果文档已经上传，则P LATΩ使用基于语义的差异机制[ 22 ]执行内部差异分析，然后就像修补文档一样进行。• patchadocument：plato：patch使用XUp日期标准中给出的补丁信息，以非正式语言PL为已经上传的文档打补丁(see第3.2节）。PLATΩ将此补丁信息转换为形式表示DL和TL，用于修补证明辅助系统。• Request a menu：plato：service在文档中以非正式语言PL为对象请求菜单。响应是服务中的菜单语言SL（或错误消息）。PLATΩ使用其可映射的相关对象在PL中使用DL和TL中的对象来请求来自证明的服务支持为后者提供援助。• 执行菜单操作：plato：execute触发一个带有实际参数的操作的执行。结果可以是当前菜单的补丁、文档的补丁或自定义答案（或错误消息）。目的是计算菜单中的操作。这种类型的响应提供了相当多的交互可能性：如果选定的操作嵌套在菜单中的某个位置，证明辅助系统通常会修改菜单。这将由PLATΩ传播到相应的响应，该响应仅修改菜单并将文档的补丁和自定义答案留空。 如果所选择的如果操作位于菜单的顶层，则在证明辅助系统中的执行将更有可能改变形式表示。无论如何，PLATΩ会将这些更改推广到文本编辑器的非正式表示中的更改，因此响应通常会删除菜单并适当地修补文档。自定义答案为任意交互可能性留下了空间比如知识检索或自然语言反馈。• 关闭会话：plato：close终止会话。附录A给出了PLATΩ3.2与文本编辑和校对辅助系统的PLATΩ的目标是为文本编辑器界面奠定兼容的基础在不同的环境中。它应该是一个干净的、可扩展的接口，简单且易于实现，因此它可以快速适应任何操作系统上的任何科学文本编辑器。因此，我们决定用XML[11]表示数学文档和服务菜单，对于XUp日期更新语言中的文档和菜单[20]，并使用XML-RPC[31]作为接口协议。XUpDATE[20]是一种XML更新语言，它使用XML对其更新进行编码，并使用表达式语言XPATH[10]来选择要处理的元素。更新可以包含与PLATΩ相关的以下类型的元素：insert-before、insert-after、append、update、remove。所有M. Wagner等/理论计算机科学电子笔记174（2007）8793更新中的操作必须并行地应用于目标文档。XML-RPC是一种远程过程调用协议，它使用XML对其调用进行编码，并使用HTTP作为传输机制。它是一个非常简单的协议，只定义了少量的数据类型和命令，其完整的两页描述可以在[31]中找到。ΩMEGA系统在LIS p中实现。因此，我们决定实现ΩMEGA的接口，它为每个PLATΩ方法提供LIS p函数，其中L也是 p。这些函数只对数学文档的形式表示进行操作，它们将在下一节中更详细地说明。PLATΩ允许为同一个证明辅助实例并行启动、停止和管理多个服务器。 一般来说，我们的目标是一种独立于要整合的特定证据辅助系统。因此，证明语言以及服务菜单语言在定义、公式、引用和菜单参数内容的子语言上被参数化扩展这些子语言允许在表示能力以及服务功能方面扩展整个系统的能力一旦自然语言分析领域取得 因此，PLATΩ被设计为支持进化的基础证明辅助系统朝着一个理想的数学辅助系统在下一节中，我们将介绍这一更普遍观点的更多方面。然而，重点是将ΩMEGA系统集成到科学的WYSIWYG文本编辑器TE XMACS中。4一个工作示例在本节中，我们将结合ΩMEGA来评估介体PLAT Ω和TE XMACS。我们将举例说明简单集合理论中所有可用的样例方法。PLATΩ通过讨论a在本文中，我们描述了在文本编辑器中的非正式表示和证明辅助系统中的正式表示之间的中介。关于本示例的通信文档、补丁描述和菜单的所有详细信息，请参见[28]。由于TE XMACS证明辅助系统的接口正在持续发展的PLATΩ plugin for TEXMAcS由ΩMEGA一个组，它将PLATΩ的接口函数映射到TE XMACS的当前接口函数，并为TEXMACS中的PL宏定义一个样式文件。在下面的例子中，我们使用这个插件在TEXmacS和PLATΩ首先，文本编辑器TE XMACS方法创建新会话方法plato：init和客户端名称一起，例如 的所得到的会话名称必须由文本编辑器保存，以便将其用于与PLATΩ的后续通信。在文本编辑器中，我们使用语义注释语言PL（定义见[28]）编写了一个示例文档。本文档中的简单集合理论94M. Wagner等/理论计算机科学电子笔记174（2007）87图2.TE XMACS中的单集理论包含例如子集，集合=，并集和交集的定义和公理。图2示出了如在TE XMAcS中所见的理论，图3示出了该理论的编码。理论中的TE X宏与PLATΩ宏。此外，我们还写了一个简单集合中的分配性理论，它从第一个简单集合理论中引入了所有知识。这第二个理论包括一个定理的分配性的交集。 用户已经通过引入两个子目标开始了这个定理的证明。图4示出了在TE XMAcS中看到的理论，图5示出了该理论在TE XMAcS中的编码。通过按下键盘快捷键，用户始终可以轻松地在这两个视图都在文本编辑器中。文档中包含的PL宏必须是M. Wagner等/理论计算机科学电子笔记174（2007）8795图3. 理论简单集在TE XMACS中的编码由用户2提供并用于自动提取相应的PLdocument，PLATΩ的文档将本PL文档与plato：upload，PLATΩ分离理论知识，如定义，公理和定理从证明，并开始生成，正式代表。一方面，PLATΩ创建了一个DL文档，其中包含接近OMDO c的定义、公理和定理。另一方面，证明被转换成一个TL文档，一个抽象的表示为PDS实例的T问 L层的证明辅助系统。从DL文档中，ΩMEGA的PLATΩ实例生成了一个理论2目前，这仍然需要一些关于PL和TE XMAcS宏语言的专业知识。今后的工作包括为这项任务提供更好的支持。96M. Wagner等/理论计算机科学电子笔记174（2007）87图4. TE XMACS中单集的理论图5. 简单集理论分配性在TE XMACS中的编码表示，MAYA将其作为用于创建开发图的输入。图6显示了上传的理论，单位为Ω。对于该评估，我们使用旧的用户界面LΩUI [25]来可视化ΩMEGA的状态。用户当然只与文本编辑器交互。旧的LΩUI界面，包括MAYAPLATΩ. 在本文中，它们仅被呈现以显示内部表示通过PLATΩ从TE XMACS获得在TL文档中，ΩMEGA的PLATΩ实例构建了TASK L层的具体数据结构（见图10）。7）。上传过程已成功终止，证明辅助系统中的形式表示已完成生成，因此PLATΩ返回M. Wagner等/理论计算机科学电子笔记174（2007）8797图6. ΩMEGA中的单集理论图7. ΩMEGA中交的分配性定理的部分证明进一步开发文档，用户已经开始通过导出新的子目标并引入假设来证明第一个子目标（见图2）。8）。这一修改--文档编码的阳离子（见图9）必须通过PLATΩ传播到Ω中的形式表示。 一般来说，在以下方面的差异98M. Wagner等/理论计算机科学电子笔记174（2007）87图8. 用户对TE XMACS中证明的图9. 用户对TE XMACS应计算文档的最后一个同步版本并将其发送使用plato：patch实现plat Ω。此时，TE XMACS无法计算此差异，因此整个文档由plato：upload再次发送，PLATΩ计算差异。非正式PL文档的差异然后通过PLATΩ转换为DL和TL中的正式表示的差异。由于这些修改并不涉及理论知识，因此这种转换只会导致中间表示的修改，最终导致TASK LAYER证明数据结构的表示。ΩMEGA的PLATΩ实例使用此补丁信息来修改TASK层，而不是从头开始完全重建它（参见图10）。贴片M. Wagner等/理论计算机科学电子笔记174（2007）8799图10. PLATΩ对ΩMEGA证明的图11.用户请求的TE XMACS程序已成功终止，因此PLATΩ返回总之，用户能够同步他的非正式表示在文本编辑器文档中的正式表示在证明辅助系统。100M. Wagner等/理论计算机科学电子笔记174（2007）87图12. 用PLATΩ修改TE XMACS图13. 系统对ΩMEGA证明的PLATΩ的下一个有趣的特性是从底层证明辅助系统获得系统支持的可能性选择假设中最近引入的公式，用户从PLATΩ请求服务菜单M. Wagner等/理论计算机科学电子笔记174（2007）87101图14. 用PLATΩ修改TE XMACS请求T请求层中的对应任务的服务，可用推断的列表被返回到P请求层。为了快速响应文本编辑器，我们生成嵌套的操作，允许增量计算公式由应用推理而不是为所有可用的推理预先计算所有可能的结果公式而产生。对于该示例，在证明辅助系统中手动生成推断，因为从开发图中的理论知识自动推断生成仍在开发中。菜单将以TE XMAcS格式显示给用户如图11所示，其中我们已经扩展了应用交叉点定义的操作-到其嵌套操作计算结果。执行Compute Results调用方法plato：executeinPLATΩ，这导致在TASK L层中计算所有结果公式，用于推理定义交集-，定义为对应的公理。PLATΩ告诉文本编辑器如何更改菜单，发送菜单的补丁描述。用户选择所需的公式（见图12），这将触发应用程序并启动一个plato：execute。PLATΩ调用TASK层，用于应用选定的推理以获得选定的公式。TASK层执行所请求的操作，该操作通常修改证明数据结构（参见图13）。 此修改由PLATΩ实例为ΩMEGA转化为补丁描述，用于TL中的正式表示。之后，PLATΩ将该TL补丁转换为IL补丁，并最终将PL补丁转换为TEXMAcS中的非正式文档，然后将其发送到文本编辑器。此外，通过发送一个补丁描述来关闭菜单，该补丁描述将删除该菜单。目前，新的证明片段与额外的预定义自然语言片段一起插入然而，我们计划集成自然语言证明呈现系统P。REX[15]转换为P LAT Ω，以便为证明辅助系统添加的证明步骤生成真正的自然语言输出。102M. Wagner等/理论计算机科学电子笔记174（2007）87图15. PLATΩ对TE XMACS证明的文本编辑器最终根据该补丁描述对文档的编码进行补丁（参见图14）。图15示出了在TEX mac中显示的打补丁的文档。请注意，用户可以更改文档的任何部分，包括由证明辅助系统生成。由于版本的一致性维护，文档的进一步开发可以是用户手动创作和与校对辅助系统的交互式创作的混合最后但并非最不重要的是，关闭文档或文本编辑器将通过调用方法plato：close关闭P LAT Ω和证明辅助系统Ω MEGA中的活动会话。 对于这个评估，我们选择了一个简单的数学域，关注中介的系统行为。一般来说，问题解决能力只依赖于底层的证明辅助系统。尖端的证明援助，可以通过扩展复杂领域的代表性子语言。5相关工作Nicolas de Bruijn的AUTOMATH项目[13]和他的数学白话的想法必须被称为该领域的开创性工作。与AU-TOMATH类似，MIZAR3和ISAR[29]项目旨在实现良好的平衡在适合机器处理的严格的形式化表示语言和人类可读的自然表示之间。“语法框架”方法（GF）[ 23 ]更进一步，采用基于λ -演算的形式主义来定义由抽象和具体语法组成的 抽象地3www.mizar.orgM. Wagner等/理论计算机科学电子笔记174（2007）87103语法人们可以形式化地表示数学定义、定理和证明，并检查它们的正确性，而具体语法定义了从抽象语法到语言对象的映射。这些方法的一个共同问题是 对 机 器 和 用 户 侧 的 表 示 的 不 同 要 求 。 一 个 UTOMATH 以 及 MIZAR 和ISARsacrifice可读性，以获得机器程序。兼容性。相比之下，GF显示出高可读性和机器加工性但是支持的自然语言片段太小，而且不灵活，不允许数学家使用他们熟悉的语言。许多数学辅助系统在试图增强可读性的同时，更倾向于机器处理能力而不是人类创作这是通过分离输入和输出语言来实现的例如，系统PcO q[2]使用示意性方法以准自然语言表示其输出。系统NUPRL[16]，CLAM[1]和Ω MEGA/P.REX[15]更进一步，使用自然语言处理技术，以生成真正的自然语言输出。[12]第十二话是一个严格区分数学文献中的非正式部分和正式部分的系统：用户可以不受任何限制地输入文本的非正式部分，但这些部分不用于机器处理。然而，形式部分必须用计算机代数系统MATHEMATI cA的输入语言编写。与此相反，我们建议在我们的方法[7]一个正式的表示兰-脱离任何特定逻辑或演算的数学内容的语言这允许我们表示任意内容，而不管底层逻辑如何。此外，该语言允许我们表示概念和欠规范的不同层次，因此特别适合于表示由人类以自然方式与我们的方法密切相关的是MATH-LANG项目[18]。它还提出了一个自上而下的方法，从自然开始，数学教科书中的机器加工。然而，到目前为止，MATH LANG项目主要集中在支持抽象表示的分析上与我们的方法相反，真正的定理证明和数学辅助工具之间的差距仍然是开放的。据我们所知，还没有任何尝试将证明辅助系统与文本编辑器以灵活的方式集成在一起，就像通过PLATΩ所做的那样。上述所有方法都没有将输入文档视为独立的一等公民，其内部状态必须与证明辅助系统中的正式表示保持一致，同时允许各方进行任意更改。在这个方向上唯一的工作已经进行的背景下，P屋顶一般[3]。在PROOF G中，用户通常以合适的格式编辑中心文档。编辑环境，从该编辑环境中，可以通过各种工具来评估该文档，例如检验文档是否包含有效校样的校样助手，或者将文档排版或呈现为系统可读的面向人类的文档的呈现器。然而，该系统只是一个接口，证明辅助系统，处理他们的输入增量。 因此，文件通常以自上而下的方式递增地处理，特别是已由校对辅助系统处理的部分被锁定104M. Wagner等/理论计算机科学电子笔记174（2007）87并且不能由用户编辑。此外，文档是在校对助手的输入格式中，而不是在一些排版程序的格式中。虽然我们已经尝试在PLATΩPLATΩ可以很容易地适应不同的证明助理，因为已经是可能的P屋顶G一般。6结论主要贡献是设计和开发一个通用的调解人，称为P拉特Ω，文本编辑器和证明辅助系统Ω兆之间。本中介允许用户用他习惯的语言编写他的数学文档，即自然语言和公式的混合。这些文档通过使用灵活的参数化证明语言。 PLATΩ自动建立相应的响应ΩMEGA中的形式表示，并进一步注意维护同时提供一种在两种表示之间传播更改的机制。底层证明辅助系统关于形式表示的各种服务可以通过上下文敏感的服务菜单通过PLAT 总而言之，PLATΩ有助于证明辅助系统向理想的数学辅助系统的演变。在本文中，我们已经说明了如何在文本编辑器中开发的非正式的，自然的证明映射到ΩMEGA中的正式表示。这个映射是否已经意味着非正式证明是有效的？显然不是，因为Ω兆证明草图在T问 L层可能是不健全的，只有充分扩大这些CO RE-演算层的证明草图将确保可靠性。在我们的方法中，这种扩展可以理想地通过ΩMEGA然而，这显然取决于非正式的结构质量和粒度。证据当然，如果非正式证明是错误的，扩展将失败，需要与用户交互来修补证明引用[1] 玛丽安西·阿莱克索迪克劳斯·津恩和艾伦·邦迪数学证明的英文摘要。InChri s tophenzmüllerandWolf gangWind s tei ger ， editors ， SecondInte rnationalJointConfernceon Automated Reasoning - Workshop onComputer-Supported Mathematical Theory Development ， pages 49 -6 0 ， U n i v e r s i t yCo l l e g eCo r k ， Co r k ， Ir e l a n d ， 2 0 0 4 .[2] Ahmed Amerkad，Yves Bertot，and Laurence Rideau.在Pcoq中的数学和证明演示。In Uwe Egly，ArminFiedler， Helmut Horacek， and Stephan Schmitt， editors ， Proceedings of the Workshop on ProofTransformation，Proof Presentations and Complexity of Proofs（PTP-01），pages 51-60. 2001年，在意大利，我看到了一个很好的例子。[3] David Aspinall，Christoph Lüth，and Burkhart Wol.辅助证明文件创作。Michael Kohlhase，编辑，数学知识管理MKM 2005，第3863卷，人工智能讲义，第65- 80页施普林格，2006年。[4] S. 奥 特 西 耶 CO RE 演 算 。 In R. Nieuwenhuis ， editor ， Proceedings of CADE-20， LNAI 3632 ，Tallinn，Estonia，July 2005. 斯普林格。M. Wagner等/理论计算机科学电子笔记174（2007）87105[5] SergAutexierr、Chri s tophBenzmu？llerr、Domi nikDie trich、AndreasMeierr和Claus-Pe terWirth。一个通用的模块化数据结构的证明尝试交替的想法和粒度。Michael Kohlhase，编辑，Proceedings of MKM斯普林格。[6] 塞尔日·奥特西耶和多米尼克·迪特里希。从数学知识综合证明规划方法和代理。在Jon Borwein和BillFarmer，编辑，MKM'06会议记录中Springer，2006年8月。[7] Serge Autexier和Armin Fiedler。教科书证明符合形式逻辑-未指定和粒度的问题。Michael Kohlhase，编辑，Proceedings of MKM斯普林格。[8] Serge Autexier和Dieter Hutter。玛雅的正式软件开发。在Dieter Hutter和Werner Stephan的编辑，纪念J。 Siekmann，LNAI的第2605卷。Springer，2005年2月[9] CHR。 Benzmülle rrandV. 好吧。Ω an t s-a nop e n apr o a t c o m b i n g i n t e r a t c o m i n g i n t e r a t c o m in g i n t e r a t c o m i n t e r a t c o m i n g i n t e r a t c o m i n g i n t e r a t c o m i n t e r a t c o m i n g i n t e r a tc o m i n t e r a t c o m i n g i n t e r a t c o m i n g i n t e r a t c o m i n t e r a t c o m i n t c o m i n g i n t e r a t c om i n t e r a t c o m i n t c o m i n g i n t e r a t c o m i n t c o m i n t e r a t c o m i n t c o m i n g i n t e r a t c o m in t eIn M.Kerber和M.Kohlhase，编辑，Proceedings of Calculemus-2000，St.2001年8月6日至7日，联合王国安德鲁斯。AK彼得斯。[10] A. Berglund，S. Boag，D. Chamberlin，M. F.费尔南德斯，M. Kay，J. Robie，and J. Simeon. Xml路径语言（xpath）2.0，2005。 http://www.w3.org/TR/xpath20。[11]T. Bray，J. Paoli，C. M. Sperberg-McQueen，Eve Maler，and Francois Yergeau.可扩展标记语言（xml）1.0（第三版），2004年。 http://www.w3.org/TR/REC-xml。[12] B. Buchberger，T. Jebelean，F. Kriftner，M. Marin，E. Tomuta和D.瓦萨鲁Theorema项目的概述。国际符号和代数计算研讨会论文集Press.[13] 尼古拉斯湾德布鲁因 数学语言AUTOMATH，它的用法和它的一些扩展。 自动演示研讨会，第29-61页[14] 多米尼克·迪特里希ΩMEGA系统的任务层。毕业论文，萨尔大学，Saarbruécken，Germany，2006年。[15] 阿 明 · 费 德 勒 用 户 自 适 应 证 明 解 释 。 博 士 论 文 ， Naturwissenschaftlich-TechnischeFakultéatI ，UniverrsitéatdesSaarlandes，Saarbruücken，Germany，2001年。[16] 阿曼达·M Holland-Minkley，Regina Barzilay，and Robert L.警官高级形式证明的语言化。第十六届全国人工智能会议（AAAI-99）和第十一届人工智能创新应用会议（IAAI-99），第277-284页。AAAI Press，1999.[17]黄晓蓉。以人为本的证明呈现：一种重建方法。第112章在沙漠里In fix，Sankt Augustin，德国，1996年。[18] F. Kamareddine，M. Maarek和J. B.井 面向对象的数学文本结构。In M.Kohlhase，editor，MKM 2005，Fourth International Conference on Mathematical Knowledge Management ， LNAI 3863 ， pages217施普林格，2006年。[19] 迈克尔·科尔哈斯OMDOC：为数学知识的管理、分发和教学建立互联网标准。在John A. Campbell和Eugenio Roanes-Lozano，编辑，人工智能和符号计算（AISC-00），LNCS1930卷。Springer，2001年。 http://www.mathweb.org/omdoc。[20] 安 德 烈 亚 斯 · 劳 克 斯 和 拉 尔 斯 · 马 丁 。 Xupdate xml update language （ 工 作 草 案 ） ， 2000 。 http ：org.sourceforge.net/xupdate。[21] A. Meier和E.梅利斯MULTI：一个多策略的证明规划器。In R.Nieuwenhuis，editor，Proceedings ofCADE-20，LNAI 3632，Tallinn，Estonia，July 2005.斯普林格。[22] 斯维特拉娜·拉泽维奇基于语义的xml文档查询、修补和合并。硕士论文，萨尔大学，Saarbrücken，Germmamny，2006年。[23] 奥恩·兰塔语法框架-类型理论语法形式主义。Journal of Functional Programming，14（2）：145[24] J？rgSie kmann，Chri s tophBenzm？ll er，ArminFi edl er，Andre as M eier，andndM ar tinPoll ett.使用OMEGA：102进行开发是不合理的。 在Matthias Baaz和Andrei Voronkov（编辑）的《逻辑编程、人工智能和推理》（第9届国际会议，LPAR 2002）中，编号2514，LNAI，第367-387页。施普林格，2002年。[25] J？rgSie kmann，StephanHes ss，Chri s tophBenzm？ller，Las s aadCheikhrouhou，ArminFie dler，HelmutHoracek，Michael Kohlhase，Karsten Konrad，Andreas Meier，Erica Melis，Martin Pollet，andVolker Sorge. LΩUI：可爱的Ωmega用户界面。Formal Aspects of Computing，11：326106M. Wagner等/理论计算机科学电子笔记174（2007）87[26] 诉 抱 歉 一 个 将 推 理 技 术 集 成 到 证 明 规 划 中 的 黑 板 架 构 。 P hDthesis ， FR6. 2Inform atik ，UniversitüatdesSaarlandes，Saarbruücken，Germamani，No