重点证明

在数理逻辑中，重点证明是通过目标导向的证明搜索产生的一系列分析性证明，是结构证明理论和还原逻辑的研究课题。它们构成了目标导向证明搜索的最一般定义--有人选择一个公式并进行世袭还原，直到结果满足某些条件。

极端的情况是，只有在达到公理的时候，还原才会终止，这就形成了统一证明的子家族。当聚焦证明在某个终止条件下是完整的，则称一个序列微积分具有聚焦属性。

对于系统LK、系统LJ和系统LL，统一证明是集中证明，其中所有原子都被赋予负极性。

许多其他序列计算已被证明具有聚焦属性，特别是S5立方体中模态逻辑的经典和直觉变体的嵌套序列计算。

在直觉逻辑的顺序微积分中，统一证明可以被描述为那些向上阅读时先执行所有右边规则再执行左边规则的证明。

通常，统一证明对于逻辑来说并不完整，也就是说，并非所有的序列或公式都承认统一证明，所以我们考虑的是它们完整的片段，例如直觉逻辑的遗传性Harrop片段。

由于其确定性行为，统一证明搜索已被用作定义逻辑编程语言范式的控制机制。偶尔，统一证明搜索在给定逻辑的序列微积分的变体中实现，其中上下文管理是自动的，从而增加了人们可以定义逻辑编程语言的片段。

聚焦原则最初是通过线性逻辑中同步和异步连接词之间的歧义来分类的，即与上下文互动的连接词和不互动的连接词，这是逻辑编程研究的结果。

它们现在是还原逻辑中一个越来越重要的控制例子，并能极大地改善工业界的证明搜索程序。

聚焦的基本思想是识别和凝聚证明中的非决定性选择，因此一个证明可以被看作是消极阶段（可逆规则被急切地应用）和积极阶段（其他规则的应用被限制和控制）的交替。

根据顺序计算的规则，公式被归入两个类别中的一个，称为正面和负面，例如，在LK和LJ中，公式j∨ψ{displaystylephilorpsi}是正数。是正数。

唯 一的自由是在原子上自由分配极性。对于负的公式，可证明性在右规则的应用下是不变的；同样，对于正的公式，可证明性在左规则的应用下是不变的。

在这两种情况下，人们可以安全地将规则以任何顺序应用于相同极性的遗传子公式。在右规则应用于正公式，或左规则应用于负公式的情况下，可能导致无效的顺序，例如，在LK和LJ中，没有顺序的证明从一个正确的规则开始。

如果一个微积分的原始还原是可证的，那么相同极性的遗传还原也是可证的，那么这个微积分就接受了聚焦原则。也就是说，人们可以承诺专注于分解一个公式及其相同极性的子公式而不损失完整性。

一个序列微积分经常通过在相关的微积分中工作而被证明具有聚焦属性，在这种微积分中，极性明确地控制了哪些规则的适用。

这种系统中的证明处于聚焦、非聚焦或中性阶段，其中前两者的特征是遗传分解；而后者的特征是强制选择聚焦。一个程序可以经历的最重要的操作行为之一是回溯，即返回到计算中做出选择的早期阶段。

在古典逻辑和直觉逻辑的焦点系统中，回溯的使用可以通过伪收缩来模拟。表示极性的改变，前者使一个公式成为负的，后者是正的；并称一个带箭头的公式为中性。