自动推理（三）

为了说明“术语重写”中的主要思想，让我们探索一个涉及符号差异化的示例（示例和随后的讨论改编自Baader＆Nipkow 1998的第1章）。令der表示对x的派生尊重，令y为与x的变量不同，让u和v为跨表达式的变量。我们定义重写系统：

der（x）⇒1

der（y）⇒0

der（u+v）⇒der（u）+der（v）

der（u×v）⇒（u×der（v））+（der（u）×v）

同样，符号⇒表示匹配重写规则的左侧的术语应由规则的右侧代替。要查看工作中的分化系统，让我们计算X×X的派生型X，der（x×x）：

der（x×x）⇒（x×der（x））+（der（x）×x）r4

⇒（x×1）+（der（x）×x）通过R1

⇒（x×1）+（1×x）通过R1

在这一点上，由于没有规则（R1） - （R4）适用，因此无需进一步减少，并且重写过程结束。获得的最终表达式称为正常形式，其存在激发了以下问题：是否有一个表达式在应用规则时永远不会终止的表达式（R1） - （R4）？或者，更一般地：在什么条件下，在有限的许多规则应用程序中，一组重写规则将始终以任何给定表达式的形式停止？这个基本问题称为重写系统的终止问题，我们声明没有证据证明系统（R1） - （R4）符合终止条件。

有可能在减少表达式时，可以以多种方式应用重写系统的规则集。实际上，在系统（r1） - （r4）中，情况实际上就是这种情况，在der（x×x）中，我们可以首先将R1应用于（x×der（x x））+der（ x）×x），如下所示：

der（x×x）⇒（x×der（x））+（der（x）×x）r4

⇒（x×der（x））+（1×x）通过R1

⇒（x×1）+（1×x）通过R1

遵循这种替代行动，减少终止的正常形式与以前的情况相同。但是，这一事实不应被视为理所当然：当且仅当独立于应用其规则的顺序时，重写系统是（全球）汇合的，每个表达式总是最终被简化为一个正常的正常形式。可以证明（R1） - （R4）是汇合的，因此，我们有权说：“计算表达的衍生物”（而不是简单的“ A”衍生物）。为了使其更实际的后果添加更多规则，以使其产生不希望的后果。例如，如果我们添加规则

U+0⇒U

到（R1） - （R4）然后，我们将能够进一步降低某些表情，但以失去汇合的价格。以下减少表明，der（x+0）现在具有两种正常形式：计算

der（x+0）⇒DER（x）+der（0）由R3

⇒1+der（0）通过R1

给出一种正常形式，并且

der（x+0）⇒DER（x）通过R5

⇒1由R1

给另一个。添加规则

der（0）⇒0

将允许进一​​步减少1+der（0）至1+0，然后r5降低到1。通过四种可能的方式，它们最终都以相同的正常形式，即1。这不是巧合，因为可以证明（R6）实际上恢复了汇合。这激发了另一个基本问题：在哪些条件下，非集体系统可以将其制成等效的汇合系统？ Knuth-Bendix完成算法（Knuth＆Bendix 1970）对此问题给出了部分答案。

与任何其他自动扣除方法一样，术语重写需要指导其应用程序的策略。 Rippling（Bundy，Stevens＆Harmelen 1993，Basin＆Walsh 1996）是一种启发式方法，其起源于归纳定理提供，它使用注释选择性地限制了重写过程。叠加结石是方程式一阶逻辑的结石，它结合了一阶分辨率和Knuth-Bendix Ordering均等的概念。叠加是驳斥完整的（Bachmair＆Ganzinger 1994），是许多定理掠夺者的核心，最著名的是E方程定理供体（Schulz 2004）和吸血鬼（Voronkov 1995）。叠加已扩展到高阶逻辑（Bentkamp等，2021）。

2.6数学归纳

数学诱导是在数学和计算机科学中证明的定理非常重要的技术。根据涉及递归定义或某种形式重复的对象或结构所述的问题，总是需要数学归纳来解决。特别是，有关计算机系统正确性的推理需要归纳和有效实现诱导的自动推理程序，将具有重要的应用。

为了说明对数学归纳的需求，假设属性ϕ是零数的真实，并且如果一个数字为tum，则其后继是正确的。然后，使用我们的演绎系统，我们可以推断出任何给定数字n，ϕ是正确的，ϕ（n）。但是我们不能推断出所有数字都是正确的，∀x（x）;此推论步骤需要数学归纳的规则：

α（0）[α（n）-α（succ（n））]

∀Xα（x）

