一阶逻辑的归结

在命题逻辑中,每个逻辑公式都可以等价于一个析取或合取范式。

斯科伦(Skolem)定理: 在一阶逻辑中,给定任意一个逻辑公式$A$$A$, 都存在一个子句标准形式$A^{{}^{\prime }}$$A^{'}$与$A$$A$是等可满足性的, 即: $A\approx A^{{}^{\prime }}$$A{\approx}A^{'}$.

将一阶逻辑公式转化为子句标准形的方法是:

1.将一阶逻辑公式转化为前束范式。

2A.如果存在量词不出现在全称量词的辖域内, 用一个个体常量替换该存在量词约束的变量。

2B.如果存在量词出现在全称量词的辖域内, 用一个斯科伦函数替换该存在量词约束的变量。

对于$\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\cdots \mathrm{\forall }{x}_k\mathrm{\exists }yB(x_1,x_2,\cdots ,x_k,y)$${\forall}x_{1}{\forall}x_{2}{\cdots}{\forall}x_k{\exists}yB(x_1,x_2,\cdots,x_k,y)$, 存在量词$y$$y$的斯科伦函数通常表示成: $y=f(x_1,x_2,\cdots ,x_k).$$y=f(x_1,x_2,\cdots,x_k).$

3.转化为斯科伦标准形:

$\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\cdots \mathrm{\forall }{x}_{k}C.$${\forall}x_{1}{\forall}x_{2}{\cdots}{\forall}x_kC.$

4.略去所有全称量词。

5.消去合取词, 将母式转化为子句标准形。

例: 求$\mathrm{\forall }x(p(x)\to q(x))\to (\mathrm{\forall }xp(x)\to \mathrm{\forall }xq(x))$$\forall x\, \left(p(x)\rightarrow q(x)\right) \rightarrow \left( \forall x\,p(x) \rightarrow \forall x\,q(x)\right)$的子句标准形。

解: $\mathrm{\forall }x(p(x)\to q(x))\to (\mathrm{\forall }xp(x)\to \mathrm{\forall }xq(x))$$\forall x\, \left(p(x)\rightarrow q(x)\right) \rightarrow \left( \forall x\,p(x) \rightarrow \forall x\,q(x)\right)$ $\mathrm{\forall }x(p(x)\to q(x))\to (\mathrm{\forall }yp(y)\to \mathrm{\forall }zq(z))$$\forall x\, \left(p(x)\rightarrow q(x)\right) \rightarrow \left( \forall y\,p(y) \rightarrow \forall z\,q(z)\right)$ $\mathrm{\neg }\mathrm{\forall }x(\mathrm{\neg }p(x)\vee q(x))\vee \mathrm{\neg }\mathrm{\forall }yp(y)\vee \mathrm{\forall }zq(z)$$\lnot \forall x\,\left( \lnot p(x) \lor q(x)\right) \lor \lnot \forall y\,p(y) \lor \forall z\,q(z)$ $\mathrm{\exists }x(p(x)\wedge \mathrm{\neg }q(x))\vee \mathrm{\exists }y\mathrm{\neg }p(y)\vee \mathrm{\forall }zq(z)$$\exists x\,\left( p(x) \land \lnot q(x) \right) \lor \exists y\, \lnot p(y) \lor \forall z\, q(z)$ $\mathrm{\exists }x\mathrm{\exists }y\mathrm{\forall }z(p(x)\vee \mathrm{\neg }p(y)\vee q(z))\wedge (\mathrm{\neg }q(x)\vee \mathrm{\neg }p(y)\vee q(z))$$\exists x\, \exists y\, \forall z\, \left( p(x) \lor \lnot p(y) \lor q(z) \right) \land \left( \lnot q(x) \lor \lnot p(y) \lor q(z) \right)$ $\mathrm{\forall }z(\boxed{{\displaystyle p(a)}}\vee \mathrm{\neg }\boxed{{\displaystyle p(b)}}\vee q(z))\wedge (\boxed{{\displaystyle \mathrm{\neg }q(a)}}\vee \boxed{{\displaystyle \mathrm{\neg }p(b)}}\vee q(z))$$\forall z\, \left( \boxed{p(a)} \lor \lnot \boxed{p(b)} \lor q(z) \right) \land \left( \boxed{{\lnot}q(a)} \lor \boxed{{\lnot}p(b)} \lor q(z) \right)$

于是, 可以得到子句标准形: $\{\{p(a),\mathrm{\neg }p(b),q(z)\},\{\mathrm{\neg }q(a),\mathrm{\neg }p(b),q(z)\}\}.$$\left\{ \left\{ p(a),\,\lnot p(b),\, q(z) \right\},\, \left\{ \lnot q(a),\, \lnot p(b),\, q(z) \right\} \right\}.$

例: 求$\mathrm{\exists }x\mathrm{\forall }yp(x,y)\to \mathrm{\forall }y\mathrm{\exists }xp(x,y)$$\exists x\, \forall y\, p(x,y) \rightarrow \forall y\, \exists x\, p(x,y)$的子句标准形。

