真值树方法

真值树
术语名称	真值树
英语名称	analytic tableau
别名	truth tree, 表列, 语义tableau, semantic_tableau

analytic tableau 方法或真值树(truth tree)方法是分析一组命题公式或谓词公式的可满足性（一致性）的一种方法。

根据定义，一个可满足公式或一组一致的公式，一定有一个使其（或一组全部）为真的指派（命题逻辑）或赋值（谓词逻辑），也对应着一组文字（即命题变元或命题变元的否定）为真或自变量取值。真值树方法通过树形结构逐步按主联结词（及量化表达式）拆分公式，将对公式的讨论转化为对其每个直接子公式的分支讨论，并重复进行，直到把原来的公式拆成文字（或谓词与个体词的组合）为止。根据每个讨论分支中的互补文字的出现排除一定不成立的讨论分支，最后被拆尽仍然有未排除分支的就说明其成真的指派/赋值存在。

原理

可以根据以下思路得到这种方案。

使一个公式集合中全体公式为真的指派可以在一些保证公式复杂性降低的变换中保持一致。比如，公式集合 [math]\displaystyle{ \{(p\lor q)\land p\} }[/math] 和 [math]\displaystyle{ \{p\lor q, p\} }[/math] 的满足情况一致，公式集合 [math]\displaystyle{ \{p\lor q\} }[/math] 的满足情况和 [math]\displaystyle{ \{p\} }[/math] 与 [math]\displaystyle{ \{q\} }[/math] 的可满足情况的并集一致。
为了便于处理多个公式，我们可以看作只向公式集中添加新的公式，也就是说，把集合 [math]\displaystyle{ \{(p\lor q)\land p\} }[/math] 变换为集合 [math]\displaystyle{ \{(p\lor q)\land p, p\lor q, p\} }[/math] 、集合 [math]\displaystyle{ \{p\lor q\} }[/math] 变换为 [math]\displaystyle{ \{p\lor q, p\} }[/math] 与 [math]\displaystyle{ \{p\lor q, q\} }[/math] ，考虑两个新集合满足情况的并集。每个步骤中添加的公式都是原来的子公式，也就是会变短，因此这样新添加的公式是有限的。经过有限步后，一定可以把相关的公式都添加进来。（也有的说法中，会去除对应集合中已处理的不是文字的公式）
直接添加的公式，按正常添加处理；需要分成两个不同集合的，按照原集合和添加公式分支，即集合 [math]\displaystyle{ \{p\lor q\} }[/math] 可以表示为公共部分 [math]\displaystyle{ \{p\lor q\} }[/math] 和两个分支 [math]\displaystyle{ \{p\} }[/math] 、 [math]\displaystyle{ \{q\} }[/math] 。
最后添加的公式一定是形如 [math]\displaystyle{ p }[/math] 和 [math]\displaystyle{ \lnot p }[/math] 的文字。如果存在互补文字（即集合公共部分与分支部分加在一起，对某个命题变元同时存在 [math]\displaystyle{ p }[/math] 和 [math]\displaystyle{ \lnot p }[/math] ），则这个分支判定为不可满足，被关闭(close)，成为一个闭合(closed)分支。一个分支被关闭后，无论添加什么都不可能不再是可满足的，因此不需要进一步讨论。
如果一个分支没有被闭合，但是没有未处理的公式，也就是没有新的可添加公式了，那么这个分支中不存在冲突，对应的公式集与原公式集存在同一个成真指派。此时原公式集有成真指派，是一致的。

算法

输入：一个公式或一个公式集。
相关名词
- 中间数据：按照下一节中描述的分支规则，公式本身可以描述为一棵树。
- 树中的叶结点、分支（指叶结点的路径）一一对应，可混合使用这两个词语。
- 每个分支有开放(open)或闭合(closed)的标记，也可以表述为放入开放（闭合）分支集/从开放（闭合）分支集中取出。
- 每个结点上都有一个公式集，其中包含至少一个公式。（注：部分材料中，多个公式的结点被描述为一串只具有一个公式的结点，其他描述需要对应修改）
- 一个结点的公式或一个分支的公式指这个结点的路径上全部公式集的不相交的并集。

