計算機科學家邏輯/謂詞邏輯/等價和正規化

等價和正規化

公式的等價定義與命題情況相同

定義 6

公式 $F$ 和 $G$ 稱為（語義）等價，如果對於 $F$ 和 $G$ 的所有解釋 ${\mathcal {I}}$ ， ${\mathcal {I}}(F)={\mathcal {I}}(G)$ 。我們寫 $F\equiv G$ 。

命題情況下的等價關係在定理4中成立，此外對於量詞我們還有以下情況。

定理 1

以下等價關係成立

$\lnot \forall xF$ $\equiv$ $\exists x\lnot F$

$\lnot \exists xF$ $\equiv$ $\forall x\lnot F$

如果 $x$ 在 $G$ 中不作為自由變量出現

$\forall xF\land G$ $\equiv$ $\forall x(F\land G)$

$\forall xF\lor G$ $\equiv$ $\forall x(F\lor G)$

$\exists xF\land G$ $\equiv$ $\exists x(F\land G)$

$\exists xF\lor G$ $\equiv$ $\exists x(F\lor G)$

$\forall xF\land \forall xG$ $\equiv$ $\forall x(F\land G)$

$\exists xF\lor \exists xG$ $\equiv$ $\exists x(F\lor G)$

$\forall x\forall y\;F$ $\equiv$ $\forall y\forall xF$

$\exists x\exists y\;F$ $\equiv$ $\exists y\exists xF$

證明： 我們只證明等價關係

\forall xF\land G\equiv \forall x(F\land G)

其中 $x$ 在 $G$ 中沒有自由出現，例如。假設一個解釋 ${\mathcal {I}}=(U,{\mathcal {A}})$ 使得

{\mathcal {I}}(\forall xF\land G)=true

{\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true

{\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true

{\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}_{[x/d]}(G)=true{\text{ (x = does not occur free in = G)}}

{\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true

{\text{iff }}{\mathcal {I}}(\forall x(F\land G))=true.

請注意，以下對稱情況不成立

$\forall xF\lor \forall xG$ 與 $\forall x(F\lor G)$ 不等價

$\exists xF\land \exists xG$ 與 $\exists x(F\land G)$ 不等價

替代性定理與命題情況一樣成立。

**示例：**讓我們使用替代性和定理 1 中的等價關係來轉換以下公式

(\lnot (\exists xP(x,y)\lor \forall zQ(z))\land \exists wP(f(a,w)))

\equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))

\equiv ((\forall x\lnot P(x,y)\land \exists z\lnot Q(z))\land \exists wP(f(a,w)))

\equiv (\exists wP(f(a,w))\land (\forall x\lnot P(x,y)\land \exists z\lnot Q(z)))

\equiv \exists w(P(f(a,w))\land \forall x(\lnot P(x,y)\land \exists z\lnot Q(z)))

\equiv \exists w(\forall x(\exists z\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))

\equiv \exists w(\forall x\exists z(\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))

\equiv \exists w\forall x\exists z((\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))

定義 7

令 $F$ 為一個公式， $x$ 為一個變數， $t$ 為一個項。 $F[x/t]$ 是從 $F$ 透過將 $x$ 的所有自由出現替換為 $t$ 而獲得的。
注意，這個概念可以重複使用： $F[x/t_{1}][y/t_{2}]$ 以及 $t_{1}$ 可能包含 $y$ 的自由出現。

引理 1

令 $F$ 為一個公式， $x$ 為一個變數， $t$ 為一個項。

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

引理 2 (受限重新命名)

令 $F=QxG$ 為一個公式，其中 $Q\in \{\forall ,\exists \}$ 且 $y$ 為一個不在 $G$ 中出現的變數，則 $F\equiv QyG[x/y]$

定義 8

如果一個公式中沒有變數同時出現於約束和自由狀態，並且每個量詞之後都是一個不同的變數，則稱該公式為 proper 公式。

引理 3 (proper 公式)

對於每個公式 $F$ ，都存在一個公式 $G$ ，該公式為 proper 公式，並且與 $F$ 等價。
證明： 由受限重新命名直接得出。
例子

F=\forall x\exists y\;p(x,f(y))\land \forall x(q(x,y)\lor r(x))

有等價的 proper 公式

G=\forall x\exists y\;(p(x,f(y)))\land \forall z(q(z,u)\lor r(z)

定義 9

如果公式具有形式 $Q_{1}\cdots Q_{n}F$ ，其中 $Q_{i}\in \{\forall ,\exists \}$ ，並且在 $F$ 中沒有出現量詞，那麼該公式稱為前束正規化。

定理 2

對於每一個公式，都存在一個等價的前束正規化。
例子

$\forall x\exists y\;(p(x,g(y,f(x)))\lor \lnot q(z))\lor \lnot \forall x\;r(x,z)$

$\forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists x\;\lnot r(x,z)$

$\forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists v\lnot r(v,z)$

$\forall x\exists y\exists v\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \lnot r(v,z)$

證明：透過對公式結構進行歸納，我們可以直接得到原子公式的定理。

$F=\lnot F_{0}$ ：存在一個 $G_{0}=Q_{1}y_{1}\cdots Q_{n}y_{n}G'$ ，其中 $Q_{i}\in \{\forall ,\exists \}$ ，等價於 $F_{0}$ 。因此我們有

$F\equiv {\overline {Q_{1}}}y_{1}\cdots {\overline {Q_{n}}}y_{n}\lnot G'$

其中 ${\overline {Q_{i}}}={\begin{cases}\;\;\,\exists &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{i}=\exists \end{cases}}$

$F=F_{1}\circ F_{2}$ 其中 $\circ \in \{\land ,\lor \}$ 。存在 $G_{1},G_{2}$ 是正確的預nex 正規化，並且 $G_{1}\equiv F_{1}$ 以及 $G_{2}\equiv F_{2}$ 。透過有界重新命名我們可以構造

G_{1}=Q_{1}y_{1}\cdots Q_{k}y_{k}G_{1}'

G_{2}=Q_{1}'z_{1}\cdots Q_{l}'z_{l}G_{2}'

其中 $\{y_{1},\cdots ,y_{n}\}\cap \{z_{1},\cdots ,z_{l}\}=\emptyset$ ，因此

F\equiv Q_{1}y_{1}\cdots Q_{k}y_{k}Q_{1}'z_{1}\cdots Q_{l}'z_{l}(G_{1}'\circ G_{2}')

在下文中，我們將正確的預nex 正規化公式稱為 PP-公式或 PPF。

定義 10

令 $F$ 為一個 PPF。當 $F$ 包含一個 $\exists$ -量詞時，進行以下變換

$F$ 有如下形式

\forall y_{1},\cdots \forall y_{n}\exists z\;G

其中 $G$ 是一個 PPF，而 $f$ 是一個 $n$ -元函式符號，它在 $G$ 中不出現。

令 $F$ 為

\forall y_{1},\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})]

