自动推理（二）

独立共同发现的线性解决方案（Loveland 1970，Luckham 1970）总是解决针对最近导出的解决方案的条款。这为推导提供了一个简单的“线性”结构，提供了直接的实现；然而，线性分辨率保留了反驳的完整性。使用线性解析，我们只需八步即可推导出上例中的空子句：

1 P(x)∨Q(x) 假设

2 ∼P(x)∨R(x) 假设

3 ∼Q(x)∨R(x) 假设

4 ∼R(a) 否定结论

5 ~P(a) 研究 2 4

6 Q(a) 研究 1 5

7 R(a) 研究 3 6

8 [ ] 决议 4 7

除了无限制包含之外，到目前为止提到的所有策略都保持了反驳的完整性。效率是自动推理中的一个重要考虑因素，有时人们可能愿意牺牲完整性来换取速度。单位分辨率和输入分辨率是线性分辨率的两种改进。在前者中，已解决的子句之一始终是文字；在前者中，已解决的子句之一始终是文字。在后者中，总是从原始集合中选择一个已解决的子句进行反驳。尽管有效，但这两种策略都不完整。排序策略对推导中出现的谓词符号、术语、文字或子句施加某种形式的部分排序。有序解析不将子句视为文字集，而是视为文字的序列（线性顺序）。有序解析非常有效，但与单位和输入解析一样，反驳并不完整。最后，必须指出的是，某些策略会以牺牲其他方面为代价来改善推论过程的某些方面。例如，一种策略可能会减少证明搜索空间的大小，但代价是增加最短反驳的长度。定理证明策略的分类和详细介绍可以在 Bonacina 1999 中找到；有关决议的相对复杂性（即效率衡量标准）的讨论，请参阅 Buresh-Oppenheim & Pitassi 2003 和 Urquhart 1987。

有几种基于分辨率或分辨率细化的自动推理程序。 Otter（后继为 Prover4）是自动推理发展的驱动力（Wos、Overbeek、Lusk & Boyle 1984），但它已被 Vampire 等功能更强大的程序取代（Voronkov 1995、Kovács & Voronkov 2013）。解决方案还为流行的逻辑编程语言 Prolog (Clocksin & Mellish 1981) 提供了底层逻辑计算机制。

2.2 顺序推导

希尔伯特式演算（Hilbert and Ackermann 1928）传统上被用来表征逻辑系统。这些演算通常由一些公理图式和少量规则组成，这些规则通常包括肯定前件和替换规则。尽管它们满足所需的理论要求（健全性、完整性等），但这些演算中的证明构造方法很困难，并且不反映标准实践。 Gentzen 的目标是“建立一种形式主义，尽可能准确地反映数学证明中涉及的实际逻辑推理”（Gentzen 1935）。为了完成这项任务，Gentzen 分析了证明构造过程，然后设计了两种经典逻辑演绎演算：自然演绎演算 NK 和序贯演算 LK。 （实际上Gentzen首先设计了NK，然后引入LK来进行元理论研究）。演算在很大程度上实现了他的目标，同时设法确保了合理性和完整性。这两种演算的特点是推导规则数量相对较多，公理模式简单。在这两种演算中，LK 是在自动推理程序的实现中使用最广泛的一种，也是我们将首先讨论的一种； NK 将在下一节中讨论。

尽管 LK 规则的应用会影响逻辑公式，但这些规则被视为操纵的不是逻辑公式本身，而是序列。数列是 Γ→Δ 形式的表达式，其中 Γ 和 Δ 都是（可能为空）公式集。 Γ 是后件的前件，Δ 是后件。序列可以这样解释：让 I 成为一种解释。然后，

I 满足连续的 Γ→Δ（写为：I⊨Γ→Δ） iff

要么 I⊭α （对于某些 α ε γ ）或 I ⊨ β （对于某些 β ε Δ ）。

换句话说，

I⊨Γ→Δ iff I⊨(α1 &…& αn)⊃(β1∨…∨βn)，其中 α1 &…& αn 是 Γ 中公式的迭代合取，β1∨…∨βn 是以下公式的迭代析取Δ 中的那些。

如果 Γ 或 Δ 为空，则它们分别有效或不可满足。 LK 的公理是连续的 γ→Δ，其中 γ∩Δ≠∅。因此，要求 → 符号的每一侧出现相同的公式意味着 LK 的公理是有效的，因为没有任何解释可以使 Γ 中的所有公式为真，同时使 Δ 中的所有公式为假。 LK 每个逻辑连接词有两条规则，外加一条额外规则：剪切规则。

公理剪切规则

γ,α→Δ,α

γ→Δ,α α,λ→Σ

γ,λ→Δ,Σ

