归纳定理证明中的战略问题与挑战

理论计算机科学电子笔记125（2005）5-43www.elsevier.com/locate/entcs归纳定理证明中的战略问题、问题和挑战Bernhard Gramlich1Fakultüatfur？rInformatik，TUWienFavoritenstr.9摘要（自动）归纳定理证明（ITP）是自动推理和定理证明中的一个具有挑战性的领域通常，（自动）定理证明（TP）是指自动证明一般（通常是一阶）定理的方法，技术和工具如今，TP领域已经达到一定程度的成熟，功能强大的TP系统被广泛使用。ITP的情况是惊人的不同，在这个意义上，证明归纳定理在本质上自动的方式仍然是一个非常具有挑战性的任务，即使是最先进的现有ITP系统。在一般TP和ITP中，指导证明搜索过程的策略在自动化以及交互式或混合环境中具有根本的重要性。在本文中，我们将分析和讨论ITP中最重要的策略和证明搜索问题，比较ITP和TP，并论证为什么ITP在某种意义上更具挑战性。更一般地说，我们将系统地隔离，调查和分类ITPw.r.t.中的主要问题和挑战。自动化，在不同的水平和从不同的角度来看。最后，基于这种分析，我们将提出一些关于该领域最新技术水平的论文，可以被认为是实质性进展的可能标准，以及未来有希望的研究方向，走向（更多）自动化ITP。关键词：归纳定理证明，自动定理证明，自动化，交互，策略，证明搜索控制，挑战。1背景和概述定理证明任务在计算机科学中无处不在，例如，在程序规范、转换和验证等领域。大多数情况下，给定的、生成的或结果的证明任务不是一般的（在这个意义上，要建立底层逻辑规范的所有模型中的1Email：gramlich@logic.atwww：http://www.logic.at/staff/gramlich/1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.0066B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5但更具体的是，有效性仅在模型的某些子类中显示（或在唯一的标准模型中，只要它存在）。在这类有限的模型中有效的公式类通常比一般定理的公式类大得多。通常，任何证明这些性质的合理方法[2]事实上，在计算机科学应用中，特别是在软件工程和关于规范和程序的推理（的形式基础）中，规范者、程序员或用户通常对给定规范（或公理化）的所有模型不感兴趣，而是对由规范诱导的、与她/他的直觉密切对应的特定（并且通常是唯一的）自然模型感兴趣。这意味着对于证明性质（一般）TP通常是不充分的，只能用作一种第一默认方法。如果一个猜想可以通过TP证明，那么它也是一个归纳定理，但如果它不能通过TP证明（甚至证明一般是无效的），它仍然可能是一个归纳定理。自动TP已经被证明是相当成功的今天（在其范围内 的应用程序），而这并不真正适用于ITP，更确切地说，是自动化ITP。因此，更好地了解这些困难也可能有助于改进ITP方法和技术。本文主要是非技术性的和高层次的，侧重于相关的是，在（自动化）ITP，使问题的难度。我们假设一些基本的知识，术语和符号在一阶逻辑。虽然演示文稿基本上是非技术性的，真正理解，欣赏或批评的分析开发，特别是结论和相互关系，我们推测，一些熟悉ITP的理论和实践将是必要的，因为没有自己的经验，ITP的问题通常被低估。对于感兴趣的读者，我们提供了大量的参考资料，可以作为一个起点，更详细地研究ITP的各个方面和方法。虽然到文献的链接是相当全面的，我们不要求任何形式的完整性与此书目。2事实上，归纳定理的定义通常也可以这样给出。它具有归纳的性质，从这个意义上说，从一个公式的许多--通常是无限多（基础）--实例中，可以（归纳地）推导出一个更一般的公式，参见。例如[12]。此外，应该注意的是，我们在这里处理的归纳法（作为证明方法）不应该与归纳学习领域的归纳法混淆。 例如在ALT（数学学习理论）会议上使用。B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）57作为主要贡献，我们认为ITP的主要问题和挑战的系统分析和评价。他们最终对该领域的最新技术水平进行了评估，其中一些论文被认为是实质性的进展，以及未来相应的有希望的研究方向，朝着（更多）自动化ITP发展。在进入细节之前，让我们提到一些论文和会议记录，这些论文和会议记录在后面没有明确讨论，其中与TP和ITP中的证明搜索相关的某些问题已经进行了深入的讨论。这方面工作的一个主要论坛是自1997年以来举行的自动演绎法战略讲习班，参见。[90]、[93]、[91]、[92]、[22]。 另一个来源是自1990年代初以来不定期举行的关于归纳证明自动化的讲习班，但最多是非正式的程序（参见第13段）。例如[108]）。其他文献包括[45，48]，[49]，[64]，[65]，[66]，[68]，[86，87，88，89]，[104，106，110]，[119]，[120]，[125]，[130]，[135]，[147]，[149]，[154]，[155]，[157，158，159]，[161，162]，[171]，[172]，[175]，[177]，[178]，[196]，[203]，[231]，[233]，[234]。本文的研究计划如下。在本节中，我们将讨论归纳法的一些基础知识，TP与ITP，以及ITP的不同方法和假设。在第2节中，我们将详细介绍和讨论ITP中的相关战略问题和问题。在第3节中，我们将给出对当前最先进的系统和目前使用的一些主要ITP系统的评估（同样不要求完整性），以及成功和失败的总结。最后，在第4节中，我们将分离、总结和关联我们认为ITP中的主要问题和挑战，从而在第5节中提出一些关于未来的论文，以及关于有希望的研究路线/实质性进展的标准这些论点可能是相当有争议的，可能不会被广泛分享，但有相当多的证据。如果它们能引起研究界的热烈讨论，这已经是一个非常积极的结果。1.1关于归纳如前所述，归纳的概念在其用法上是模糊的，尽管基本概念--从具体实例到更一般的东西--是相同的。证明技术可以是归纳的，因为它们采用基于归纳原理的归纳图式。陈述的有效性的概念也可以是归纳的。还有其他一些概念和领域，归纳和归纳过程是有意义的，比如（算法）归纳学习机制。我们关心的是前两个，即定理的归纳证明（更确切地说，证明）或归纳性质的证明。在更仔细地了解这意味着什么之前，8B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5►►让我们考虑一下这种意义上的归纳出现在哪里（在计算机科学和数学中）。答案很简单：几乎所有地方！例如，当推理递归定义的域或数据结构及其上定义的函数时，或者关于程序和规范时，通常不仅需要一般TP，而且需要更多，即ITP。特别是在计算机科学中，基于逻辑的规范通常（显式或隐式）被假定为构造性地指定和/或建模某些系统或计算任务，人们通常对给定规范的所有可想象的模型不感兴趣，而只对某些模型感兴趣（即， 在某些受限的模型类别中）或者甚至仅在捕获人们所想到的基本属性的独特的特定模型（标准模型）中。 这种限制往往其特征在于要求所考虑的某个模型中的每个元素都必须是项生成的。 换句话说，模型中的元素需要在规范中有一个语法对应物。 从某种意义上说，这是计算机科学背景下对许多（尽管不是所有）应用程序的一个非常自然的要求。不幸的是，在关于验证和定理证明的文献中，（一般）有效性和归纳有效性（分别是-定理和归纳定理）之间的区别有时没有被适当地提及，甚至被忽视。对于某些目的来说，这是很成问题的，因为，正如我们将要讨论的，证明技术的含义是深远的。有根据归纳法的非常一般的原理，用于证明依赖于参数x的某个性质P，可以以推理规则的形式陈述如下：你好[（y。[y x<$P（y）]）<$P（x）]P（x）有良好基序（在x的域上）。<归纳法中常用的归纳原则和模式（自然归纳法、结构归纳法、价值过程归纳法等）。都是通过适当的实例从这个一般原理中获得的。接下来，让我们简要回顾一下语法和语义之间的基本概念和关系，特别是可导出性和有效性之间的关系（在一阶逻辑框架中）。通常，基于某组公理和某组规则，所得到的推理系统定义F，公式F的（语法）可导性。如果F是可导的，则它是（给定推理系统中的基本公理集的）演绎定理。F从某个假设集合G（被认为是附加公理）的句法蕴涵或相对可导性被记为G <$F，在这种情况下，F被称为G的演绎结论。在语义方面，人们通常有一个解释给定B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）59|►|⇒►►⇒|逻辑规范。满足一个规范G的解释是G的一个模型。一个公式是F有效（|= F）如果它在初始公理的所有模型中成立。从某个假设集合G（被认为是附加公理）得到的F的语义蕴涵或相对有效性由G表示|= F，其中F称为G的语义推论。滥用符号，F在初始公理的某个特定模型M中（或在初始公理的某类模型K中）成立的事实也用M表示|= F（或K |= F）。现在，出于明显的原因-在逻辑和（自动）TP -一个努力的（语义）有效性和（句法）可推导性的等价，并为有效和有效的方式来建立后者。在一阶逻辑中，任何合理的推理系统都是众所周知的（F=F）和完全（=FF）。不幸的是，有效性和可推导性之间的这种良好（有限）对应关系在ITP中一般都丢失了 我们在这里不深入讨论这种现象，而只提一个特殊的简单情况。考虑在某个特征向量上的某个（隐式泛量化的）方程组E然后，由yT（ε）/=E给出了某个方程s = t的归纳有效性或初始有效性 =s=t，其中T（m）/=E 是通过E诱导的同余分解的基项代数。为了从句法上捕捉归纳有效性的概念，即，在演绎或可推导性方面，需要一个无限的特征：T（）/=E|=s=tσ。Esσ=tσ这里，置换σ的范围覆盖给定签名上的所有基置换。为了解决这个有限的证明任务，人们通常使用（适当的）归纳证明技术，以证明E sJ=tJ确实对s=t的所有基实例sJ=tJ成立。在上述情况下，至少有可能通过推导性陈述的无限连接来表征归纳有效性，即，以明确的方式将这并不总是那么容易。事实上，这在很大程度上取决于所使用的归纳有效性的概念。在各种情况下，有一些很好的理由选择一个版本的归纳有效性，偏离了它的标准定义方式。我们在这里简要地提到一个方面，并给出一些相关文献的提示。基本的激励方面进行不同的是一个不受欢迎的非单调现象。为了说明这一点，考虑由0 +x=x，s（x）+y=s（x+y）给出的加法的方程规范E那么很容易验证（证明）（X）x +0 = x是E的归纳定理，即， 它在初始代数T（λ）/=E中成立。现在我们通过减法的（一致的）定义来加强原始规范，通过x−0 = x和s（x）−s（y）= x−y产生EJ。然而，与直觉相反，10B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5∗- -−now（）不再是EJ的归纳定理！ 其（本质）原因在于，富集在初始模型中引入了新的垃圾项，破坏了所需的属性。也就是说，例如用0s（0）代替x，我们得到（0s（0））+ 0 = 0s（0），这在EJ中无法证明。这里，富集是一致的（即，没有识别出先前不同的元素），但是在新操作仅部分定义（就“旧数据构造器”而言）的意义上是不完整的从[128，127]（关于不完全规范的一致性和完备性证明）和[232]，[235]使用所谓的构造器模型的工作开始，这条推理路线-采用，定义和使用我们将不详细讨论这些方法，但应该注意的是，上述非单调性现象在ITP中具有严重的后果。通常情况下，要么强加一个非常严格的规范纪律，从而避免局部性和非单调性问题（这种方法在大多数当前ITP系统中采用），要么必须使用一个更自由但技术上更复杂的更复杂的框架。因此，在某种意义上，现有方法的充分性和可行性之间存在着权衡1.2TP与ITP接下来，我们将讨论TP和ITP之间的一些共同点和差异，根据上下文，我们假设目标是尽可能自动化。1.2.1从逻辑角度比较假设E是一个等式一阶规范，使得它允许某个唯一的标准模型。3让我们用Th（E）表示E 那些在标准模型E中为真的，由ITh（E）。 从逻辑的角度来看，我们 可以提出以下意见：(1) 我们有Th（E） ITh（E），但一般是ITh（E）/ITh（E）。(2) Th（E）的任何合理的演算都是可靠的和完备的，并且Th（E）是（一般）不可判定但半可判定的，即，Th（E）是递归可排数的，但不是它的补数。此外，切割消除是可能的。[3]例如，如果E是一组（隐含泛量化的）正条件方程，其中条件是方程的合取，则保证存在这样一个唯一的标准模型（初始代数）。B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）511⊆(3) 对ITh（E）的任何合理的演算都是合理的，但一般来说必然是不完整的。4ITh（E）一般既不是可判定的也不是半可判定的，即，甚至不是递归可重复的。此外，削减消除是不可能的（[167]）。实际上，关于（1），结合（2）和（3），存在ITh（E）与Th（E）一致的情况，因此ITh（E）特别地变得半可判定。当包含体Th（E）ITh（E）是非严格的。 例如，如果E是纯等式的，则E称为ω-完全的，如果一个方程是有效的，且它是归纳有效的。在这样的ω-完全（等式）规范中，试图证明一个猜想的归纳有效性与试图证明它的（一般）有效性是一样的。不幸的是，ITP和TP重合的情况仅适用于非常有限的情况和设置，并且不适用于涉及ITP的大多数验证问题。然而，应该注意的是，有已知的情况下，某些公式的归纳有效性是可判定的，以及某些子任务的具体决策程序。这种知识和相应的有效决策程序是最先进的TP和ITP系统的关键组成部分，参见。例如[199]，[63]，[216]，[184，185]，[209]，[6]，[121]，[141]，[126]，[78，79]，[140]，[219，220]。关于ω-完备规范，例如在进程代数中有有趣的应用，我们参考例如[98]，[96]，[1]，[95]，[170]，[18]，[71]见附件。关于（2）和（3），这些关系和性质显示了证明有效性和证明归纳有效性之间的根本区别，这些区别可以追溯到理论计算机科学和数理逻辑中的开创性工作，参见。例如[80]、[97]、[217、218]、[156]、[167]。尤其是w.r.t. (3)不可能割消（[167]）也有严重的后果，并构成了与一般TP的实质性区别。在本质上，这意味着在ITP中辅助引理（要猜测）通常是无法避免的。关于ITh（E）甚至不是递归可证明的事实，这表明（在其他方面中），当试图证明归纳猜想时，应该确保肯定证明尝试可能是成功的，通过（也）寻找矛盾，从而尽早排除错误的证明。[4]实质上，这是由于哥德尔的第一不完备性定理，该定理指出，在一个形式（演绎）算术系统中，存在为真但不可证明的公式。 （参见[80]，[97]）。12B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）51.2.2证据检索方面的比较在这里，我们只给出一个初步的粗略说明TP和ITP之间关于证明搜索问题的本质区别。这些方面中的一些将在后面详细介绍。从证明搜索、证明搜索树构造和证明搜索控制的抽象观点来看，其特征在于：• TP：证明搜索树是有限分支的，对于任何合理的（健全的和完整的）底层推理系统，如有序归结cf。例如[11]和基于paramodulation-based定理证明（cf.例如[186]）。在证明搜索过程中搜索和构造反例（例如通过模型构建技术，参见例如[69]，[197]）可能有所帮助，但在某种意义上不是成功证明所必需的。（一阶）TP中的证明搜索控制是（已知的）具有挑战性的，特别是当试图有效但仍然完整时。• ITP：证明搜索树是无限分支的，对于任何合理的（健全的）底层推理系统，以及几个不同的原因。反例的寻找和构造在证明搜索过程中是非常必要和重要的。ITP中的证明搜索控制是非常具有挑战性的，对于几乎所有非平凡的归纳猜想，有时甚至是平凡的。证明搜索树在ITP中是无限分支的，而不是TP，本质上是由于归纳推理能力的不完备性。这种无限性的一个基本来源已经由这样的事实给出，即通常有无限多的（可靠的）归纳图式可以用于证明尝试。此外，作为一个众所周知的结果，在实践中，人们经常不得不引入各种猜测步骤，如推广命题，发明辅助归纳引理（也要证明）和引入归纳情况分裂。 这些归纳猜测步骤意味着，目前还不清楚是否实际处理的猜想确实可以是一个归纳定理。因此，为了消除错误的假设并削减无用的分支，同时尝试反驳假设是至关重要的，例如，通过寻找反例5.这些方面的结合使得ITP5不知何故，似乎在自动推理社区中，（显式）证伪的主题，包括模型构建和反例的构建，尚未得到应有的关注（参见，例如，[200]）。对于最近试图集中在这一主题，见例如。[3]的文件。······B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）513在具有一定程度自动化的系统中，证据搜索控制是非常具有挑战性的。1.3关于ITP的就本文件而言，没有必要以适当的深度介绍和讨论ITP的现有方法。这显然也超出了范围，需要更多的空间。然而，我们至少要提到一些在实践中很重要的问题，这些问题对ITP系统的设计和实施首先，让我们考虑一些问题和方面的逻辑和框架，在不同的方法。• 一阶逻辑与高阶逻辑：虽然高阶逻辑更有表现力，但为了ITP（自动化）的目的，一阶逻辑已经足够具有挑战性。• 完全一阶与泛片段：大多数ITP系统和方法都集中在泛量化的一阶公式上。允许实际的量化（或任意的量化变更）显然会使事情变得相当复杂。典型地，存在归纳推理是通过试图建设性地找到见证人并证明他们满足各自的归纳 性 质 来 处 理 的 ， 参 见 。 [2019- 05 -19 00 ： 00][2019- 05 - 1900 ：00][2019 -01：• Unsorted vs. many-sorted vs. order-sorted：包括/要求更严格的类型规则可能有助于避免证明搜索中的无用计算，但当然也限制了系统和规范的建模ITP系统的类型化概念是相当多样化的，从相当不类型化的（例如，[39]）到强类型系统（例如，[190]）。• 偏性和归纳有效性的概念：对不确定性的处理，即，只有部分定义的新功能是一个重要的问题（也见上文的讨论）。在扩展规范时允许无限制的递归常常使大多数以前的归纳定理失效。因此，任何一个人都必须适应归纳有效性的概念（参见。例如[235]，[128，127]，[230，229]，[169]），或使非关键，例如通过简单地禁止它，或通过以某种定义明确的方式使具体化（参见[169]）。例如[39]，[41]，[176]）。无论如何，对不确定性的处理对框架和整个ITP进程具有深远的影响• 构造函数与析构式归纳：关于基本数据结构的表示，可以用构造函数构造性地表示数据对象，也可以破坏性地提取相关信息。14B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5通过析构函数（或选择）函数，例如对于具有构造函数nil，cons和析构函数car，cdr的列表（cf.例如[39]）。通常，表示和证明可以很容易地从构造函数转换到析构函数框架，反之亦然，然而，从证明技术的角度来看，最好坚持使用这些双重框架之一• 固定与惰性归纳排序（生成）：ITP的大多数方法通过分析公式（和底层规范）并为其设计一个适当的（然后固定的）归纳模式来开始对归纳猜想的证明尝试，然后根据该模式进行。另一种方法是在没有固定归纳模式的情况下开始证明，而是在证明尝试中收集关于哪个归纳模式会将推理真正变成正确归纳证明的信息。后一种方法已经在例如[201]中进行，并且也部分纳入[169]，[8]。当然，后一种方法的通用性和优雅性也有其代价。也就是说，整个归纳推理的正确性变得不平凡，必须在后验中建立，而且--更严格地说--在技术上证明，搜索变得更加困难，因为目标导向性通常严重依赖于现有的固定归纳模式，不再容易获得。• 基础（演绎）逻辑框架：这可能基于几种不同的方法（对于具有等式的一阶逻辑），如有序解、叠加、调节等。它可以是基于饱和的或不基于饱和的，等式的或非等式的，基于子句范式或任意子句等，这些方法具有已知的所有优点和缺点。所有这些问题都与ITP中的证据搜索相关，但在此不作讨论• 显式与隐式归纳：（自动化）ITP的早期作品（参见。例如[36，37，39，38，42，43]，[223]）都使用显式归纳，在这个意义上，对于给定的归纳猜想，显式地计算出具体的归纳模式，随后的推理基于该模式。从[182]，[81]，[101，102]的开创性工作开始，隐式或“无归纳”归纳的替代方法被开发出来该方法的基本思想大致如下（在具有相等性的子句的上下文中），参见。[60]给定一个指定（子句集）E和一个归纳推理集C，人们将C添加到E并试图导出不一致性。如果这被证明是不可能的，那么C中的子句是E的归纳结果。在这里，“不一致”理解为w.r.t. 对E.“Turning out to be impossible” means that one has to devise ap- propriatestrategies ofB. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）515在许多情况下，电感性饱和过程有希望终止（有或没有不一致性）。在1980年代和后来的[182]，[81]，[101，102]的方法被以各种方式扩展，细化和推广例如[192]，[122，123]，[72，74]，[9]，[83]，[76，77]，[62]，[60]。另外，开发了介于显式诱导和隐式诱导之间的其它相关方法，例如，[100]，[204]，[44]，[127，128]，[133]，[235]，[131，132]，[160]，[31]，[29]，[26]，[27]，[230，229]，[169]，[227]。以前是现在也是一个关于显性与隐性归纳及其组合的持续辩论，特别是关于这些方法的优点和缺点以及它们之间的关系。但似乎很明显，关于ITP中证据搜索过程中的基本问题，这两种方法基本上面临着相同的问题。出于这个原因，我们在这里不详细讨论后一个方面和关系。接下来，为了完整起见，让我们提到关于ITP系统的几个（尽管不是全部）重要方面，特别是与系统架构，其功能，目的及其证明搜索控制有关的方面。• 独立工具与更大系统中的组件：显然，这个属性对设计和架构有影响。• 同构与异构工具：同构工具可能更容易实现、理解和维护，但功能可能要差得多。• 内置理论与显式处理：如何处理预定义的基本数据类型及其属性，以及函数的某些有问题的属性（如结合性和交换性）是任何实现的关键方面。• 专门证明任务的子工具（决策程序等）：这样的子工具当然应该是可用的，但是它们的集成通常是不平凡的。• 预期的功能（是/否与公正、证明对象、重用、增量、模块化）：预期的功能在设计过程中当然非常重要，并且通常使不同的系统很难比较。• 通用推理系统与特定问题领域的专用工具：显然，这样的决定也有深远的影响。• 实验工具与高精度系统（认证）：开发后一种类型的系统通常意味着更多的工作和相关设计决策的关注。• 后对比治疗前与集成开发：要用系统处理的设想推理任务（包括归纳证明）的类型，16B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5我我我HH |H|总体开发模型（例如，首先编程，然后验证;或者，首先指定和验证，然后编程）显然是对系统设计和体系结构的一种检查。• 期望的自动化/交互程度：显然，（期望的）高度自动化意味着比交互式推理风格• 证明搜索控制架构/概念/语言：对于至少具有一定程度自动化的ITP系统，证明搜索控制的架构、用于描述和引导证明搜索的底层概念和语言是实现具有预期自动化能力的系统的关键组件在本文的其余部分，让我们在一阶逻辑中用等式固定ITP的理论（逻辑）设置（尽管对于其他合理设置，结果分析也是相同的），部分遵循[60]：设E是一组一阶句子。一阶公式φ是Ei ∈ φ的归纳推论，对于每一个Herbrand解释，、=E表示=φ。 如果E是一个Horn子句集，则存在E（或标准）模型E的唯一最小Herbrand模型。在这种情况下，我们不需要考虑所有的Herbrand解释，而只需要考虑最小的解释：如果E是Horn子句的集合，c是肯定子句，则c是E i的归纳结果，|= c。注意，E的归纳结论不应与IE理论中的元素混淆。归纳理论包含在IE中，但不是相反（因为否定的陈述表达了E中的某些元素是不同的，并不适用于E的所有Herbrand解释）。在证明或证伪归纳定理时，我们总是要记住在IE中的有效性，归纳定理是在标准模型E中有效的公式。此外，在ITP设置中，我们假设数据库包含具有所有公理和定义的基本规范E，一组已经证明（或以其他方式建立）的归纳引理L，以及当前的归纳引理集合C（允许C包含多个元素在实践中是方便的，因为在证明尝试期间通常会生成在ITP的其他合理的基本逻辑设置中，ITP中基本问题的后续分析将很可能非常相似。这也涉及到方面，无论潜在的归纳概念是明确的或隐含的，如上所述。虽然精确的分析显然取决于所使用的框架，但基本的技术和证据搜索问题是相同的。然而，它们的语法和技术外观可能不同。B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5172ITP战略在这里，我们将深入讨论ITP中的关键策略和验证控制方面（尽管不是技术性的），其中（隐含的）目标始终是获得高度自动化。2.1为什么策略在ITP中如此重要？正如我们之前所讨论的（见第1节），ITP在某种意义上比一般TP更难，因此这也应该在证明搜索过程中得到反映。那么，为什么（好的）策略对ITP如此重要？一些主要原因是• ITP方法的不完整性，• 搜索空间的结构和大小（在多个维度上无限分支，见下文），• 归纳证明尝试的递归性质，• 在ITP尝试中衡量进展的困难• 以适当和智能的方式控制/指导证据搜索过程的困难这个难题包括许多更详细的步骤和决定：· 下一步应该做什么（尝试）· 什么时候应该认为证明尝试失败（无望）？· 在这种情况下该怎么办· 何时应用回溯？· 何时以及如何进行归纳？· 何时以及如何简化（简化到何种程度）？· 何时以及如何开始归纳（生成归纳模式）？· 如何使归纳假设适用（以目标导向的方式）？· 何时以及如何进行案例分析？2.1.1基本战略控制问题让我们更准确地考虑一下什么是相关的战略问题。为此，我们看一下归纳证明尝试的典型结构• 尝试非归纳方法（何时以及如何？）：测试不一致性，生成反例。开始TP尝试（无诱导）。尽可能多的w.r.t.当前的定义和引理数据库。· 但是：简单性可能需要归纳论证！···18B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5• 尝试归纳：分析了猜想中的递归结构和涉及的函数。基于此分析（包括一些前瞻）为适当的归纳模式生成候选项。进行诱导：分成几个案子。- 是的使归纳假设适用。· 概括推测。· 生成（辅助）引理。那么，上述清单中的关键和基本战略控制问题是什么？首先，以下问题是显而易见的，但不是他们的答案：• 什么时候应该测试不一致性，以及如何测试？什么时候应该寻找反例，如何寻找？• 什么时候应该决定尝试没有归纳的一般TP，什么时候不应该？下一个动作列表对于每个合理的ITP系统来说都是核心和根本重要的，所有这些动作都是关键的6，并且被认为是搜索树中的选择选项-无限分支：(1) 简化（无限分支7和临界）(a) 什么时候？(b) 怎么做？使用哪些定义和引理？按什么顺序？(c) 递归地使用归纳法来验证条件引理的适用性？(d) 转换为正常形式？(e) 逆简化（逆扩展）？多远？(2) 归纳法（无限分支和临界）(a) 计算并选择合适的归纳模式。(b) 生成相应的证明任务。(c) 使归纳假设适用，例如：通过异花受精、松土和其他减少差异的技术。6 我们在这里所说的关键是指，如果没有这样一个（适当的）行动（或类似的行动）， 整个证明尝试可能是无望的。7事实上，W.R.T.对于一个由定义、引理和当前结构组成的有限数据库，这种简化操作的第一步通常只是有限分支，因为只有有限多的可能性。然而，当简化可以是非终止的（在这种情况下，“简化”只有直观的意义，而不是形式的意义），或者当在简化过程中允许其他无限分支操作时，如用于验证某些条件引理的条件的归纳，多步简化是无限分支的。···B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）519→⇐(3) 案例分析（无限分支和临界）(a) 什么时候？(b) 怎么做？ 根据什么标准？(c) 如何核实个案？(4)泛化（无限分支和临界）(a) 什么时候？(b) 怎么做？ 为了什么目的？(c) 如何避免过度概括？(5) 引理生成/推测（无限分支和临界）(a) 什么时候？(b) 怎么做？ 为了什么目的？(c) 组织：自上而下（相对ITP）还是自下而上（证据是绝对的）？关于这份清单的一些评论和意见似乎是合乎顺序的（参见第10段）。[47]也用于ITP中无限支化行为的某些方面的讨论）。首先，很明显，证明搜索与无限分支步骤原则上可以被序列化（假设只有可数的选择），即，用一棵无限分枝的树来模拟然而，在实践中和w.r.t.问题的性质，这将是完全不满意和不可行的。关于简化（1），对于什么可以简化以及如何简化，通常存在非常高的不确定性（b）。当前数据库此外，“简化”的概念并不总是明确的，因为不需要确保这种转换的基础良好。如果它是有保证的，例如，通过在项和公式上强加一些有根据的排序，则不再允许某些期望的变换步骤（扩展或逆简化）。在交换性等置换性质的存在下，保证简化过程的终止是困难的，必须进行额外的努力以避免循环（或更一般形式的非终止）推理。另一方面，众所周知，在许多例子中，某些变换必须是“非简化的”才能导致最终的成功。通过递归地允许归纳（c），简化的能力大大增加，例如，通过对cσ的归纳证明，验证了形式为lrc的条件引理对实际公式C=D[lσ]的适用性.由于简化通常是不连续的，也经常是不终止的，因此确定一个人应该简化到什么程度是非常重要的。(e)，（f）.经验表明，过于简化也会妨碍找到证明，反之亦然。20B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5归纳（2）也许是研究最深入的操作。[39][3终止证明）是一个相当好理解的领域。在[39]中，对一个给定的归纳猜想计算和选择适当的归纳图式是一个两阶段的过程。首先，在引入某个函数f的定义时，分析定义，特别是递归结构，并存储关于f的递归结构及其递归终止原因的结果知识（在内部知识库中）。然后，当尝试对某个公式进行归纳时，猜想中所有定义的通过这种方式，计算出大量的候选归纳模式，然后根据一些质量标准尽可能地合并[39，42]（及其继任者[151]）的战略和战略已经取得了惊人的成功和令人印象深刻。递归分析和归纳模式生成的其他作品、变体和显式版本包括例如。[210]、[51、50]、[222、222]。给定一个具体的（可靠的）归纳模式，相应的证明任务（b）的生成通常是简单的。然而，归纳推理的核心和挑战是使归纳假设适用的目标导向技术。[8]这一步有许多思想、策略和逻辑学，更一般地说，这是基于差异约简和证明计划的推理。例如，交叉受精（[39]）和涟漪（cf. 例如[25][26][27][28][29][2[107]，[112]，[113]，[109]，[14，15，17，16]，[65]，[67]），[136]。案例分析（3）也是ITP中一个非常具有挑战性的主题和子任务。特别是，什么时候应该开始案例分析，如果是，如何开始？又根据什么样的标准来生成案例呢？此外，如果案例分析不是明显完整的，在这个意义上，所有的案例都被涵盖了，9验证完整性通常又涉及归纳推理，因此归纳的全部权力（和困难）。何时以及如何应用案例分析（在ITP中）的问题也是非常困难的问题，因为没有太多的文献存在（尽管任何ITP系统都有这样做的方法），参见。例如[39，42]，[151]，[30]。一个相关的问题是区分大小写的粒度应该有多细越是特殊的情况，信息量越大[8]一般来说，一个猜想的归纳图式由几个基本情况和几个归纳步骤组成，所有这些都必须被成功地处理。图9一些案例分析的完整性与案例c1，。..，cn总是可以通过增加一个对c i的析取的否定的格来强制执行。然而，有时人们更愿意使用语义上的区别，其中完整性必须被显式地（归纳地）验证。B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）521⇐⇐ ⇒⇐来证明本案中的财产另一方面，这是一个众所周知的现象--上述（2）中的一些技术也可以用于计划和尝试（希望）合理的案例分析。如果要找到一个证明，归纳推理（4）和引理生成（5）的推广是不可避免的，它们是密切相关的根本当然，搜索空间是无限分支的。这样的操作。对于引理生成，这是显而易见的。 在推广某些猜想C的情况下，这也很容易看到。 如果C只是一个等式（或另一个普遍量化的文字），那么只有无限多的可能性来进行句法推广（根据公式上的良基实例化排序然而，一旦允许语义概括，就有无限多的可能性。一般化和引理生成都是非常容易出错的，因为它们可能导致错误的推论，而原来的猜想是归纳正确的。因此，提供机制以避免过度概括和避免产生错误的“引理”是极其重要的。通常，这两种操作都只是在考虑到一些或多或少的具体目标的情况下应用的，即解决先前证明尝试的失败。然而，这样一个步骤在多大程度上可能真正有助于处理实际的猜想，仍然有待发现和验证，无论是先验还是后验。到目前为止，有一些但不是很多关于（4）和（5）的具体方法和策略的文献，以及更一般地关于如何在实践中（自动地）做到这一点并将这些特征集成到整个ITP系统中的文献，参见。例如[35，36，37，39，42]，[146]，[75]，[118]，[225]，[138]，[126]，[141]，[163]、[219、220]。2.1.2组织战略问题接下来，让我们讨论（更谦虚地：提出问题并说明可取的特性）ITP中一些最重要的组织（和战略）问题。同样，这份清单肯定是不完整的，我们想集中讨论一些我们认为重要的问题。(i) 关于数据和知识库（定义、结构、语法等），）的人：(a) 在成功验证尝试的情况下：[10]这里我们指的是任何归纳地暗示C的陈述，例如，如果C是条件的，也就是说，的形式D c，我们可以证明c d以及D d，然后后者（归纳）推广D c。更一般地说，在从句中，一般化可以通过弱化后继部分和/或加强先行部分来完成。22B. Gramlich/Electronic Notes in Theoretical Computer Science 125（2005）5哪些（中间）引理应该被保存（存储）？哪