分析表法

在证明理论中，是句法和相关逻辑的决策程序，也是一阶逻辑公式的证明程序。一个分析表是为一个逻辑公式计算的树状结构，在每个节点上都有一个要证明或反驳的原公式的子公式。计算构建了这个树，并使用它来证明或反驳整个公式。tableau方法也可以确定各种逻辑的有限公式集的可满足性。

对于反驳表法来说，其目的是要证明一个公式的否定不能被满足。从主连接词开始，有处理每个常用连接词的规则。在许多情况下，应用这些规则会导致副表层一分为二。定量词被实例化了。如果一个表格的任何分支导致明显的矛盾，该分支就会关闭。如果所有的分支都关闭了，证明就完成了，原始公式就是一个逻辑真理。尽管分析表法的基本思想来自于结构性证明理论的切割消除定理，但表法计算的起源在于逻辑连接词的意义（或语义），因为与证明理论的联系是在最近几十年才建立的。更具体地说，表计算由一个有限的规则集合组成，每个规则都规定了如何将一个逻辑连接词分解成其组成部分。这些规则通常用有限的公式集来表达，尽管有些逻辑我们必须使用更复杂的数据结构，比如多集、列表，甚至是公式树。因此，集表示{集、多集、列表、树}中的任何一个。如果每个逻辑连接词都有这样的规则，那么这个程序最终会产生一个只由原子公式和它们的否定式组成的集合，它不能再被进一步分解了。就有关逻辑的语义而言，这样一个集合很容易被识别为可满足或不可满足。为了跟踪这个过程，表本身的节点以树的形式列出，这个树的分支以系统的方式被创建和评估。这样一种搜索这棵树的系统性方法，产生了一种进行演绎和自动推理的算法。请注意，无论节点是否包含集、多集、列表或树，都存在这棵较大的树。

它可以用来检查有效性或必然性：如果一个公式的否定是不可满足的，那么它就是有效的，而公式命题表格的主要原则是试图将复杂的公式分解成更小的公式，直到产生互补的字词对或无法进一步扩展。该方法在一棵树上工作，树上的节点被标记为公式。在每一步，这棵树都会被修改；在命题的情况下，xxx允许的修改是增加一个节点作为叶子的后代。这个过程开始于生成由集合中的所有公式组成的树，以证明不满足性。然后，以下程序可以非确定性地重复应用。

挑选一个开放的叶子节点。在所选节点上方的分支上挑选一个适用的节点。应用适用的节点，这相当于根据一些扩展规则扩展所选叶子节点下方的树。对于每个新创建的节点，既是一个字面/否定字面，并且其补码出现在同一分支的先前节点中，标记该分支为关闭。将所有其他新创建的节点标记为开放节点。最终，这个过程会终止，因为在某些时候，每个适用的节点都会被应用，而扩展规则保证树中的每个节点都比用来创建它的适用节点更简单。