先行规则 (θ→) 后继规则 (→θ)

&→

γ,α,β→Δ

γ,α&β→Δ

→&

γ→Δ,α γ→Δ,β

γ→Δ,α&β

∨→

γ,α→Δ γ,β→Δ

γ,α∨β→Δ

→∨

γ→Δ,α,β

γ→Δ,α∨β

⊃→

γ→Δ,α γ,β→Δ

γ,α⊃β→Δ

→⊃

γ,α→Δ,β

γ→Δ,α⊃β

⊃≡

γ,α,β→Δ γ→Δ,α,β

γ,α=β→Δ

⊃

γ,α→Δ,β γ,β,→Δ,α

γ→Δ,α=β

∼→

γ→Δ,α

γ,∼α→Δ

→～

γ,α→Δ

γ→Δ,∼α

∃→

γ,α(a/x)→Δ

Γ,∃xα(x)→Δ

→∃

γ→Δ,α(t/x),∃xα(x)

γ→Δ,∃xα(x)

∀→

γ,α(t/x),∀xα(x)→Δ

γ,∀xα(x)→Δ

→∀

γ→Δ,α(a/x)

γ→Δ,∀xα(x)

规则线上方的序列称为规则的前提，线下方的序列称为规则的结论。量化规则 ∃→ 和 →∀ 有一个特征变量条件限制了它们的适用性，即 a 不能出现在 Γ,Δ 或量化句子中。这一限制的目的是确保替换过程中使用的参数 a 的选择是完全“任意”的。

LK 中的证明被表示为树，其中树中的每个节点都用序列标记，并且原始序列位于树的根部。节点的子节点是在该节点应用规则的前提。树的叶子上标有公理。这是集合 {∀x(P(x)∨Q(x)),∀x(P(x)⊃R(x)),∀x(Q(x)) 中 ∃xR(x) 的 LK 证明)⊃R(x))}。在下面的树中，Г代表这个集合：

Г,P(a)→ P(a),R(a),∃xR(x) Г,P(a),R(a)→ R(a),∃xR(x)

Г,P(a),P(a)⊃R(a)→R(a),∃xR(x)

Г,P(a)→R(a),∃xR(x)

Г,Q(a)→ Q(a),R(a),∃xR(x) Г,Q(a),R(a)→ R(a),∃xR(x)

Г,Q(a),Q(a)⊃R(a)→R(a),∃xR(x)

Г,Q(a)→R(a),∃xR(x)

Г,P(a)∨Q(a)→R(a),∃xR(x)

∃xR(x)→R(a),∃xR(x)

∃xR(x) → ∃xR(x)

在我们的示例中，证明树中的所有叶子都标有公理。这确立了 Γ→∃xR(x) 的有效性，从而确立了 Γ⊨∃xR(x) 的事实。 LK采用间接的方法来证明结论，这是LK和NK之间的一个重要区别。 NK 构建了一个实际证明（根据给定假设得出的结论），而 LK 构建了一个证明来证明证明（根据假设得出的结论）的存在。例如，为了证明 α 被 Г 蕴含，NK 从 Г 构造了 α 的逐步证明（假设存在）；相反，LK 首先构造了连续的 Γ→α，然后尝试通过证明它不能被伪造来证明其有效性。这是通过搜索一个反例来完成的，该反例使（其中的所有句子） 为真并使 α 为假：如果搜索失败，则反例不存在，因此后继有效。在这方面，LK 中的证明树实际上是反驳证明。与解析一样，LK 是反驳完成的：如果 Γ⊨α 那么后续的 Γ→α 有一个证明树。

目前来看，LK并不适合自动扣除，并且在有效实施之前必须克服一些障碍。当然，原因是 LK 完整性的陈述只需为每个蕴涵关系断言证明树的存在，但推理程序的任务更为困难，即实际上必须构造一个证明树。一些主要障碍：首先，LK 没有指定在构建证明树时必须应用规则的顺序。其次，作为第一个问题的特殊情况，规则 ∀→ 和 →∃ 规则中的前提继承了应用该规则的量化公式，这意味着这些规则可以重复应用于发送证明搜索的同一公式进入无限循环。第三，LK没有表明在应用规则时接下来必须选择哪个公式。第四，量词规则没有提供关于在其部署中必须使用哪些术语或自由变量的指示。第五，作为前一个问题的特殊情况，量词规则的应用可能会导致无限长的树枝，因为在实例化中使用的正确术语永远不会被选择。幸运的是，正如我们将在下面提示的那样，可以成功解决这些问题。

