計算機科學家邏輯/謂詞邏輯/歸結

歸結

在命題情況下，我們透過“去除”兩個要進行歸結的子句中的一對互補文字來定義歸結推理規則。然而，在一階情況下，這並不總是足夠的。

${\begin{matrix}C_{1}:&p(x)\lor q(x)\\C_{2}:&\lnot p(f(x))\end{matrix}}$

在這兩個子句中，沒有互補文字，但是，在將項$f(a)$替換為變數$x$在$C_{1}$和將$a$替換為$x$在$C_{2}$後，我們得到

${\begin{matrix}C_{1}':&p(f(a))\lor q(f(a))\\C_{2}':&\lnot p(f(a))\end{matrix}}$

現在我們可以應用命題邏輯中的推理規則，並得到歸結式$q(f(a))$。

另一種可能性是將$f(x')$替換為$x$在$C_{1}$中，得到

$C_{1}'':p(f(x'))\lor q(f(x'))$

然後我們可以得到從$C_{1}''$和$C_{2}$的$q(f(x'))$ 解，從某種意義上說，它比之前推匯出的解更通用。

定義 18

替換$\sigma$是一個函式，它將變數對映到項，並且幾乎處處都是恆等對映。因此，它可以表示為

$\sigma =\{x_{1}/t_{1},\cdots ,x_{n}/t_{n}\}$

如果$t_{1},\cdots ,t_{n}$是基本項，我們稱$\sigma$為基本替換。空替換用$\epsilon$表示。

定義 19

令$\theta =\{x_{1}/t_{1},\cdots ,x_{n}/t_{n}\}$為一個替換，且$E$為一個表示式（即文字或項），則$E\theta$是從$E$中同時替換$E$中每個出現的$X_{i},1\leq i\leq n$得到的表示式，用項$t_{i}$替換。

示例

當$\theta =\{x/a,y/f(b),z/e\}$ 且 $E=p(x,y,z)$ 時，我們得到 $E\theta =p(a,f(b),c)$

定義 20

設 $\sigma =\{x_{1}/t_{1},\cdots ,x_{n}/t_{n}\}$ 和 $\lambda =\{y_{1}/s_{1},\cdots ,y_{m}/s_{m}\}$ 是兩個代換。則代換的複合，記為 $\sigma \circ \lambda$，是從 $\{x_{1}/t_{1}\lambda ,\cdots ,x_{n}/t_{n}\lambda ,y_{1}/s_{1},\cdots ,y_{m}/s_{m}\}$ 中刪除任何滿足 $t_{j}\lambda =x_{j}$ 的元素 $x_{j}/t_{j}\lambda$ 和任何滿足 $y_{i}\in \{x_{1},\cdots ,x_{n}\}$ 的元素 $y_{i}/s_{i}$ 所得到的代換。
示例

定義 21

設 $\{E_{1},\cdots ,E_{n}\}$ 是一個表示式集合，且 $\theta$ 是一個代換，$\theta$ 是 $\{E_{1},\cdots ,E_{n}\}$ 的一個統一化子，當且僅當

$E_{1}\theta =E_{2}\theta =\cdots E_{n}\theta$

.

一個統一代換 $\theta$ 被稱為最一般統一代換，當且僅當對於每個統一代換 $\sigma$，都存在一個替換 $\lambda$ 使得 $\sigma =\theta \circ \lambda$。

接下來，我們將討論一種計算最一般統一代換的演算法。為此，我們假設有一組要進行統一的項 $\{t_{1},\cdots ,t_{n}\}$。首先，我們透過引入一個尚未出現在此集合中的新變數，例如 $y$，並將此集合轉換為一組方程。

$N=\{y=t_{1},\cdots ,y=t_{n}\}$

我們現在將轉換此集合，使其統一代換保持不變，其中 $\sigma$ 是一組 $\{s_{1}=t_{1},\cdots ,s_{n}=t_{n}\}$ 的統一代換，如果 $\{s_{1}\sigma =t_{1}\sigma ,\cdots ,s_{n}\sigma =t_{n}\sigma \}$ 成立。

統一

給定一組表示式。將其轉換為一組如上定義的方程 $N$。儘可能地應用以下轉換規則

1. ${\frac {R\uplus \{t=x\}}{R\uplus \{x=t\}}}$ 方向化
   
   其中 $x$ 是一個變數，而 $t$ 是一個非變數項
   
   
2. ${\frac {R\uplus \{s=s\}}{R}}$ 刪除
   
   
   
3. ${\frac {R\uplus \{f(s_{1},\dots ,s_{n})=f(t_{1},\dots ,t_{n})\}}{R\uplus \{s_{1}=t_{1},\dots ,s_{n}=t_{n}\}}}$ 分解 (項約簡)
   
   
4. ${\frac {R\uplus \{x=t\}}{R[x/t]\uplus \{x=t\}}}$ 消去 (變數消去 I)
   
   如果 $x$ 不在 $t$ 中，但在 $R$ 中
   
   
5. ${\frac {R\uplus \{x=y\}}{R[x/y]\uplus \{x=y\}}}$ 合併 (變數消去 II)
   
   如果 $x\neq y$ 在 $R$ 中
   
   
6. ${\frac {R\uplus \{f(s_{1},\dots ,s_{m})=g(t_{1},\dots ,t_{n})\}}{\mbox{FAIL}}}$ 衝突
   
   如果 $f\neq g$ 或 $m\neq n$
   
   
7. ${\frac {R\uplus \{x=t\}}{\mbox{FAIL}}}$ 出現檢查
   
   如果 $x$ 在 $t$ 中
   

定理 7

設 $N$ 為一組表示式。上述統一演算法會終止。如果它返回 $FAIL$，則 $N$ 沒有統一式，否則 $N$ 會被轉換為一組方程 $\{y_{1}=u_{1},\cdots ,y_{m}=u_{m}\}$，它表示 $N$ 的最一般統一式。

定義 22

如果一個子句 $C$ 的兩個或多個文字具有一個統一式 $\sigma$，則 $C\sigma$ 稱為 $C$ 的一個因子。

示例

對於 $C=\{p(x),p(f(y)),\lnot q(x)\}$ 和 $\sigma =\{x/f(y)\}$，我們得到因子 $C\sigma =\{p(f(y)),\lnot q(f(y))\}$

定義 23

設$C_{1}$ 和 $C_{2}$ 是兩個沒有公共變數的子句，使得 $L_{1}\in C_{1}$ 且 $L_{2}\in C_{2}$，並且 $L_{1}$ 和 $L_{2}$ 有一個最一般合一化 $\sigma$。 $C_{1}$ 和 $C_{2}$ 的二元消解式是

$(C_{1}\sigma -L_{1}\sigma )\cup (C_{2}\sigma -L_{2}\sigma )$

示例：給定 $C_{1}=\{p(x),q(x)\}$ 和 $C_{2}=\{\lnot p(a),r(x)\}$。將 $C_{2}$ 重新命名為 $C_{2}=\{\lnot p(a),r(y)\}$，透過使用最一般合一化 $\{x/a\}$，得到消解式 $\{q(a),r(y)\}$。

我們通常以圖形方式描繪消解式，例如：

定義 24

兩個子句 $C_{1}$ 和 $C_{2}$ 的消解式是以下二元消解式之一

• $C_{1}$ 和 $C_{2}$ 的二元消解式
• $C_{1}$ 的二元消解式和 $C_{2}$ 的一個因子
• $C_{1}$ 的一個因子的二元消解式和 $C_{2}$
• $C_{1}$ 的一個因子的二元消解式和 $C_{2}$ 的一個因子的二元消解式

示例

給定 $C_{1}=\{p(x),p(f(y)),r(g(y))\}$ 和 $C_{2}=\{\lnot p(f(g(a))),q(b)\}$。

$C_{1}$ 的一個因子是 $C_{1}\prime =\{p(f(y)),r(g(y))\}$。 $C_{1}\prime$ 和 $C_{2}$ 的二元消解式，因此也是 $C_{1}$ 和 $C_{2}$ 的二元消解式是 $C_{3}=\{r(g(g(a))),q(b)\}$。

下面的引理用於消解完備性證明。

引理 5（提升引理）

如果$C'_{1}$ 和 $C'_{2}$ 分別是 $C_{1}$ 和 $C_{2}$ 的例項，並且 $C'$ 是 $C'_{1}$ 和 $C'_{2}$ 的一個解，那麼存在 $C_{1}$ 和 $C_{2}$ 的一個解 $C$，使得 $C'$ 是 $C$ 的一個例項。

圖 1

定理 8

一個子句集 $S$ 是不可滿足的，當且僅當空子句可以透過歸結原理從 $S$ 推匯出。
證明
假設 $S$ 是不可滿足的。令 $A=\{A_{1},A_{2},\ldots \}$ 為 $S$ 的基本原子集，因此是 Herbrand 基。令 $T$ 為一棵完整的二叉樹，如 圖 2 所示。根據 Herbrand 定理（版本 1），存在一棵封閉的有限語義樹 $T'$。有兩種情況

• 如果 $T'$ 只包含一個節點（因此是根節點），則從這棵樹的空分支收集的解釋只使空子句為假。因此，空子句必須在 $S$ 中。

• 假設$T'$包含多個節點。那麼，$T'$中一定存在一個推理節點$N$，因此它的兩個子節點$N_{1}$和$N_{2}$都是失敗節點。如果這樣的節點不存在，那麼每個節點都至少有一個非失敗節點，這意味著在$T'$中至少存在一條無限路徑，這將違反它是一個有限閉合語義樹的事實。設$N,N_{1},N_{2}$如上所述；並設${\begin{matrix}I(N)&=&\{m_{1},m_{2},\ldots ,m_{n}\}I(N_{1})&=&\{m_{1},m_{2},\ldots ,m_{n},m_{n},m_{n+1}\}I(N_{2})&=&\{m_{1},m_{2},\ldots ,m_{n},m_{n},\lnot m_{n+1}\}\end{matrix}}$

現在，令$C_{1}'$ 和 $C_{2}'$ 分別是子句 $C_{1}$ 和 $C_{2}$ 的基本例項，使得 $C_{1}'$ 被 $I(N_{1})$ 證偽，而 $C_{2}'$ 被 $I(N_{2})$ 證偽，使得兩者均不被 $I(N)$ 證偽。

因此，我們有 $\lnot m_{n+1}\in C_{1}'$ 和 $m_{n+1}\in C_{2}'$，並且我們可以構造歸結式

$C'=(C_{1}'-\{\lnot m_{n+1}\})\cup (C_{2}'-\{m_{n+1}\})$

$C'$ must be false in $I(N)$, because both $(C_{1}'-\lnot m_{n+1})$ and $(C_{2}'-m_{n+1})$ are false in $I(N)$. According to the Lifting Lemma 5 there exists a resolvent $C$ of $C_{1}$ and $C_{2}$, such that $C'$ is a ground instance of $C$. Let $T\;''$ be the closed semantic tree for $S\cup \{C\}$ , obtained from $T'$ by deleting all nodes below the first node which falsifies $C'$. Note, that $S$ is unsatisfiable if and only if $S\cup \{C\}$ is unsatisfiable. Clearly, $T\;''$ has less nodes than $T'$ and we now can iterate this process until only the root of the semantic tree is remaining. This, however is only possible if the empty clause $\square$ is derivable. For the opposite direction, assume that $\square$ is derivable by resolution from $S$ and let $R_{1},\ldots ,R_{k}$ the resolvents constructed during this process. Assume $S$ is satisfiable and $M$ to be a model for $S$. From the correctness lemma according to the propositional case we known, that if a model satisfies two clauses it also satisfies its resolvent. Therefore $M$ has to satisfy $R1,\ldots ,R_{k}$; this, however, is impossible, because one of this resolvents is $\square$.

圖 2

問題

問題 14（謂詞）

在每種情況下，用謂詞邏輯歸結法推匯出空子句！

1. $\{\{p(x,0,x)\},\{p(x,s(y),s(z)),\lnot p(x,y,z)\},\{\lnot p(s(s(s(0))),s(s(0)),u)\}\}$
2. $\{\{q(x),q(s(x))\},\{\lnot q(x),\lnot q(s(s(x)))\}\}$
   ($\star$)
3. $\{\{\lnot r(x,f(x),y),\lnot r(x,g(y),z)\},\{r(c,u,i(v)),r(h(u),v,j(v))\}\}$

$\Box$

問題 15（謂詞）

透過對項和公式構造的歸納，展示以下的提升引理：如果$F$ 是一個謂詞邏輯公式，並且${\mathcal {I}}$ 是一個適合$F$ 的解釋，

以及$F[x/t]$。那麼

${\mathcal {I}}(F[x/t])={\mathcal {I}}_{[x/{\mathcal {I}}(t)]}(F),$

是有效的，如果$t$ 不包含任何被$[x/t]$ 在$F$ 中的替換所繫結的變數。

透過替換繫結。
$\Box$

問題 16（謂詞）

計算 - 如果可能 - 以下子句集的最一般統一。

1. $\{p(x,a),p(f(c),y)\}$
2. $\{p(f(x),a,x),p(y,z,z)\}$
3. $\{q(x,x),q(g(y),y)\}$
4. $\{r(x,x),r(a,h(y))\}$

$\Box$

問題 17 (謂詞)

確定以下子句對的所有直接消解式

1. $\{\lnot p(x),q(x,b)\}$ 和 $\{p(a),q(a,b)\}$
2. $\{p(x),p(f(x))\}$ 和 $\{\lnot p(x),\lnot p(f(f(x)))\}$
3. $\{\lnot q(c,g(c))\}$ 和 $\{\lnot p(x),q(x,x)\}$
4. $\{\lnot p(x,y,z),\lnot p(y,u,v),\lnot p(x,v,w),p(z,u,w)\}$ 和 $\{p(g(x,y),x,y)\}$

$\Box$

問題 18 (謂詞)

計算 - 如果可能 - 以下子句集的最一般統一。

1. $\{o(x,x),o(a,f(y))\}$
2. $\{p(x,a),p(f(c),y)\}$
3. $\{q(g(x),a,x),q(y,z,z)\}$
4. $\{r(x,x),r(h(y),y)\}$

$\Box$

問題 19 (謂詞)

確定以下子句對的所有直接消解式

1. {¬p(x), ¬p(b), q(x,b)} 和 {p(a), q(a,b)}
2. {r(x), r(f(x))} 和 {¬r(x), ¬r(f(f(x)))}
3. {¬s(c,g(c))} 和 {s(x,x), ¬t(x)}

$\Box$

問題 20（謂詞邏輯）

對於以下子句集，給出（a）線性推導，（b）使用單元分解的推導，（c）透過謂詞邏輯分解獲得空子句的進一步（最短）推導！

{{¬e(x), o(s(x))}, {¬e(x), ¬o(s(x)), e(s(s(x)))}, {e(a)}, {¬o(s(s(s(s(s(a))))))}}

$\Box$

問題 21（謂詞邏輯）

在每種情況下，用謂詞邏輯歸結法推匯出空子句！

1. $\{\{p(x,0,x)\},\{p(x,s(y),s(z)),\lnot p(x,y,z)\},\{\lnot p(s(s(s(0))),s(s(0)),u)\}\}$
2. $\{\{q(x),q(s(x))\},\{\lnot q(x),\lnot q(s(s(x)))\}\}$
   ($\star$)
3. $\{\{\lnot r(x,f(x),y),\lnot r(x,g(y),z)\},\{r(c,u,i(v)),r(h(u),v,j(v))\}\}$

$\Box$