計算機科學家邏輯/謂詞邏輯/求解策略/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 演算。

弱條件會導致一個連線演算。

強連結條件會導致一個模型消去演算。