LK中的公理序列是有效的，如果其前提为，则规则的结论是有效的。这个事实使我们能够在任一方向上应用LK规则，从公理到结论，或从结论到公理。同样，除了削减规则外，所有规则的前提都是其各自结论的副形。出于自动扣除的目的，这是一个重要的事实，我们希望分配削减规则；幸运的是，LK的无剪裁版本保留了其反驳完整性（Gentzen 1935）。这些结果为以倒退的方式建造证明树提供了有力的案例。的确，通过这种方式，随着剪切LK的反驳，随着剪切LK的进行越来越简单，因为子形式比其父式公式更简单。此外，就命题规则而言，进入树上的新子形成完全由无剪切的LK规则决定。此外，假设可以完成证明树，则分支最终最终会产生原子，并且可以快速确定公理的存在。向后工作的另一个原因是，无剪切LK的真实功能片段是汇合的，因为非量化器规则的应用是无关紧要的：如果有证据，无论您做什么，您，您，您会遇到它！为了将量词规则带入图片中，可以安排事物，以便所有规则都有被部署的机会：在应用任何量词规则之前，尽可能地将所有非量化器规则申请。这要解决第一个和第二个障碍，而且现在如何处理第三个障碍并不难。可以通过要求从Herbrand Universe中选择要使用的术语来解决第四和第五障碍（Herbrand 1930）。

在自动定理中使用序列型结石证明是通过机械化数学的努力开始的（Wang 1960）。当时，决议引起了自动推理社区的大部分注意力，但是在1970年代，一些研究人员开始进一步研究非分辨率方法（Bledsoe 1977），促使努力努力开发更加面向人类的定理系统（ Bledsoe 1975，Nevins 1974）。最终，依次的推论再次获得了动力，尤其是在重新分配为分析表中的动力（Fitting 1990）。 Tableaux中使用的演绎方法基本上是无剪切的LK，其套件代替了序列。

2.3自然扣除

尽管LK和NK通常都被标记为“自然扣除”系统，但由于其更自然，类似人类的证明构建方法，后者更应获得标题。 NK的规则通常以隐式理解的上下文作用在标准逻辑公式上，但在文献中通常也给出了它们在“判断”上更明确地作用，即γ⊢α的表达，其中γ是的表达一组公式和α是一个公式。这种形式通常被理解为使转移有γ的证明（Kleene 1962）。在1935年和1965年的普拉维茨（Prawitz）之后，我们采取了以前的方法。系统NK没有逻辑公理，并为每个逻辑结缔组织提供了两个简介 - 淘汰规则：

简介规则（θi）消除规则（θe）

＆我

αβ

α＆β

＆e

α1和α2

αi（i = 1,2）

∨i

αi（i = 1,2）

α1∨α2

∨e

α∨β[α -γ] [β -γ]

γ

⊃i

[α-β]

α⊃β

⊃e

αα⊃β

β

吗

[α - β] [β-α]

α−β

◦e

αi（i = 0,1）α0α1

α1-i

〜我

[α-⊥]

〜α

〜e

[〜α - ⊥]

α

∃i

α（T/X）

∃Xα（x）

∃e

∃xα（x）[α（a/x） - β]

β

∀i

α（A/X）

∀Xα（x）

∀e

∀Xα（x）

α（T/X）

一些说明：首先，表达[α -γ]表示α是γ证据中的辅助假设，最终被放电，即丢弃。例如，∃e告诉我们，如果在构建证明的过程中已经衍生出∃xα（x），并且以α（a/x）为辅助假设，则允许β（a/x）作为辅助假设。其次，在∃e和∀I中，本征参数a必须是陌生的，在该规则的结论中，没有充电的“主动” - “主动” - 毫无用处，而对于∃e的结论则是∃Xα（x）。第三，⊥是两个矛盾的公式，β和〜β的速记。最后，NK是完整的：如果γ⊨α，则使用NK规则有γ的证明。

与LK一样，在NK中构建的证据被表示为树木，证明的结论位于树的根部，问题的假设位于叶子上。 （证明通常也作为判断序列γ⊢α的序列，从印刷页面的顶部到底部。）这是∀X（p（x）∨ q（x）），∀x（p（x）⊃R（x））和∀x（q（x）⊃R（x））：

∀x（p（x）∨q（x））

p（a）∨q（a）

∀X（p（x）⊃R（x））

p（a）⊃R（a）

[p（a） - r（a）]

r（a）

∀x（q（x）⊃R（x））

Q（a）⊃R（a）

[q（a）—r（a）]

r（a）

r（a）

∃xr（x）