如果不存在更多 $\exists$ -量詞，那麼 $F$ 處於 Skolem 標準型。

定理 3

令 $F$ 是一個 PPF。 $F$ 是可滿足的當且僅當 $F$ 的 Skolem 標準型是可滿足的。

證明：令 $F=\forall y_{1}\cdots \forall y_{n}\exists z\;G$ ；經過一次按照 while 迴圈的轉換後，我們得到

F'=\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})

其中 $f$ 是一個新的函式符號。我們需要證明這種變換是可滿足性保持的：假設 $F'$ 是可滿足的。那麼存在一個模型 ${\mathcal {I}}$ 對於 $F'$ ${\mathcal {I}}$ 是 $F$ 的一個解釋。根據模型性質，我們有對於所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f(y_{1},\cdots ,y_{n})])=true

根據引理1，我們可以得出結論

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true

其中 $v={\mathcal {I}}(f(u_{1},\cdots ,u_{n})$ 。因此，我們有，對於所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$ ，存在一個 $v\in U_{\mathcal {I}}$ ，其中

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true

因此，我們有 ${\mathcal {I}}(\forall y_{1}\cdots \forall y_{n}\exists z\;G)=true$ ，這意味著 ${\mathcal {I}}$ 是 $F$ 的一個模型。

對於定理的反方向，假設 $F$ 有一個模型 ${\mathcal {I}}$ 。那麼我們有，對於所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$ ，存在一個 $v\in U_{\mathcal {I}}$ ，其中

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true

令 ${\mathcal {I'}}$ 是一個解釋，它只在函式符號 $f$ 上與 ${\mathcal {I}}$ 不同，其中 ${\mathcal {I}}$ 沒有定義。我們假設 $f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})=v$ ，其中 $v$ 是根據上述等式選擇的。

因此，我們有對於所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}'$

{\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})]}(G)=true

根據引理 1，我們得出結論，對於所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$

{\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f^{(}y_{1},\cdots ,y_{n})])=true

這意味著 ${\mathcal {I}}'(\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})])=true$ ，因此 ${\mathcal {I}}'$ 是 $F'$ 的模型。

以上結果可用於將一個公式轉換為一組子句，即它的子句正規化。

轉換為子句正規化

給定一個一階邏輯公式 $F$ 。

將 $F$ 轉換為等價的適當 $F_{1}$ ，透過有界重新命名。
令 $y_{1},\cdots ,y_{k}$ 是 $F_{1}$ 中的自由變數。將 $F_{1}$ 轉換為 $F_{2}=\exists y_{1}\cdots \exists y_{k}\;F_{1}$
將 $F_{2}$ 轉換為等價的前束正規化 $F_{3}$ 。
將 $F_{3}$ 轉換為它的斯科倫正規化 $F_{4}=\forall x_{1}\cdots \forall x_{l}\;G$
將 $G$ 轉換為其 CNF $G\prime =(\bigwedge _{i=1}^{n}~(\bigvee _{j=1}^{m}~L_{i,j}))$ ，其中 $L_{ij}$ 是一個文字。這將導致 $F_{5}=\forall x_{1}\cdots \forall x_{l}\;G\prime$
將 $F_{5}$ 寫成一組子句。

F_{6}=\{C_{1},\cdots ,C_{n}\}

，其中

C_{i}=\{L_{i,1},\cdots ,L_{i,m}\}

問題

問題 6 (謂詞)

令 $F$ 為一個公式， $x$ 為一個變數， $t$ 為一個項。則 $F[x/t]$ 表示用 $t$ 替換 $F$ 中每個 $x$ 的自由出現而得到的公式。根據公式 $F$ 的結構，對這個三元函式 $F[x/t]$ 給出形式定義。

$\Box$

問題 7 (謂詞)

顯示以下語義等價性

$\forall x(p(x)\to (q(x)\land r(x)))\equiv \forall x(p(x)\to q(x))\land \forall x(p(x)\to r(x))$
$\forall x(p(x)\to (q(x)\lor r(x)))\not \equiv \forall x(p(x)\to q(x))\lor \forall x(p(x)\to r(x))$