在树中创建根结点，将这组公式作为根结点数据，将这一结点标记为开放。
若开放结点集非空，重复：
- 从开放结点集中取出一个有待处理公式的开放叶结点（理论上不限顺序，深度优先搜索或广度优先搜索甚至不规则搜索都没关系），对其中任取一个待处理公式（理论上不限顺序，由于一般来说越靠近根结点越复杂，建议先处理靠近根结点的公式），按下一节中描述的规则为其添加一个或两个子结点，将本结点标记为已处理，新增结点标注为开放。
- 检查新增结点。若新增结点中有文字，且这一分支的公式中恰有一个文字与其构成互补文字，则这一结点标注为闭合。
若此时全部分支被闭合，判定原公式不可满足（或原公式集不一致）。
此时存在开放分支且无待处理公式，判定原公式可满足（或原公式集一致）。

分支规则

规则表示方式

对每一个公式，其可能不需要处理、处理时向当前分支添加一个新结点、处理时向当前分支添加两个新结点变成两个分支。

命题逻辑

对一个有联结词 [math]\displaystyle{ \lnot,\land,\lor,\rightarrow,\leftrightarrow }[/math] 的公式集，可以考虑以下规则：

形式	处理方式
[math]\displaystyle{ p }[/math]	不需要处理
[math]\displaystyle{ \lnot p }[/math]	不需要处理
[math]\displaystyle{ \lnot\lnot\phi }[/math]	[math]\displaystyle{ \{\phi\} }[/math]
[math]\displaystyle{ \phi\land\psi }[/math]	[math]\displaystyle{ \{\phi,\psi\} }[/math]
[math]\displaystyle{ \lnot(\phi\land\psi) }[/math]	[math]\displaystyle{ \{\lnot\phi\},\{\lnot\psi\} }[/math]
[math]\displaystyle{ \phi\lor\psi }[/math]	[math]\displaystyle{ \{\phi\},\{\psi\} }[/math]
[math]\displaystyle{ \lnot(\phi\lor\psi) }[/math]	[math]\displaystyle{ \{\lnot\phi,\lnot\psi\} }[/math]
[math]\displaystyle{ \phi\rightarrow\psi }[/math]	[math]\displaystyle{ \{\lnot\phi\},\{\psi\} }[/math]
[math]\displaystyle{ \lnot(\phi\rightarrow\psi) }[/math]	[math]\displaystyle{ \{\phi,\lnot\psi\} }[/math]
[math]\displaystyle{ \phi\leftrightarrow\psi }[/math]	[math]\displaystyle{ \{\phi,\psi\},\{\lnot\phi,\lnot\psi\} }[/math]
[math]\displaystyle{ \lnot(\phi\leftrightarrow\psi) }[/math]	[math]\displaystyle{ \{\lnot\phi,\psi\},\{\phi,\lnot\psi\} }[/math]

谓词逻辑

在以上规则基础上，增加 [math]\displaystyle{ \forall,\exists }[/math] ，可以考虑以下规则，需要注意其中部分操作允许任意项：

形式	处理方式
[math]\displaystyle{ \forall x\phi }[/math]	[math]\displaystyle{ \{\phi[t/x]\} }[/math] ，其中 [math]\displaystyle{ t }[/math] 是任意项
[math]\displaystyle{ \lnot\forall x\phi }[/math]	[math]\displaystyle{ \{\lnot\phi[a/x]\} }[/math] ，其中 [math]\displaystyle{ a }[/math] 是未自由出现本在分支任意公式中的个体常项或个体变项
[math]\displaystyle{ \exists x\phi }[/math]	[math]\displaystyle{ \{\phi[a/x]\} }[/math] ，其中 [math]\displaystyle{ a }[/math] 是未自由出现本在分支任意公式中的个体常项或个体变项
[math]\displaystyle{ \lnot\exists x\phi }[/math]	[math]\displaystyle{ \{\lnot\phi[t/x]\} }[/math] ，其中 [math]\displaystyle{ t }[/math] 是任意项
[math]\displaystyle{ \lnot(\phi\land\psi) }[/math]	[math]\displaystyle{ \{\lnot\phi\},\{\lnot\psi\} }[/math]
不需要根据	[math]\displaystyle{ t=t }[/math]
[math]\displaystyle{ t=t',\phi[t/x] }[/math]	[math]\displaystyle{ \{\phi[t'/x]\} }[/math] ，其中 [math]\displaystyle{ t,t' }[/math] 是任意项且在 [math]\displaystyle{ \phi }[/math] 中可自由代入
[math]\displaystyle{ t=t',\phi[t'/x] }[/math]	[math]\displaystyle{ \{\phi[t/x]\} }[/math] ，其中 [math]\displaystyle{ t,t' }[/math] 是任意项且在 [math]\displaystyle{ \phi }[/math] 中可自由代入

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
	Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性