与LK一样，预防构建的前进策略并不是充分的重点。因此，尽管向前读了证据，也就是说，从叶到根，从逻辑上讲，从假设到结论，这并不是它们通常构造的方式。通过以相反顺序应用规则实施的向后链接策略更有效。上面在实施序列推论中讨论的许多障碍也适用于自然推论。这些问题可以以类似的方式处理，但是自然推论本身会引入一些问题。例如，正如⊃引言规则所建议的那样，为了证明α⊃β的目标可以试图证明β的假设是α。但是请注意，尽管目标α⊃β与任何其他引入规则的结论不符，但它与所有消除规则的结论匹配，推理计划也需要考虑这些路线。与前向链接类似，这里有设定与证明无关的目标的风险，并且可能导致该计划误入歧途。机智：是什么阻止程序进入越来越大的连词的永无止境的过程？或者，有什么可以防止⊃灭绝的不受控制的落后应用链？幸运的是，NK享有subformula特性，从某种意义上说，每个公式进入自然推力证明都可以限制为γ∪δ∪{α}的子形式，其中δ是由〜-淘汰规则做出的一组辅助假设。 。通过利用Subformula属性，自然扣除自动扣除可以大大减少其搜索空间，并将淘汰规则的向后应用受到控制（Portoraro 1998，Sieg＆Byrnes 1996）。如果人们愿意将NK逻辑的范围限制在其直觉片段中，可以实现进一步的收益，在这种意义上，每个证明都具有正常形式，因为即可通过简介规则获得任何公式，然后被消除规则消除（Prawitz，1965年） ）。

使用NK扣除额的自动定理证明系统的实现是出于渴望具有与人类用户使用的相同证明格式和方法的程序原因的愿望。在教育领域尤其如此，在该领域中，学生在一个类似NK的微积分进行互动构造正式的证据的领域，在定理供体的指导下，随时准备在需要时提供帮助（Portoraro 1994，Suppes 1981）。其他以研究为导向的，定理的牺牲品确实存在于NK的精神（Pelletier 1998），但很少见。

2.4矩阵连接方法

矩阵连接方法的名称（Bibel 1981）指示其运行方式。术语“矩阵”是指表示问题的逻辑公式集的形式； “连接”一词是指方法对这些公式的操作方式。为了说明工作中的方法，我们将使用命题逻辑中的一个示例，并证明R需要P∨Q，P⊃R和Q⊃R。这是通过确定公式来完成的

（p∨q）＆（p⊃r）＆（q⊃r）＆〜r

不满意。为此，我们首先将其转换为结合的正常形式：

（p∨q）＆（〜p∨r）＆（〜q∨r）＆〜r

然后，此公式表示为矩阵，每行一个连词，并且在一行中，每列一个分离：

p q

〜p r

〜q r

〜r

现在的想法是探索通过此矩阵运行的所有可能的垂直路径。垂直路径是从矩阵中的每一行选择的一组文字，因此每个文字都来自另一行。垂直路径：

路径1 p，〜p，〜q和〜r

路径2 p，〜p，r和〜r

路径3 p，r，〜q和〜r

路径4 p，r，r和〜r

路径5 q，〜p，〜q和〜r

路径6 q，〜p，r和〜r

路径7 q，r，〜q和〜r

路径8 q，r，r和〜r

路径是互补的，如果它包含两个互补的文字。例如，路径2是互补的，因为它具有p和〜p，但路径6也是如此，因为它均包含r和〜r。请注意，一条道路包括两个互补的文字，就没有意义，因为它本身已经成为互补的。这通常可以大大减少要检查的路径数量。无论如何，上述矩阵中的所有路径都是互补的，并且这一事实确定了原始公式的不可满足性。这是矩阵连接方法的本质。该方法可以扩展到谓词逻辑，但这需要其他逻辑设备：skoLemn，可变的重命名，量词重复，通过统一的路径互补性以及在所有矩阵路径上同时取代（Bibel 1981，Andrews 1981）。该方法的变化已在高阶逻辑（Andrews 1981）和非古典逻辑（Wallen 1990）中实现。

2.5术语重写

平等是一个重要的逻辑关系，其自动推力中的行为应得到自己的独立待遇。方程式逻辑，更一般而言，术语重写类似于平等的方程式为重写规则，也称为减少或解调规则。诸如f（a）= a之类的平等语句允许将术语（例如g（c，f（a）））简化为g（c，a）。但是，相同的方程式也有可能产生一个无关紧要的术语：g（c，f（a）），g（c，f（f（a））），g（c，f（f（f（a）） ））），…。术语重写与方程逻辑的区别在于，在术语中，重写方程式用作单向减少规则，而不是在两个方向上工作的平等。重写规则具有T1⇒T2的形式，基本思想是在表达式e中查找术语t，以便用unifierθ统一t统一，以便可以用t2θ替换Eθ中的T1θ。例如，重写规则x +0⇒x允许将succ（scucs（scucd（0）+0）重写为succ（succ（succ（0））。