计算机科学家逻辑/命题逻辑/解析图

解析图

在本节中，我们介绍一种演算，即解析图，它作为消解法的替代方案。虽然这种演算是在独立于消解法的情况下发展起来的，但事实证明它有一些有趣的共同特征。最明显的区别是解析图直接作用于公式，不需要将公式转换成子句范式。

解析图 - 简史

解析图演算的发展始于 1950 年代。首先要提到的是 Beth (1955)、Hintikka (1955) 和 Schütte (1956)。他们的目标主要是开发没有元语言结构的演算。后来在 1960 年代，这种演算中推导树和节点的想法，以及在这样的树中用公式标记节点，成名于 Smullyan 在 1968 年引入的解析图的概念。然后，Kanger (1957)、Prawitz (1960)、Wang (1960)、Davis (1960) 和 Maslov (1968) 引入了解析图演算机械化的想法。

后来，解析图的概念被修改和完善，以便在自动推论中使用，例如 Loveland 在 1968 年（模型消除）、Kowalski 和 Kuehner 在 1971 年（SL-消解）以及 Bibel 在 1975 年、Andrews 在 1976 年（连接或配对方法）。如今，有许多基于这项工作的高性能定理证明器。

演算

解析图演算的优点之一是它可以在不将公式转换为子句范式的情况下定义。
示例 给定一组公式 $\{\lnot P\land \lnot (Q\lor R),\lnot (Q\land \lnot R)\}$。我们的目标是构建一棵树，其分支包含用公式标记的节点。

为此，重要的是根据公式的引导连接词来分析公式。Smullyan 观察到，如果非字面量公式被分组到相同类型的公式中，可以节省一些工作：$\alpha$ 用于表示连接类型的公式，$\beta$ 用于表示命题情况下的析取类型的公式。请注意，在上面的例子中，$\lnot (Q\land \lnot R)$ 必须被视为析取类型的公式，因为前面有一个否定符，它位于连结符之前。公式与其类型之间的对应关系总结在表 1 中。字母 $\alpha$ 和 $\beta$ 用于表示（仅表示）相应类型的公式。现在让我们定义解析图演算的基本数据结构以及相应的扩展规则。

定义 13

一个逻辑 $L$ 的 tableau 是一个有限分支树，其节点是来自 $L$ 的公式。tableau $T$ 中的一条分支是 $T$ 中的一条最大路径。当没有混淆时，分支通常与其节点（公式）的集合等同。给定一个来自 $L$ 的公式集 $\Phi$，$\Phi$ 的 tableau 是通过（可能是无限的）一系列应用以下规则构建的。

1. 由单个节点 $true$ 组成的树是 $\Phi$ 的 tableau（初始化规则）。
2. 令 $T$ 是 $\Phi$ 的一个 tableau，$B$ 是 $T$ 中的一条分支，$\psi$ 是 $B\cup \Phi$ 中的一个公式。如果树 $T'$ 是通过扩展 $B$ 通过表格 2 中具有前提 $\psi$ 的 tableau 规则模式的实例一样多的新线性子树构建的，并且新子树的节点是规则实例的扩展中的公式，那么 $T'$ 是 $\Phi$ 的一个 tableau（扩展规则）。

我们示例中的一个 tableau 如图 2 所示。

定义 14

在一个分析表 $T$ 中，对于一个句子集合 $\Phi$，一个分支 $B$ 是封闭的当且仅当 $B\cup \Phi$ 包含一对互补公式 $\phi ,\lnot \phi$，或 $false$；否则，它是开放的。如果分析表的所有分支都是封闭的，那么分析表是封闭的。对于一个公式集合 $\Phi$（其不可满足性），一个分析表证明是一个针对 $\Phi$ 的封闭分析表 $T$。

问题 31（命题逻辑）

给出以下公式的严格分析表证明

1. $\lnot ((A\downarrow B)\downarrow (A\lor B))$
2. $((A\to B)\land (B\to C))\to (\lnot (\lnot C\land A))$

$\Box$

子句范式分析表

现在让我们改进计算方法，专门针对子句集的情况，这些子句集表示以CNF形式的公式。请注意，在合取范式的情况下，我们只有文字，它们通过 $\lor$-连接词连接。因此每个子句都是 $\beta$-类型的。在图 3 中，给出了一个子句集的分析表。来自给定子句集的子句形成了初始分析表；然后只有 $\beta$-规则可用于进一步扩展分析表。

在以下子句范式分析表的正式定义中，我们从一个初始分析表开始，该分析表是通过从给定的子句集S中获取任意子句形成的。对于进一步扩展分析表，可以使用来自S的子句的 $\beta$-规则应用。哪个子句是允许的由一个 *链接条件* 控制。

定义 15

一组子句 $S$ 的子句（范式）真值表是 $S$ 的真值表，其节点是 $S$ 中的文字，并且通过以下规则（可能是无限的）序列来构建。

1. 以 $true$ 为根，并以 $L_{1},\cdots ,L_{n}$ 为直接后继的树是 $S$ 的真值表，其中 $C=L_{1},\cdots ,L_{n}\in S$ （初始化规则）。
2. 令 $T$ 是 $S$ 的真值表，$B$ 是 $T$ 的一个分支，并且 $C=L_{1},\cdots ,L_{n}\in S$，使得链接条件（见下文）满足。如果树 $T'$ 是通过 $n$ 个子树 $L_{i}$ 扩展 $B$ 而构建的，那么 $T'$ 是 $S$ 的真值表（扩展规则）。

以下列出了三种可能的链接条件

1. 无条件。
2. 弱连接条件：存在一个字面量 $L\in B$ 以及 ${\overline {L}}\in C$.
3. 强连接条件：令 $L$ 为 $B$ 的叶节点，则存在 ${\overline {L}}\in C$.

实际上我们已经定义了三种不同的演算

• 在没有连接条件的情况下，它被称为子句范式真值表。
• 在有弱连接条件的情况下，我们称之为连接演算，而
• 在有强连接条件的情况下，它被称为模型消去。

子句范式真值表的示例在图 3 中给出。连接演算真值表的示例是

最后，模型消去真值表由以下给出

定理 11

子句范式真值表是完备的。
注意强连接条件不允许合流

证明过程。如果没有连接条件（即空条件），那么很容易得到一个合流版本。对于弱连接条件的情况，这不是很明显。为了得到命题子句的判定过程，我们需要一个额外的条件

定义 16

子句集 $S$ 的真值表的分支 $B$ 被称为正则的，如果没有任何字面量出现超过一次。

定理 12

具有正则性和连接条件的子句范式真值表为命题逻辑提供了一个判定过程。

问题（诊断）

考虑这个有两个输入线和一个输出线的电子电路

假设，如所示，两条输入线都为“1”，而输出线为“1”，这与预期输出值“0”相矛盾。

1. 首先，对电路进行形式化，即对三个元件和两个连接的功能进行形式化，忽略元件无法正常工作的可能性（即不要使用abnormal -字面量）。
2. 考虑向输入线提供值对“0-0”、“1-0”和“1-1”。对于这些值对中的每一个，使用（1）中的结果，通过解析真值表计算预期的输出值。你如何从真值表中读出结果？
3. 使用你的形式化和解析真值表来证明输出值“1”在输入为“1-1”的情况下与预期行为相矛盾。你如何从真值表中读出结果？
4. 现在通过abnormal -字面量修改（1）中元件的形式化，如课堂上所示。使用解析真值表计算输入为“1-1”且输出为“1”的所有可能的诊断。你如何从真值表中读出结果？