计算机科学家逻辑/谓词逻辑/求解策略/SLD-求解

选择性线性确定 (SLD) 求解

在本节中，我们将介绍一种针对 Horn 子句的线性求解特殊形式。我们将通过以下形式的符号来解释程序中的子句

{\begin{matrix}A&\gets &&&{\text{program clause (fact)}}\\A&\gets &B_{1},\ldots ,B_{n}&&{\text{ program clause }}\\&\gets &B_{1},\ldots ,B_{n}&&{\text{ goal }}\\\end{matrix}}

定义 27

设 $P$ 为一组程序子句。假设一个选择函数，对于给定的目标 $\gets A_{1},\ldots ,A_{n}$ ，可以从其子目标 $A_{i}$ 中选择一个。进一步假设一个目标 $G_{i}=\gets A_{1},\ldots ,A_{m},\ldots ,A_{n}$ 和一个选择函数，该函数选择 $A_{m}$ 。设 $C_{i}=A\gets B_{1},\ldots ,B_{q}$ 为 $P$ 中一个子句的变体，使得 $C_{i}$ 和 $G_{i}$ 没有共同的变量。如果 $\theta _{i+1}$ 是 $A_{m}$ 和 $A$ 的最一般统一，则目标

G_{i+1}=\gets (A_{1},\ldots ,A_{m-1},B_{1},\ldots ,B_{q},A_{m+1},\ldots ,A_{n})\theta _{i+1}

被称为 SLD-消解式

定义 28

对一组程序子句 $P$ 和一个目标子句 $G$ 的 $P\cup \{G\}$ 的 SLD-演绎（-反驳）是一个线性演绎（反驳），其中只出现 SLD-消解步骤，并且 $G$ 是起始子句。

一个 $R$ -计算的答案替换 $\theta$ 对于 $P\cup \{G\}$ 是 $\theta _{1}\circ \ldots \circ \theta _{n}|_{Var(G)}$ ，其中 $\theta _{1},\ldots ,\theta _{n}$ 是从 $P\cup \{G\}$ 的 SLD 证伪中获得的 mgU，选择函数为 $R$ 。
对于 $Var(G)$ 的替换 $\theta$ 是 $P\cup \{G\}$ 的答案替换。
如果 $P\models \forall G\theta$ ，则它对于 $P\cup \{G\}$ 是正确的答案替换。

定理 11

令 $P$ 是一个程序子句集， $G$ 是一个目标子句，而 $R$ 是一个选择函数。对于 $P\cup \{G\}$ 的每个正确答案替换 $\theta$ ，都存在一个 $R$ -计算的答案替换 $\sigma$ 对于 $P\cup \{G\}$ 以及一个替换 $\gamma$ ，使得 $\theta =\sigma \circ \gamma \;|_{Var(G)}$

在命题逻辑部分，我们已经解释了命题真值表及其变体，例如连接演算和模型消去。在本节中，我们将介绍一阶情况下的模型消去。请注意，在这种情况下，我们需要一个额外的推理规则，即归约规则。

定义 29

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

以 $true$ 为根， $L_{1},\cdots ,L_{n}$ 为其直接后继的树，其中 $C=L_{1},\cdots ,L_{n}$ 是来自 $S$ 的子句的新变体，是 $S$ 的真值表（初始化规则）。
令 $T$ 为 $S$ 的真值表， $B$ 是 $T$ 的一个分支， $C=L_{1},\cdots ,L_{n}$ 是来自 $S$ 的子句的新变体，使得链接条件满足 mgu $\sigma$ 。如果树 $T'$ 是通过用 $n$ 个子树 $L_{i}$ 扩展 $B$ 而构建的，那么 $T'\sigma$ 是 $S$ 的真值表（扩展规则）。
令 $T$ 为 $S$ 的一个 tableau， $B$ 是 $T$ 的一个分支， $L$ 是 $B$ 的一个叶节点，而 $L'\in C$ ，使得 ${\overline {L'}}$ 和 $L$ 具有一个 mgu $\sigma$ ，则 $T\sigma$ 是 $S$ 的一个 tableau（归约规则）。

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

无条件。
弱链接条件：存在文字 $L\in B$ 和 $L'\in C$ ，使得 ${\overline {L'}}$ 和 $L$ 具有一个 mgu $\sigma$
强链接条件：存在 $B$ 的一个叶节点 $L$ ，以及 $L'\in C$ ，使得 ${\overline {L'}}$ 和 $L$ 具有一个 mgu $\sigma$ 。

类似于命题情况，不同的链接条件会导致不同的演算。

空条件会导致一个子句范式 tableau 演算。

弱条件会导致一个连接演算。

强链接条件会导致一个模型消去演算。