解: $\mathrm{\exists }x\mathrm{\forall }yp(x,y)\to \mathrm{\forall }y\mathrm{\exists }xp(x,y)$$\exists x\, \forall y\, p(x,y) \rightarrow \forall y\, \exists x\, p(x,y)$ $\mathrm{\exists }x\mathrm{\forall }yp(x,y)\to \mathrm{\forall }w\mathrm{\exists }zp(z,w)$$\exists x\, \forall y\, p(x,y) \rightarrow \forall w\, \exists z\, p(z,w)$ $\mathrm{\neg }\mathrm{\exists }x\mathrm{\forall }yp(x,y)\vee \mathrm{\forall }w\mathrm{\exists }zp(z,w)$$\lnot \exists x\, \forall y\, p(x,y) \lor \forall w\, \exists z\, p(z,w)$ $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\neg }p(x,y)\vee \mathrm{\forall }w\mathrm{\exists }zp(z,w)$$\forall x\, \exists y\, \lnot p(x,y) \lor \forall w\, \exists z\, p(z,w)$ $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }w\mathrm{\exists }z(\mathrm{\neg }p(x,y)\vee p(z,w))$$\forall x\, \exists y\, \forall w\, \exists z\, \left( \lnot p(x,y) \lor p(z,w) \right)$ $\mathrm{\forall }x\mathrm{\forall }w(\mathrm{\neg }p(x,\boxed{{\displaystyle f(x)}})\vee p(\boxed{{\displaystyle g(x,w)}},w))$$\forall x\, \forall w\, \left( \lnot p\left(x,\boxed{f(x)}\right) \lor p\left(\boxed{g(x,w)},w\right) \right)$

于是, 可以得到子句标准形: $\{\{\mathrm{\neg }p(x,f(x)),p(g(x,w),w)\}\}.$$\{ \{ \lnot p\left(x,f(x)\right),\,p(g(x,w),w) \} \}.$

将命题逻辑中的归结方法直接应用到一阶逻辑中, 称为触底归结(Ground Resolution).

$Res(C_1,C_2)=(C_1-\{x\})\vee (C_2-\{\overline{x}\}).$$Res(C_1,C_2) = (C_1 - \{x\}) \lor (C_2 - \{\bar{x}\}).$

对于命题逻辑,输入: $\{pq,\overline{q}r\},$$\{pq,\bar{q}r\},$ 输出: $\{pr\}.$$\{pr\}.$

对于一阶逻辑, 输入: $\{\boxed{{\displaystyle q(f(b))}},r(a,f(b))\},\{p(a),\mathrm{\neg }\boxed{{\displaystyle q(f(b))}},s(f(a),b)\},$$\left\{\boxed{q\left(f(b)\right)},r\left(a,f(b)\right) \right\},\,\left\{ p(a),\lnot \boxed{q\left(f(b)\right)}, s\left(f(a),b\right) \right\},$ 输出: $\{p(a),r(a,f(b)),s(f(a),b)\}.$$\left\{ p(a),r\left(a,f(b)\right), s\left(f(a),b\right) \right\}.$

除了触底归结, 在一阶逻辑中还需要借助替换(Substitution)操作实现归结。

设: $E=\{p(x),q(f(y))\},$$E=\left\{ p(x), q\left( f(y) \right) \right\},$ $\theta$$\theta$是一个替换: $\theta =\{x\leftarrow y,y\leftarrow f(a)\},$$\theta = \left\{x \leftarrow y, y \leftarrow f(a) \right\},$ 则替换操作$E\theta$$E\theta$可通过同时替换所有相关变量得到: $E\theta =\{p(y),q\left(f(f(a))\right)\}$$E\theta = \left\{ p(y), q\left( f\left(f(a) \right) \right) \right\}$ 同时替换是必要的, 否则会得到以下错误的替换结果: $E\theta =\{p(y),q\left(f\left(y\right)\right)\}$$E\theta = \left\{ p(y), q\left( f\left(y \right) \right) \right\}$ $E\theta =\{p(f(a)),q\left(f(f(a))\right)\}$$E\theta = \left\{ p\left(f(a)\right), q\left( f\left(f(a) \right) \right) \right\}$ 多个替换可以组合。

若: $E=\{u,v,x,y,z\}$$E=\left\{ u, v, x, y, z \right\}$ $\theta =\{x\leftarrow f(y),y\leftarrow f(a),z\leftarrow u\}$$\theta = \left\{x \leftarrow f(y), y \leftarrow f(a), z \leftarrow u \right\}$ $\sigma =\{y\leftarrow g(a),u\leftarrow z,v\leftarrow f(f(a))\}$$\sigma = \left\{y \leftarrow g(a), u \leftarrow z, v \leftarrow f\left(f(a)\right) \right\}$ 则:

$\theta \sigma =\{x\leftarrow f(g(a)),y\leftarrow f(a),u\leftarrow z,v\leftarrow f(f(a))\}$$\theta \sigma = \left\{x \leftarrow f\left(g(a)\right), y \leftarrow f(a), u \leftarrow z, v \leftarrow f\left(f(a)\right) \right\}$ $E(\theta \sigma )=p(z,f(f(a)),f(g(a)),f(a),z)$$E(\theta \sigma) = p\left(z, f\left(f(a)\right), f\left(g(a)\right), f(a), z\right)$ $E\theta =p(u,v,f(y),f(a),z)$$E\theta = p\left(u, v, f(y), f(a), z\right)$ $(E\theta )\sigma =p(z,f(f(a)),f(g(a)),f(a),z)$$(E\theta) \sigma = p\left(z, f\left(f(a)\right), f\left(g(a)\right), f(a), z\right)$

因此:

$E(\theta \sigma )=(E\theta )\sigma$$E(\theta \sigma) = (E\theta) \sigma$

尽管两个文字: $p(f(x),g(y))$$p\left(f(x),g(y)\right)$ 和 $\mathrm{\neg }p(f(f(a)),g(z))$$\lnot p\left(f\left(f(a)\right),g(z)\right)$ 不具备触底归结的条件, 但是通过替换: ${\theta }_1=\{x\leftarrow f(a),y\leftarrow f(g(a)),z\leftarrow f(g(a))\}$$\theta_1 = \left\{x \leftarrow f(a), y \leftarrow f\left(g(a)\right), z \leftarrow f\left(g(a)\right) \right\}$ 可将原文字转换为: $\begin{array}{c}p(f(f(a)),g\left(f(g(a))\right))\\ \mathrm{\neg }p(f(f(a)),g\left(f(g(a))\right)).\end{array}$$\begin{array}{c} p\left(f\left(f(a)\right),g\left(f\left(g(a)\right)\right)\right)\\ \lnot p\left(f\left(f(a)\right),g\left(f\left(g(a)\right)\right)\right). \end{array}$ 从而可以实现归结。 这个做法称为合一(Unification).

在合一操作中, 替换并不唯一。

例如: $\begin{array}{c}{\theta }_2=\{x\leftarrow f(a),y\leftarrow a,z\leftarrow a\}\end{array}$$\begin{array}{c} \theta_2 = \left\{x \leftarrow f(a), y \leftarrow a, z \leftarrow a \right\} \end{array}$ 的替换结果是: $p(f(f(a)),g(a)),\mathrm{\neg }p(f(f(a)),g(a))$$p\left(f\left(f(a)\right),g(a)\right),\,\, \lnot p\left(f\left(f(a)\right),g(a)\right)$ 或者 $\begin{array}{c}{\theta }_3=\{x\leftarrow f(a),z\leftarrow y\}\end{array}$$\begin{array}{c} \theta_3 = \left\{x \leftarrow f(a), z \leftarrow y \right\} \end{array}$ 替换结果是: $p(f(f(a)),g(y)),\mathrm{\neg }p(f(f(a)),g(y)).$$p\left(f\left(f(a)\right),g(y)\right),\,\, \lnot p\left(f\left(f(a)\right),g(y)\right).$ 其中, ${\theta }_3$$\theta_3$称为公式$E$$E$的最广合一子(Most General Unifier, MGU).

其它替换建立在最广合一子基础之上, 如: $\begin{array}{l}{\theta }_2={\theta }_3{\lambda }_1,{\lambda }_1=\{y\leftarrow a\}\\ {\theta }_1={\theta }_3{\lambda }_2,{\lambda }_2=\{y\leftarrow f(g(a))\}\end{array}$$\begin{array}{l} \theta_2 = \theta_3 \lambda_1, \qquad \lambda_1=\left\{y \leftarrow a\right\}\\ \theta_1 = \theta_3 \lambda_2, \qquad \lambda_2=\left\{y \leftarrow f\left(g(a)\right)\right\} \end{array}$​

例: 已知子句标准形为 $\{p(f(x),g(y)),q(x,y)\},\{\mathrm{\neg }p(f(f(a)),g(z)),q(f(a),z)\}$$\{p(f(x),g(y)), q(x,y)\}, \{{\lnot}p(f(f(a)),g(z)), q(f(a),z)\}$ 针对$L_1=p(f(x),g(y))$$L_1=p(f(x),g(y))$和$L_2^c=p(f(f(a)),g(z))$$L_2^c=p(f(f(a)),g(z))$两个文字, 可通过最广合一子: $\{x\leftarrow f(a),y\leftarrow z\}$$\{x{\leftarrow}f(a),y{\leftarrow}z\}$ 将子句标准形归结为: $\{q(f(a),z),q(f(a),z)\}$$\{q(f(a),z), q(f(a),z)\}$ 或 $\{q(f(a),z)\}.$$\{q(f(a),z)\}.$