换句话说，要证明∀xα（x）证明α（0）就是这种情况，并且α（scucc（succ（n））从假设α（n）的假设中得出。推理系统中归纳的实施提出了非常具有挑战性的搜索控制问题。其中最重要的是能够确定在证明期间应用归纳的特定方式，即找到适当的诱导模式。相关问题包括选择适当的归纳变量，并识别基础和归纳步骤的所有可能情况。

NQTHM（Boyer＆Moore 1979）一直是自动归纳定理证明的最成功的实施之一。本着绅士的精神，博耶和摩尔对人们如何通过归纳来证明定理感兴趣。他们的定理示意剂是用功能编程语言lisp编写的，这也是代表定理的语言。例如，为了表达添加的换算性，用户将输入LISP表达式（相等（加X y）（加上y x））。系统中定义的所有定义的术语都是功能性术语，包括其基本的“谓词”：t，f，等于x y，如果x y z，以及，不，等等。用户隐藏；证明是通过重写术语的递归定义来进行的，最终将结论的陈述减少到t谓词。 Boyer-Moore定理摊子已被用来检查一些相当深的定理的证明（Boyer，Kaufmann＆Moore 1995）。引理缓存，问题声明概括和证明计划是在归纳定理证明的技术方面特别有用的（Bundy，Harmelen＆Hesketh 1991）。

3。其他逻辑

3.1高阶逻辑

高阶逻辑与一阶逻辑不同，允许对功能和谓词进行定量。语句“任何两个人都以一种或另一种方式相互关联”，可以在高阶逻辑中合法表达为∀x∀y∃rr（x，y），但在一阶逻辑中却不得。高阶逻辑本质上比一阶逻辑更具表现力，并且在精神上更接近实际的数学推理。例如，设定有限的概念不能表示为一阶概念。由于其表现力更丰富，不足为奇的是，实施自动化定理供奉献的高阶逻辑比一阶逻辑更具挑战性。这在很大程度上是由于以下事实：高阶逻辑中的统一比一阶情况更复杂：统一的术语并不总是具有最通用的统一，并且高阶统一本身是不可确定的。最后，鉴于高阶逻辑是不完整的，因此，对于任何自动推理程序来说，总会有一些证据完全遥不可及。

用于自动化一阶扣除的方法可以适用于高阶逻辑。 TPS（Andrews等，1996； Andrews等，2006）是一种定理的高阶逻辑系统，它使用Church的典型λ-Calculus作为其逻辑表示语言，并且基于结合Huet统一的连接型扣除机制算法（Huet 1975）。作为TPS功能的样本，该程序已自动证明了有限集的子集是有限的，这是所选公理的几种公理中的等效性，而Cantor定理表明，一组比成员的子集更大。该计划证明了后者是通过断言个人对个人的职能没有的，并通过对角线论点进行了证明。 Hol（Gordon＆Melham 1993）是另一个主要的高阶开发系统，主要用作硬件和软件关键系统的开发。 HOL基于实现交互式定理的LCF方法（Gordon，Milner＆Wadsworth 1979），它建立在强大的功能编程语言ML上。像TPS一样，HOL可以以自动和交互式模式运行。由于最有用的自动推理系统很可能是强调互动定理证明的最有用的自动推理系统（Farmer，Guttman＆Thayer 1993），并且可以用作在人类的指导下运作的助手。 （Harrison 2000）讨论了浮点算法的验证以及在用户指导下Hol Light证明的浮点数数学属性。 Isabelle（Paulson 1994）是一个通用，高阶的框架，用于快速的演绎系统原型制作。可以通过使用许多句法和演绎工具在Isabelle的Metalogic中制定对象逻辑。 Isabelle还提供了一些现成的定理证明的环境，包括Isabelle/Hol，Isabelle/ZF和Isabelle/Fol，可以用作应用程序的起点，并由用户进一步开发（Paulson 1990，Nipkow＆Paulson 2002）。 Isabelle/ZF已被用于证明选择公理的等效公理，良好的原理配方以及基本算术的关键结果，即对于任何无限的基础κ，κ·庇护κ=κ（Paulson＆Grabczewski） 1996）。

为了帮助证明在交互式证明中产生的高阶定理和放电目标，用户可以要求Isabelle/Hol通过大锤通过大锤调用外部一阶抛弃（Paulson 2010），这是一个旨在结合自动推理系统互补功能的子系统包括SMT求解器在内的类型（请参阅SAT求解器的部分； Blanchette等人，2013年）。 LEO-II（Benzmüller等人，2015年）也是基于决议的高阶逻辑的自动定理供体，该定理供应商已应用于各种问题，最著名的是Gödel的本体论证明了上帝的存在（请参阅章节） 4.6逻辑和哲学）。 LEO-II已被LEO-III取代，该LEO-III实现了在多代理黑板体系结构中运行的高阶阶数偏式演算，以进行并行证明搜索；该体系结构允许使用Leo-III的本机证明微积分独立运行代理，以及以合作的方式，是外部，专业，一年和高级定理的代理商，以及型号的定理和模型发现者（Benzmüller，Steen＆Wisniewski 2017，Steen和Steen和Steen和Steen和Benzmüller2021）。

