计算机科学家逻辑/谓词逻辑/语义树

语义树

在本节中，我们将介绍语义树的概念，它可以用来证明解析的完备性。为此，我们假设读者熟悉树、二叉树和树路径的概念。

定义 15

一组子句 $S$ 的语义树是一棵二叉树 $T$ ，其根为 $N_{0}$ ，使得边用文字标记，文字由 $S$ 的 Herbrand 基中的元素构成，使得

如果 $N$ 是一个内部节点，它的两条出边用互补文字 $A$ 和 $\lnot A$ 标记。
在 $T$ 中，到达节点 $N$ 的每条路径中，都不会包含 $I(N)$ 中的互补文字，其中 $I(N)$ 是路径边上的文字集。

定义 16

如果每条路径都包含 Herbrand 基中的每个原子（正或负），则语义树称为完整的。

示例： $S=\{p(x),q(f(x))\}$ ，其 Herbrand 基为

\{p(a),q(a),p(f(a)),q(f(a)),p(f(f(a))),\ldots \}

请注意，对于语义树 $T$ 和节点 $N$ ，集合 $I(N)$ 可以被看作是对基本原子进行真值赋值，就像在 Herbrand 解释中一样。因此，我们称 $I(N)$ 为部分解释。一个完整的语义树对应于对解释的穷尽“枚举”。

定义 17

语义树 $T$ 的一个节点 $N$ 是一个失败节点，如果 $I(N)$ 使 $S$ 中的一个子句的某个基本实例为假，但对于 $N$ 的每个祖先节点 $N'$ ， $I(N')$ 不会使 $S$ 中的任何子句的基本实例为假。
如果语义树 $T$ 中的每条路径都包含一个失败节点，那么该树称为闭合树。
如果闭合语义树中的节点 $N$ 的两个直接子节点都是失败节点，则称该节点为推断节点。

示例： $S=\{p(x),\lnot p(x)\lor q(f(x)),\lnot q(f(a))\}$ ，其中 Herbrand 基是

\{p(a),q(a),p(f(a)),q(f(a)),p(f(f(a))),\ldots \}

令 $T$ 为一个完整的语义树，那么我们称 $T'$ 为相应的闭合树，如果它可以通过在失败节点处剪切所有分支从 $T$ 中获得。

定理 5（Herbrand 定理 - 版本 1）

一组子句 $S$ 是不可满足的，当且仅当对于 $S$ 的每个完整语义树，都存在一个相应的有限封闭语义树。

证明： 假设 $S$ 是不可满足的，并且 $T$ 是 $S$ 的一个完整语义树。对于每条路径 $P$ ，我们都有标签集 $I_{B}$ ，这是一个解释，因为树是完整的。因此， $I_{B}$ 使子句 $C\in S$ 的一个地面实例 $C'$ 为假，因为 $S$ 是不可满足的。由于 $C'$ 中只有有限多个文字，因此必须存在一个失败节点 $N_{B}$ ，它距离根节点有限距离。由于每条路径都有这样的失败节点，因此存在一个相应的封闭语义树 $T'$ ，它是有限的。

对于相反方向，假设对于每个完整语义树 $T$ ，都存在一个相应的有限封闭树 $T'$ 。那么，每条路径都包含一个失败节点，因此，每个解释都使 $S$ 为假；因此 $S$ 是不可满足的。

定理 6（赫布兰德定理 - 版本 2）

一组子句 $S$ 是不可满足的，当且仅当存在一个有限不可满足的集合 $S'$ ，该集合包含 $S$ 中子句的地面实例。

证明： 假设 $S$ 是不可满足的，并且 $T$ 是 $S$ 的一个完备语义树。根据 Herbrand 定理版本 1，存在 $S$ 的一个有限闭合语义树 $T'$ 。设 $S'$ 是在 $T'$ 的所有失败节点上被证伪的子句的基实例集。 $S'$ 是有限的，并且被所有解释所证伪，因此是不可满足的。我们通过逆否命题证明相反的方向。