连接逻辑表示和高效计算

理论计算机科学电子笔记151（2006）127-142www.elsevier.com/locate/entcs连接逻辑表示和高效计算马丁·波利特FachereichInforormatik，Uiv ersitüatdesSaarlanddes，Germany我知道了。联合湾网址：http：//www. 一个g s。联合湾d e/~ po llet沃尔克·佐尔格英国伯明翰大学计算机科学学院V. Sorge@cs. bham. AC. 网址：http：//www. cs. bh am. AC. uk/~ vx s摘要当逻辑层次定理证明与计算方法相结合时，重要的是要确定可以有效计算的函数和它们可以应用的对象。 这 通常通过将逻辑级项和函数映射到它们的计算对端来实现。然而，这些映射往往是非常特别和脆弱的，这在很大程度上取决于特定的逻辑表示的条款。本文提出了一种利用计算性质标注逻辑证明中术语的方法。这使得在演绎系统中的计算对象的紧凑表示以及它们与可以容易地为它们计算的函数的连接成为可能。这简化了可以通过计算方法有效处理的演绎问题的识别，并且还从作为特定表示的人工制品的平凡属性中抽象出来。我们确保我们的概念的逻辑正确性，提供了可能性，以取代他们的逻辑表示的条款，并通过扩大计算程序的战术应用，可以严格检查。关键词：计算与推理，数学知识表示，注释术语1介绍在演绎系统中数学对象的表示往往受到特定系统的形式主义和逻辑要求的影响。例如，自然数通常用零的后继来表示，或者通过构造函数递归地连接数字列表。虽然这些表示通常适合于推理1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.027128M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127抽象数学概念的性质，它们在处理具体对象时常常是一个障碍，即，抽象概念的实例及其计算属性。这些表示不仅常常与非正式的数学术语相分离，而且与适合于直接计算操作的表示相分离。此外，在复杂的公式中自动识别这些对象通常已经很困难。当我们看一下数学中的典型表示时，似乎关于对象的信息被附加到对象本身。 它从字母的选择开始：a似乎是集合A中元素的一个比任何其他字母更好的符号，大写字母表示集合，G代表在群论的背景下，n和m是“典型的”任意自然数。形式系统能够通过使用类型将这种信息附加到对象上，并且可以通过它们的类型来识别对象或属性。其他表示更难建模，例如，运算的结合性通过忘记括号来记住，'+'用于不同的类似加法的运算。[1]这些观察表明了一种更面向对象的方法：即，将关于对象的信息存储在对象本身，而不是在分离的过程中，例如，接口。这也简化了某些对象的识别，例如在复杂的公式中，以及将对象上的信息重新用于不同的目的。为了捕捉与某些数学表示有关的信息，我们引入了注释常数的数据结构[14]（见第二节）。3）。 它处理特定的对象类，这些对象在逻辑语言中作为术语给出，但从数学的角度来看应该被视为常量。带注释的常量用包含实际对象信息的逻辑常量替换术语作为注释。注释一方面允许重构原始对象，如果它是必要的，在形式证明。另一方面，它使识别的对象通过专门的证明规则，以及执行有效的操作和计算的对象表示。我们将在第二节中给出两个由注释常量捕获的数学概念二、我们已经在Omega证明开发环境中实现了几类带注释的常量[13]，以简化自动证明构建，主要是在证明规划场景中。除了简单的对象，如数字，列表和集合，我们还尝试了更复杂的对象，如矩阵[15]和排列[4]。特别是，当自动验证计算机代数算法在欧米茄大量的具体的验证，1重载允许重用符号，但无助于重用关于符号的知识。M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127129使用带注释的常量可以有效地处理ical对象。不幸的是，可以由当前形式的带注释常量处理的对象范围仅限于具体术语，即不包含变量的术语。然而，通常希望还将包含变量的项标识为特定的数学对象。例如，我们希望区分表示有限集合的对象，即使它们包含变量，以便对它们执行有效的集合操作。因此，我们将注释常数的概念扩展到注释术语（Sec.4）允许有变量的项，并显示这对可以对它们进行的计算的一些影响。由于我们的具体实现是在Omega系统的逻辑框架内-一个简单类型的lambda演算（参见。[1]）-我们将在这个形式主义中提出我们的例子。然而，带注释的常数和项的一般概念不限于特定的逻辑系统。2两个例子我们首先检查两个例子来激发我们的概念的注释常数。通常的演绎系统依赖于有限签名的使用一组有限的常量、函数和谓词符号。因此，无穷多组常数通常是递归构造的，这意味着单个对象是根据它们的构造给出的，而不是从数学的角度来看它们实际上是常数。这一事实使得这些对象不仅处理起来麻烦，而且常常难以识别。虽然有些对象，如整数或列表，即使嵌入复杂的术语中，仍然可以相当容易地在其形式逻辑表示中识别，但对于其他构造，这并不那么明显。例如，在lambda演算中，有限集合通常表示为包含等式的析取的lambda项。{a，b，c}形式的集合表示为λx（x=a<$x=b<$x=c）。现在，一个lambda项是否真的表示一个有限集并不一定是显而易见的。此外，集合之间的相等性与其元素的顺序无关。然而，lambda表达式的（语法）相等性取决于顺序。另一个例子是矩阵的形式表示。矩阵的数学定义例如在[11，p.441]中给出“By130M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127的R，（a ij），（i = 1，.，m并且j= 1，.，n），通常以如下形式书写. a11···a1n···am1···amn我们把元素aij称为矩阵的系数或分量。将这个定义转换为正式的表示是简单的。根据具体的逻辑语言，我们可以将矩阵视为由双索引函数、行数、列数和底层环组成的元组。对于一个具体矩阵的实例，我们可以用下面的方式给出函数a：i，j−→. 3，如果i=j<$i∈[1，2] 1，如果i= 1 <$j= 21，如果j= 1，则i =2.其中（aij）=Σ3个1 .1 3虽然左侧的函数表示足以描述矩阵，但它已经丢失了右侧实际矩阵表示隐含的信息：该定义将表示引入为矩形形式，其中矩阵的元素相对于其索引进行排序，以使相关信息直接可访问并简化推理。然而，如果我们在lambda演算中观察上述矩阵的一个表示，使用if-then-else构造[λi，jif（i=j<$（i= 1<$i = 2））then3else 1]，这就不再明显地能够定义矩形结构。其他明显的信息，如对称性，也不太容易在lambda项。甚至访问矩阵的组件也需要相当多的推理。虽然通过添加一些语法糖和复杂的翻译和显示设施，仍然可以处理由具体数学对象的粗略形式表示所引起的一些问题，但在术语水平上的处理仍然很困难。特别地，对于自动化系统（例如，自动定理证明器、证明计划器或计算机代数系统），自动区分公式的哪一部分构成具体的数学对象而哪一部分不构成具体的数学对象就成了问题。当我们想要避免在不遵守约束条件的情况下操作函数表达式而产生语义上不正确的表达式时，这一点尤其重要。虽然子列表通常可以被替换而不违反其他属性，但矩阵表达式的操作需要显式地保留对象的矩形性质。因此，如果某些项或子项可以被明确地标记为必须遵守某些附带条件的具体的抽象对象，则是有帮助的。我们通过以下方式实现这一目标：M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127131使用带注释的常量。3注释常量对象注释常数是一种提供表示层的机制，该表示层既可以捕获计算对象的直观数学表示的属性，也可以将这些对象连接到形式逻辑框架中的相应表示。注释常数在Omega系统[13]中实现，并且对于简单对象（如数字和列表）进行了更特殊的处理，但也适用于更复杂的结构，如置换[14]，矩阵，块矩阵和包含椭圆的矩阵[15]。为了清楚起见，我们在下面使用有限集合的更简单的例子来解释这个想法。3.1注释常量给定一个逻辑语言L，一个常数符号c∈ L和一个基项t∈ L，使得c=t。然后我们定义一个带注释的常数为三元组（c，t，a），其中a是注释。注释a是可以从中重构c和t的任何对象（使用任意数据结构）。把c看作对象的名称，t看作逻辑内部的表示，a看作逻辑外部的对象的表示。这个想法是，a是我们感兴趣的某个计算对象，它应该被视为某个常数对象。然而，它在逻辑语言中的实际表述是t，它通常不是常数。因此，为了将t区分为逻辑语言中的计算对象，它被常量替换为C.带注释的常数（c，t，a）允许我们通过使用注释a来有效地计算c，并保证我们可以通过用t替换c来重新获得完整的逻辑形式化。作为一种类型的注释常数的例子，我们考虑有限集。有限集合在数学术语中有一个特殊的符号，例如，由三个元素a，b和c组成的集合用{a，b，c}表示。我们可以通过给集合一个名字来定义它，例如，A，以及逻辑中作为基础项的定义关于集合的重要知识是：集合是相等的，如果它们包含相同的元素，而不考虑它们的顺序，或者两个集合的并集由其中一个集合的成员元素组成，等等。这种类型的集合操作与逻辑推理没有太大关系，因为它与计算有关。例如，两个集合的并集可以非常有效地计算，不应该是寻找证明过程的一部分有限集合的注释常数用属性定义132M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127常量符号：我们给集合起一个名字，比如A。更适合我们的目的是从集合元素的重复自由排序中生成一个标识符，例如A{a，b，c}。定 义 ： 集 合 的 定 义 对 应 于 高阶逻辑中的 lambda 项 ， 例 如 ， λx（x=a<$x=b<$x=c）。为了规范化这些项，对集合中的元素进行排序是有用的，也就是说，我们由于注释必须完全表示对象，因此可以从注释中构建形式定义有限集合的注释：底层编程语言的集合的数据结构被用作注释，并且集合的元素被限制为封闭项，例如，该集合在具体示例中包含三个常数a、b和c我们使用注释以标准的数学符号表示概念，并且注释作为用户的输入给出常数符号及其定义根据注释选择。这意味着集合{a，b，c}和{c，b，a}将由相同的常量符号表示，因为注释是相等的。有了这种机制，就有可能在我们的对象逻辑中实现注释常量上的平凡等式作为语法等式。处理带注释常量的基本功能是在Omega系统的术语级别上实现的。在第一近似中，注释常数是具有定义的常数，并且具有其定义项t.因此，它可以在证明过程中或在扩展证明以检查形式正确性时被其定义项取代。通常情况下，这是不这样做的，但注释的常量是通过它们的注释来操作的。注释术语的定义术语仅在必要时使用3.2注释函数既然我们有了一个在逻辑项级别上可用的计算对象的简明表示，我们就可以利用它来有效地操纵对象。在我们最初的方法[14]中，带注释的常量可以通过特殊的策略进行然而，这限制了对注释常数的可能操作的检测，以实际证明过程的危险另一种方法是标识可以对特定类型的带注释常量进行操作的函数和谓词，并使用附加的计算信息对其进行增强这些信息随后可以用于操作注释常数和验证其属性。我们通过引入过程注释来实现这一点，如下所示：M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127133是逻辑语言L的一个函数或谓词。过程注释是一个三元组（f，T，p），其中p是底层编程语言的过程，具有与f相同数量的参数，T是用于构造p执行的操作的形式证明的规范（或策略）。定义与注释常数的定义相同，即f为来自L的常数函数符号，p是注释，T是p的形式对应物。然而，注意到T的作用不同于t对于带注释的常数的作用，因为T是基础演算的证明策略，而不是逻辑语言L的元素。使用过程注释的操作可以通过直接使用过程p来执行。它检查其参数，执行简化，并返回一个简化常数或项以及该操作的可能条件。然而，这导致了一个证明步骤，本质上是微积分层面上更复杂推理的缩写。此外，由于p可以是任何过程，因此不能保证其正确。因此，有必要在随后的步骤中使用证明规范T正式证明计算的正确性。从而将一个带注释的常数扩展到其形式定义，并通过策略和定理应用重建计算。这种扩展只在需要低级形式证明时才进行，当然不在证明搜索期间。作为一个例子，我们考虑具体集合的并集的过程函数：集合上的联合函数定义为：E_∞=（λS，T， xSx<$Tx）。这意味着，在我们的逻辑语言中，是一个常量符号，可以应用于任何两个集合，而不管它们的形式如何。然 而 ，我们现在可以注释并集，这样当应用于表示有限集合的注释常数时，可以有效地计算并集。例如，当{ a，b }和{c，d }时，我们希望能够计算并集{a，b}{c，d}。{c，d}是带注释的常量。过程注解：计算由具体元素给出的两个有限集合的并集的过程p。p首先检查参数是否是表示有限集合的注释常量。如果是这种情况，p将计算为两个集合的无重复连接，并将其作为新的注释常数返回以插入证明中。对于具体示例{a，b}{c，d}，过程检查参数是否为具体集合的注释常量，并返回具有{a，b，c，d}串联的注释常量作为注释。策略：策略T通过将p的计算扩展到逻辑级计算来扩展p的计算它首先在其参数中用定义替换了常数和注释常数，然后将低水平应用于-134M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127规则来构建联盟。对于具体的例子，T用适当的lambda项代替{a，b}<${c，d}，得到（λS，T，x Sx <$T x）（λx x = a <$x = b）（λxx = c <$x = d），然后应用β-归约和可能的逻辑连接词的重新排序，得到结果集合λx x = a<$x =b<$x= c<$x = d。在本例中，程序注释仅替换了定义扩展和β-归约步骤。这个过程的重要好处是，结果再次是一个对象，它立即被识别为有限集，而不需要进一步的分析。过程注释可以相对于不同类型的输入产生不同的输出。它们可以在参数之间进行区分，这些参数是项、常数、带注释的常数、特定类型的带注释的常数或具体常数的名称。该过程检查参数并选择最特殊的情况，其中任何项都是最不特殊的，而具体常数是最特殊的。例如，元素关系a1∈a2在以下情况下实现：(i) 如果参数a1是一个带注释的整数类型的常数，而a2是整数Z的具体常数，则它返回true。(ii) 如果一个1是一个项，一个2是一个带注释的常数，那么它会检查一个1是否等于一个2中的一个元素。过程注释被组合在评估策略中，该评估策略将连接到术语中包含的函数的过程注释应用于过程注释的输出，直到没有过程注释适用为止。当这种策略应用于公式{1， 2，}{ 2， 3}时，如果发现子集关系的注释是不适用的，因为它需要一个带注释的有限类常量集作为第一个参数，但第一个参数包含可以应用过程注释的集合的并集结果输出{1， 2， 3}Z再次被求值。这一次，子集关系的注释是适用的，它返回一个包含1∈Z，2∈Z和3∈Z的列表。每个公式再次被求值，元素关系的注释为每个公式返回true。这意味着评估策略是适用的，并且不返回进一步的证明义务。3.3讨论首先，注释常数提供了一个中间表示层之间的直观的数学白话和正式的系统。有了带注释的常量，就有可能从对象的正式介绍中抽象出来，允许识别某些类的对象，并直接访问关于对象的相关知识。注释可以M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127135在必要时，将其转换为完整的形式逻辑表达式，但使其有可能以从形式结构中抽象出来的方式与数学对象一起工作和推理。其次，注释允许用户友好的输入和输出设施。我们扩展了Omega的输入语言，为带注释的常量提供了标记，以指示它所表示的对象的类型。对于每一种带注释的常数，术语解析器都被一个附加的函数扩展，该函数解析注释并将这些注释转换为内部表示。在解析过程中，可以检查其他属性，并检测规范中的错误。这样就可以扩展语法类型检查。每种注释常量的附加输出函数允许具有不同的显示形式，用于向用户呈现公式。第三，过程注释使注释常量的有效操作成为可能。这些程序可以访问信息，而无需进一步分析（lambda）项（正式定义注释常数），并允许非常有效地计算标准函数和关系。这些操作和属性成为对带注释常量的数据结构的计算。4注释条款注释常量提供了一种机制，将具体的抽象对象编码为对象逻辑的常量，同时允许识别特殊对象，存储相关信息，并实现专门的推理技术。然而，由于实际的长期被替换为一个单一的常数在逻辑层面上的长期不允许- ted包含变量，因为这些将不再是证明建设期间访问。然而，我们也希望能够将包含变量的术语识别为某些类型的数学对象。 例如，在定理x，y x/= y中|{x，y}|= 2，我们想把{x，y}标记为有限集合，并在推理和应用定理时适当地处理它。由于我们不能使用注释常量，我们将通过使我们的对象逻辑可以访问我们的注释常量的组件，同时保留注释常量的大部分功能，特别是我们有效率的推理技术连接到特殊类型的数学对象，将概念扩展到注释术语136M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）1274.1“一般”具体对象建模对于一般对象，我们使用元组（f（a1，... ，a n），t），其中f是具有项a1，.，a n作为参数，t是表示f的定义的n元项。对于带注释的常量，有必要将相关信息作为注释附加到常量上，现在我们使用f来识别对象的类型，其具有1，...，n作为其分量。有限集：使用带注释的常量，我们将整个对象{a，b，c}编码为对象逻辑的常量现在我们用一个函数符号来标识有限集合。形式项：对于给定的元素数n，我们使用一个函数符号Sn，它将有限集合的元素作为参数。对于我们的例子，项S3（a，b，c）是有限集合{a，b，c}的形式表示。定义：在简单类型的微积分中，函数Sn可以定义为λx1，.，xn，y（y =x1···y = xn）.对于我们的例子，定义的扩展产生了项λy（y=ay=by=c对于带注释的常量，有限集合由用户输入的元素给出，在解析过程中，一个唯一的函数符号Sn被添加到签名中。不止一个函数符号的存在只是一个技术细节，只要我们能把任意n的Sn识别为有限集合的标记。形式项，特别是函数符号，并没有改变逻辑的基本形式。从对象逻辑的观点来看，函数Sn可以被看作是定义的占位符，但同时允许识别这个对象所属的范畴混凝土基质：类似于有限集合，我们引入函数符号来识别矩阵。形式项：对于维数为m×n的矩阵，存在一个m·n元函数M m×nwhichta kest.矩阵的元素是一个规则。他是为了马尔矩阵项3 2 71 0 4是M2×3（3，2，7，1，0，4）。定义：Mm×n的相应定义项是一个双指标函数，它包含了单个元素的所有情况，在我们的例子中，形式项将扩展为λiλj如果i= 1j= 1那么3elseifi= 1j= 2那么2elseifi= 1j= 3那么7elseifi= 2j= 1那么1elseifi= 2j= 2那么0elseif 4.M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）1271374.2功能随着形式表示从常量到项的变化，项可以被不知道特殊注释的策略操纵。因此，当策略想要访问注释时，必须从形式术语生成对象作为数据结构的这是不太有效的，但它避免了任意项的分析。对于包含具体数学对象的特殊表示，我们将注释的平凡等式表示为形式对象的语法等式，因为只要注释相等，我们就使用相同的常数。对于带注释的术语，我们必须在过程注释的机制中处理相等性，如第2节所述。3 .第三章。实现带注释常量的动机是某些对象类允许有效的推理技术，这对于扩展表示也是如此。 考虑简单问题（{1， 2，x}）{2， 3，y}）带有变量x和y的Z，它被赋予求值策略。有限集合的并集是一个创建由输入集合的重复自由成员组成的有限集合的过程。因为不知道x=y，所以这两个元素都出现在问题{1， 2，3，x，y}<$Z中。现在，有限集合的子集关系可以简化为有限集合的所有成员的元素关系。这是一个与有限集合有关的更一般的推理技术的例子：为了证明一个属性对有限集合的元素成立，检查集合中每个元素的属性。这种技术的适用性取决于集合的有限性，这可以直接用我们的注释术语来识别。对于i∈ {1， 2， 3}，得到的元素关系i∈Z是平凡的，因为整数由下式表示：注释术语。 然而，评估不能显示x∈Z或y∈Z，将两者作为新的子问题返回。由于变量的存在，我们现在可以在我们的表示上表达统一问题众所周知，纯粹的句法理论统一过程是不可判定的。另一方面，对于许多理论存在有效的算法。有了带注释的术语，我们就能够确定我们必须解决统一问题的理论。例如，对于有限集合，我们可以使用ACI统一的过程[6]。22有限集合可以用结合的、交换的和幂等的运算来建模。138M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）1275示例：排列置换是有限集合到自身的双射映射。虽然在数学中有不同的符号来表示排列，但循环符号通常是首选，并由计算机代数系统GAP使用在这种符号中，置换由无重复的不相交循环组成，即，lists（n1，.，nk），其中k≥ 1且ni i = nj，其中ii = j.循环将点n i映射到n i+1，其中i =1，.，k− 1和n k到n1。一个置换则是包含不相交循环的集合或置换的组合一个群G可以由生成置换G=p1，p2，.的列表来指定。，pk，并将置换的复合作为群运算。我们想把循环作为置换的注释，但是为了置换的形式化，我们必须决定循环是否只是置换的一个符号，或者循环是否是它右边的数学对象。在第一种情况下，一个用圈表示的置换对应于一个在对象语言中是双射的自身上的映射，在第二种情况下，一个对应于圈的对象必须在对象语言中被形式化由于圈的性质是定理的主题，我们决定选择第二种选择。详细地，循环被形式化为列表，置换被形式化为循环的集合或置换的组合，并且循环和置换都被应用运算符@解释为映射，该应用运算符@在其域中取置换和点，并返回图像。我们确定循环和排列，如果他们的应用程序在相同的映射结果。我们已经介绍了有限集合的注释，对于循环，我们介绍了以下注释。形式项：对于每个n，我们使用一个函数Cn，它的参数是循环的元素。例如，项C3（3， 1， 2）是循环（3， 1， 2）的形式表示。定义：一个循环被扩展为一个列表，其中cons作为列表构造函数，nil作为空列表，例如，C3（3， 1， 2）=cons（3，cons（1，cons（2，nil）。当一个对象是包含不相交循环的有限元素时，它可以被识别为置换，例如。{（1， 2）（3， 4）}或作为形式项S2（C2（1， 3），C2（3，4））。计算机。作为具体置换和具体点的应用操作符的过程注释，我们使用GAP。对于包含变量的排列，结果的计算通常是不可能的，例如，{（1， 2）（3，x）}@4的结果取决于x= 4是否成立（GAPM. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127139甚至不允许在表达式中使用未绑定的变量）。然而，有些情况下可以用与常数相同的方式进行评估，例如，{（1， 2）（3，x）}@x= 3。排列的识别和它们包含不相交循环的属性可以通过收集约束来至少近似结果。 对于置换{（1， 2）（3，x）}，x的值受xi= 1，xi=2和xi=3的约束类似地，对于{（1， 2）（3，x）}@4，结果被约束为3或4。定理。有了变量，现在就有可能用公式表示包含注释常数的定理，例如下面的引理。对于集合S上的所有置换p和所有两两不相交点i，j，k∈S保持p<${（i，j，k）}<$p−1={（p @ i，p @ j，p @ k）}。为了证明，我们可以利用我们的排列表示所给出的知识。为了证明置换是相等的，我们必须证明它们在域S上返回相同的值。右侧的置换仅操作点p@i、p@j和p@k。所以我们只需要考虑这三个点和第四种情况，对于l∈S中的一个点，与p@i，p@j和p@k不同。这些案例可以通过评估来显示。对于p@i，右侧的值为{ （ p@i ， p@j ， p@k ） }@（p@i）=p@j，左手边为p<${（i，j，k）}<$p−1 @（p @ i）= p <${（i，j，k）}@ i = p@j。其他情况类似，除了第四种情况，其中l/∈ {i，j，k}必须使用。既然引理是可用的，我们可以应用于其他证明，这些证明是为注释项而制定的，而不必将我们的表示扩展到它的定义。例如，在证明交错群An（n≥5）的所有三个元素的圈是共轭的。6结论通过注释术语，我们将语义信息附加到术语。这使我们能够区分存在有效计算算法的数学对象和必须纯粹通过演绎来这种区分的标准是客体被给予的形式140M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127而不是对象的属性。例如，我们在有限集合之间进行区分，其中元素从其他形式化中显式给出。在对象逻辑中，不可能定义谓词（即，一种分类），它将以元素的形式给出的有限集合与有限集合的其他表示区分开来。因此，这种区别不能在对象逻辑内部表达，而必须作为逻辑外的注释来表达唯一不离开形式语言的方法是形式化特殊对象本身的数据结构及其作为对象逻辑中的理论的解释。因此，对数据结构的所有操作都必须明确执行，并通过证明来证明。除非证明系统支持数据结构的高度自动化，否则这可能是一项乏味的任务。在我们的方法中，我们只需要为形式对象重建操作，这通常比执行操作本身更容易。数据结构高度自动化的框架的一个例子是CO q系统中实现的归纳构造演算[5]，其中可以执行归纳定义的操作，而无需证明义务。 我们的方法的优点是它不依赖于一个特定的正式系统。存在将计算集成到形式推理中的相关工作，例如NuPRL [9]的类型理论中的整数运算，以及自动定理证明器Otter [12]中某些项的函数求值我们将这一思想应用于其他类的对象和这些对象上的操作，并认为引入新类的可能性是在数学表示中建模可扩展性的一个重要特征与这些系统相比，我们的评估并没有扩展正式系统，因此并不影响正确性。我们的注释用于简化抽象证明的构造，但需要在对象级别上进行验证。将计算算法集成到定理证明中的其他方法，利用现有的系统，如MAPLE，通常集中在算术运算和实数分析问题上[2，7]。通过定理证明器中的形式化与语言之间的对应，简化了将结果集成到定理证明系统中计算机代数系统，例如，MAPLE可以处理变量，算术项可以通过它们的类型来识别，并且关于在计算机代数系统中表示的签名的子项一致性保持。3因此，只考虑定理证明者签名中的符号之间的对应关系并将它们与3项代数T∈A称为关于签名A，i∈A相容的任何项f（t1，...，tn）∈T已经包含在代数TA[3]中。M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127141计算机代数系统。这在一般情况下是不能预期的，例如，计算机代数系统GAP不允许未绑定的变量，并且只能用具体的结构执行计算。通过注释，我们能够表达计算对象和操作的更好的分类，这些对象和操作可以用于与计算机代数系统的通信。数学形式化的一个共同的观察是，不存在一个最好的形式化，但有几个可能的形式化，它们适合于不同的目的。有了注释的术语，我们不必做出决定。我们可以使用直接编码的形式表示，而有替代的表示形式的注释。7今后工作我们已经提出了扩展的注释常量注释条款和动机这种表示与例子，演示了如何的知识，特殊类型的对象可以利用计算和推理。我们已经成功地证明了注释常数在证明置换群问题解的大型案例研究中的有用性[4]。作为下一步的扩展注释的条款，必须评估在广泛的案例研究以及。特别是，必须调查证明义务的比例（可通过计算解决）是否合理地解决了由注释术语的评估机制的实现所引起的开销。随着含有注释项的定理的出现，问题出现了，是否有可能在证明过程中保持抽象表示，或者是否有必要扩展到形式表示。我们希望我们的表示对于证明规划背景下的自动证明搜索特别有益。此外，我们希望整合我们的椭圆表示，我们已经为矩阵开发了其他对象，特别是包含变量的对象。有了椭圆，我们可以更一般地将上面关于循环的引理的结论公式化，即：p{（i1，.，i n）}p−1={（p @ i1，.，p @ i n）}。对象i1，.，i，n不仅包含变量，而且可以将其本身解释为序列变量。因此，为序列变量[10]开发的技术的应用可能是有益的，应该在未来的工作中进行研究。142M. Pollet，V.Sorge/Electronic Notes in Theoretical Computer Science 151（2006）127引用[1] P. B.安德鲁斯数理逻辑与类型论导论：通过证明获得真理。Kluwer，第2版，2002年。[2] C.巴拉林湾Homann和J. Calmet。定理和算法：Isabelle和Maple之间的接口。以. H. M. Levelt，编辑，1995年符号和代数计算国际研讨会（ISSAC-95）的论文集，第150-157页ACM Press，Berkeley，CA，USA.[3] J. Calmet和K.霍曼逻辑和符号计算系统的通信和协作机制的分类。In F. Baader和K.联合Schulz，editors，Frontiers of Combining Systems：Proceedings of the 1st InternationalWorkshop，Munich（Germany），pages 221-234. Kluwer Academic Publishers，1996.[4] A. Cohen，S. H.默里，M。Pollet和V. Sorge。证明置换群问题的解。在Proc. of CADESpringer，2003年。[5] T. C和C。 PA U LIN-M OH R I N G. Indu ct ivelydefine d types. 体育教学 马丁-洛法和G。Mintts，编辑，Proc. of CologSpringer，1990年。[6] A. 多维耶， E. 庞泰利， 和G. 罗西设置统一。CoRR， cs.LO/0110023，2001年。http://arxiv.org/abs/cs.LO/0110023网站。[7] J. 哈里索湖。 你好。一个skeptic的apr oa c h o C o m b i n i ng HOL and Ma p l e。J. 自动推理，21（3）：279 -294，1998。[8] G. Huet，G.Kahn和C.波林-莫林 CoqProof Assistant-版本8.0，4月。2004年http://coq.inria.fr网站。[9] C.克赖茨Nurpl证明开发系统，版本5，12月。2002.http://www.cs.cornell.edu/Info/Projects/NuPrl/网站。[10] T.库齐亚与序列变量和可变元符号的统一及其与模式项的扩展。Proc.of AICS施普林格，2002年。[11] S.朗代数 Addison-Wesley，第2版，1984年。[12] W.麦库尼Otter3.3参考手册2003.http://www-unix.mcs.anl.gov/AR/otter/网站。[13] 欧米茄集团。与Omega合作开发。在Proc. of CADE施普林格，2002年。[14] M. Pollet和V. Sorge。在术语水平上整合计算属性。在Proc. of Calculemus[15] M. Pollet，V. Sorge，and M.克尔伯直观和形式表示：矩阵的情况。 在MKM 2004的Proc.，LNCS的第3119卷中。Springer，2004.