3.2非古典逻辑

非古典逻辑（HAACK 1978），例如模态逻辑，直觉逻辑，多价值逻辑，自身史学逻辑，非单调推理，常识性和默认推理，相关性逻辑，paraconsistent逻辑等，因此一直在越来越多地引起人们的注意自动推理社区。原因之一是将自动推力技术扩展到新的逻辑领域的自然愿望。另一个原因是需要机械化非古典逻辑，以试图为人工智能提供合适的基础。第三个原因是渴望攻击某些问题上太大而无法用纸和铅笔处理的问题。确实，自动化非古典逻辑中的某些工作提供了工作中自动推理程序的主要示例。为了说明说明，Ackerman常数问题要求相关性逻辑R中的非等效公式数量。实际上有3,088个这样的公式（Slaney 1984），并且通过“夹心”在下限和上限之间找到该数字，一个任务涉及约束2040020-元素模型的广阔宇宙，以寻找拒绝R中的非理论的模型没有自动推理计划的协助，将无法获得。

已经有三种基本方法可以自动解决非古典逻辑中问题（McRobie 1991）。当然，一种方法是尝试机械化非古典演绎计算。另一个是简单地在一阶逻辑中简单地提供问题的等效表述，然后让经典的定理供体处理它。第三种方法是在将应用分辨率或连接矩阵方法的一阶框架中制定非古典逻辑的语义。 （Pelletier等人，2017年）描述了一种自动推理系统的自动推理系统，该系统具有“间接”方法，即翻译和真实价值方法，以证明其定理。

模态逻辑

模态逻辑在计算科学作为知识和信念的逻辑，程序的逻辑以及分布式和并发系统的规范中发现了广泛的用途。因此，一个在模态逻辑（例如K，K4，T，S4或S5）中自动推理的程序将具有重要的应用程序。除S5以外，这些逻辑还共享经典逻辑的一些重要的元态结果，例如切割淘汰，因此可以为它们提供无剪切（模态）序列的计算，以及它们的自动化技术。连接方法（Andrews 1981，Bibel 1981）在帮助理解这些模态序列计算引起的搜索空间中的冗余来源方面发挥了重要作用，并且不仅为模态逻辑提供了统一的框架，而且还为直觉和经典逻辑提供了统一的框架。同样（Wallen 1990）。当前自动化模态逻辑推理的努力围绕上述翻译方法，即将模态逻辑嵌入经典逻辑中，然后使用现有的自动推理系统来证明后者的定理。 （Benzmüller＆Paulson 2013）展示了如何将量化的模态逻辑嵌入简单类型的理论，证明了嵌入的健全性和完整性，并通过简单的实验证明了如何使用现有的高阶定理掠夺者在模态逻辑中自动化证明。该方法也可以扩展到高阶模态逻辑（Benzmüller＆Paleo 2015）。事实上，经典高阶逻辑中的嵌入可以用作普遍推理的一种手段（Benzmüller，2019年）。也就是说，嵌入提供了一个通用的逻辑推理框架，该框架使用经典的高级逻辑作为一种金属含量，在其中可以代表其他各种经典和非经典逻辑。自由逻辑和类别理论的语义嵌入方法（Benzmüller＆Scott 2020）提供了对普遍性主张的进一步证据。嵌入为自动推论带来了许多实际好处：普遍性，统一性，符号和推理的表现力，以及现有强大强大的自动化定理工具的现成可用性，这些工具已知是合理的。

直觉逻辑

直觉逻辑可以自动化不同的方式。一种是直接实施Gentzen的序列和自然推论，LJ和NJ的直觉版本。这种方法继承了这些微积分所享有的更强的归一化结果，比其经典的机械化更紧凑。机械化直觉逻辑的另一种方法是利用其语义相似性与模态逻辑S4，然后在S4的自动实现中恢复。自编写符合规范的程序以来，自动化直觉逻辑在软件开发中具有应用程序，与在直觉逻辑中证明规范的问题相对应（Martin-Löf1982）。自动化证明施工过程的系统将在算法设计中具有重要的应用，还可以在建设性的数学中使用。 NUPRL（Constable等，1986）是一个支持特定数学理论的计算机系统，即建设性类型理论，其目的是在证明开发过程中提供帮助。重点是基于逻辑的工具来支持编程和实施形式的计算数学。多年来，NUPRL项目的范围已从“证明 - 程序”扩展到“系统 - 理论”。 COQ系统在精神和基于咖喱螺旋同构的基础上，在归纳构造的计算中形式化了其证明，这是一种具有丰富类型的λ-Calculus，包括依赖类型在内（Coququand＆Huet 1988，Coquand＆Paulin-Mohring，1988年） ）。像NUPRL一样，COQ旨在帮助开发数学证明以及从其正式规范中的计算机程序。

4. 应用

4.1逻辑编程

逻辑编程特别是语言序言（Colmerauer等，1973），可能是自动定理证明的最重要，最广泛的应用。在1970年代初期，发现逻辑可以用作编程语言（Kowalski 1974）。逻辑编程与其他传统形式的编程形式的区别是，逻辑程序为了解决问题，不能明确说明如何执行特定的计算。取而代之的是，逻辑程序规定了问题是什么，然后将其实际求解的任务委派给了基础定理供体。在Prolog中，定理占据基于称为SLD分辨率的分辨率的改进。 SLD分辨率是线性输入分辨率的一种变体，它结合了选择下一个要解决的文字的特殊规则； SLD分辨率还考虑到一个事实，即在计算机的内存中，实际上是订购了子句中的文字，也就是说，它们形成了一个序列，而不是集合。序言计划由陈述已知事实和规则的条款组成。例如，以下条款对飞行连接做出了一些断言：

飞行（多伦多，伦敦）。

航班（伦敦，罗马）。

航班（芝加哥，伦敦）。

航班（x，y）： - 飞行（x，z），飞行（z，y）。

条款飞行（伦敦多伦多）是事实，而飞行（x，y）： - 飞行（x，z），飞行（z，y）是一条规则，由公约写为反向的条件（符号“： - - - - ”意思是“如果逗号”的意思是“大写”是变量。前者指出，多伦多和伦敦之间存在飞行联系。后者指出，如果对于某些城市Z，X和Z之间的飞行以及Z和Y之间的飞行。文字：事实是没有负面文字的计划条款，而规则至少具有一个负面字面意义。

（请注意，在标准子句表示法中，上例中的程序规则将写为 Flight(X,Y)∨∼flight(X,Z)∨∼flight(Z,Y)。）程序规则的具体形式为有效地表达以下形式的陈述：“如果这里的这些条件同时满足，那么另一个事实就会随之而来”。最后，目标是一个没有正面文字的 Horn 子句。这个想法是，一旦编写了 Prolog 程序 Π，我们就可以尝试确定新子句 γ（目标）是否由 Π,Π⊨γ 蕴含； Prolog 证明者通过尝试从 Π∪{∼γ} 导出矛盾来做到这一点。我们应该指出，程序事实和规则本身并不能产生矛盾；程序事实和规则本身并不能产生矛盾。过程中必须有一个目标。与输入解析一样，SLD 解析对于一阶逻辑来说不是完整的反驳，但对于 Prolog 程序的 Horn 逻辑来说是完整的。基本定理：如果 Π 是 Prolog 程序，γ 是目标子句，则 Π⊨γ iff Π∪{∼γ}⊢[] 通过 SLD 解析 (Lloyd 1984)。

例如，要查明是否有从多伦多飞往罗马的航班，需要 Prolog 证明者查看子句 Flight(toronto, rome) 是否来自给定程序。为此，证明者将 ∼flight(toronto,rome) 添加到程序子句中，并尝试通过 SLD 解析导出空子句 []：

1 航班（多伦多、伦敦） 计划条款

2航班（伦敦、罗马） 计划条款

3航班（芝加哥、伦敦） 计划条款

4 航班(X,Y)∨∼航班(X,Z)∨∼航班(Z,Y) 计划条款

5 ∼航班(多伦多, 罗马) 否定结论

6 ∼航班(多伦多,Z)∨∼航班(Z,罗马) Res 5 4

7 ∼航班(伦敦、罗马) Res 6 1

8 [] 决议 7 2

Prolog 程序中规则的条件形式增加了它们的可读性，并且还允许以更友好的方式推理潜在的反驳：为了证明多伦多和罗马之间有航班，flight(toronto,rome)，将此子句与如果航班（多伦多，Z）和航班（Z，罗马）都可以证明，则程序中第四个子句的后续航班（X，Y）本身即可证明。这可以看作是替换 {Z← london} 下的情况，因为 Flight(toronto,london) 和 Flight(london,rome) 本身都是可证明的。请注意，定理证明者不仅确定多伦多和罗马之间有航班，而且还可以通过从证明中使用的统一中提取实际行程“多伦多-伦敦-罗马”。