Comp520MLCourse-6.4-PrenexCNF

前束范式

一个谓词公式, 如果它的所有量词均出现在公式的最前端, 而它们的作用域延伸到整个谓词公式的尾端, 则称该谓词公式为前束范式。

$Q_{1}x_{1}Q_{2}x_{2}{\cdots}Q_kx_kB$ $Q_{i}{\in}{{\forall},{\exists}}(1{\le}i{\le}k)$ $B$ 为不含量词的谓词公式。

$A$ $A$ ${\lnot}A(x){\vee}B(x)$ .

${\forall}x{\exists}y{\exists}z({\lnot}P(x){\rightarrow}(Q(y){\rightarrow}R(z,y)))$ ${\forall}x{\forall}y(S(x,w){\vee}T(y))$ $U(x,y)$ 是前束范式。

${\forall}xF(x,y){\rightarrow}{\exists}yG(y)$ ${\forall}x{\exists}zC(x,z){\wedge}V(z)$ 都不是前束范式。

前束范式存在定理: 任何谓词公式均存在其等价的前束范式。

化谓词公式为前束范式方法是:

1.将否定联结词向谓词公式内深入, 使之直接位于原子谓词公式之前。

2.利用换名规则和代入规则使所有约束变元符号均不相同, 自由变元与约束变元的符号也不相同。

3.利用等价式将量词逐个移至谓词公式的前端。

${\forall}xP(x){\rightarrow}{\exists}xQ(x)$ 转化为前束范式。

${\forall}xP(x){\rightarrow}{\exists}xQ(x)$ ${\Leftrightarrow}{\forall}xP(x){\rightarrow}{\exists}yQ(y)$ ${\Leftrightarrow}\lnot{\forall}xP(x){\vee}{\exists}yQ(y)$ ${\Leftrightarrow}{\exists}x({\lnot}P(x)){\vee}{\exists}yQ(y)$ ${\Leftrightarrow}{\exists}x({\lnot}P(x){\vee}{\exists}yQ(y))$ ${\Leftrightarrow}{\exists}x{\exists}y({\lnot}P(x){\vee}Q(y))$ ${\Leftrightarrow}{\exists}x{\exists}y(P(x){\rightarrow}Q(y))$

也可以这样转化:

${\forall}xP(x){\rightarrow}{\exists}xQ(x)$ ${\Leftrightarrow}{\lnot}{\forall}xP(x){\vee}{\exists}xQ(x)$ ${\Leftrightarrow}{\exists}x{\lnot}P(x){\vee}{\exists}xQ(x)$ ${\Leftrightarrow}{\exists}x({\lnot}P(x){\vee}Q(x))$

一阶逻辑公式的前束范式并不唯一。

${\lnot}({\forall}xP(x,y){\wedge}{\forall}xQ(x,z)){\rightarrow}{\exists}yR(y,x)$ ${\lnot}({\forall}xP(x,y){\wedge}{\forall}xQ(x,z)){\rightarrow}{\exists}yR(y,x)$ ${\Leftrightarrow}({\lnot}{\forall}xP(x,y){\vee}{\lnot}{\forall}xQ(x,z)){\rightarrow}{\exists}yR(y,x)$ ${\Leftrightarrow}({\exists}x{\lnot}P(x,y){\vee}{\exists}x{\lnot}Q(x,z)){\rightarrow}{\exists}yR(y,x)$ ${\Leftrightarrow}{\exists}x({\lnot}P(x,y){\vee}{\lnot}Q(x,z)){\rightarrow}{\exists}yR(y,x)$ ${\Leftrightarrow}{\exists}u({\lnot}P(u,y){\vee}{\lnot}Q(u,z)){\rightarrow}{\exists}vR(v,x)$ ${\Leftrightarrow}{\exists}u(({\lnot}P(u,y){\vee}{\lnot}Q(u,z)){\rightarrow}{\exists}vR(v,x))$ ${\Leftrightarrow}{\forall}u{\exists}v(({\lnot}P(u,y){\vee}{\lnot}Q(u,z)){\rightarrow}R(v,x))$

一个前束范式,若其不含量词的部分为析取范式, 称为前束析取范式; 若其不含量词的部分为合取范式, 称为前束合取范式。

${\forall}x{\exists}y(P(x,y){\wedge}Q(x))$ 是前束合取范式。

${\forall}x{\exists}y{\exists}z((R(x,y,z){\wedge}S(x)){\vee}Q(x))$ 是前束析取范式。

定理: 任何谓词公式均可化为与其等价的前束析取范式或前束合取范式。

将一阶逻辑公式转化为前束析取范式或前束合取范式的方法是:

${\lnot}$ ${\wedge}$ ${\vee}$ .

2.将公式化为前束范式。

3.利用分配律将公式进一步转化为前束析取范式或前束合取范式。

${\forall}x(F(x){\vee}H(y)){\rightarrow}{\forall}yG(x,y)$ 的前束合取范式。

${\forall}x(F(x){\vee}H(y)){\rightarrow}{\forall}yG(x,y)$ ${\Leftrightarrow}{\lnot}{\forall}x(F(x){\vee}H(y)){\vee}{\forall}yG(x,y)$ ${\Leftrightarrow}{\exists}x{\lnot}(F(x){\vee}H(y)){\vee}{\forall}yG(x,y)$ ${\Leftrightarrow}{\exists}v{\lnot}(F(v){\vee}H(y)){\vee}{\forall}wG(x,w)$ ${\Leftrightarrow}{\exists}v({\lnot}(F(v){\vee}H(y)){\vee}{\forall}wG(x,w))$ ${\Leftrightarrow}{\exists}v{\forall}w({\lnot}(F(v){\vee}H(y)){\vee}G(x,w))$ ${\Leftrightarrow}{\exists}v{\forall}w(({\lnot}F(v){\wedge}{\lnot}H(y)){\vee}G(x,w))$ ${\Leftrightarrow}{\exists}v{\forall}w({\lnot}F(v){\vee}G(x,w)){\wedge}({\lnot}H(y){\vee}G(x,w))$

${\forall}x{\exists}y(P(x,y){\wedge}Q(x)){\wedge}{\forall}x({\exists}zR(z,x){\rightarrow}S(w))$ 的前束析取范式。

${\forall}x{\exists}y(P(x,y){\wedge}Q(x)){\wedge}{\forall}x({\exists}zR(z,x){\rightarrow}S(w))$ ${\Leftrightarrow}{\forall}x{\exists}y(P(x,y){\wedge}Q(x)){\wedge}{\forall}x({\lnot}{\exists}zR(z,x){\vee}S(w))$ ${\Leftrightarrow}{\forall}x{\exists}y(P(x,y){\wedge}Q(x)){\wedge}{\forall}x({\forall}z{\lnot}R(z,x){\vee}S(w))$ ${\Leftrightarrow}{\forall}x({\exists}y(P(x,y){\wedge}Q(x)){\wedge}{\forall}z({\lnot}R(z,x){\vee}S(w)))$ ${\Leftrightarrow}{\forall}x{\exists}y((P(x,y){\wedge}Q(x)){\wedge}{\forall}z({\lnot}R(z,x){\vee}S(w)))$ ${\Leftrightarrow}{\forall}x{\exists}y{\forall}z((P(x,y){\wedge}Q(x)){\wedge}({\lnot}R(z,x){\vee}S(w)))$ ${\Leftrightarrow}{\forall}x{\exists}y{\forall}z((P(x,y){\wedge}Q(x){\wedge}{\lnot}R(z,x))$ ${\vee}(P(x,y){\wedge}Q(x){\wedge}S(w)))$

${\forall}x({\exists}y(A(x,y){\wedge}B(x)){\rightarrow}{\exists}zC(y,z))$ 的前束合取范式和前束析取范式。

${\forall}x({\exists}y(A(x,y){\wedge}B(x)){\rightarrow}{\exists}zC(y,z))$ ${\Leftrightarrow}{\forall}x({\lnot}{\exists}y(A(x,y){\wedge}B(x)){\vee}{\exists}zC(y,z))$ ${\Leftrightarrow}{\forall}x({\forall}y({\lnot}A(x,y){\vee}{\lnot}B(x)){\vee}{\exists}zC(y,z))$ ${\Leftrightarrow}{\forall}x({\forall}\boxed{w}({\lnot}A(x,\boxed{w}){\vee}{\lnot}B(x)){\vee}{\exists}zC(y,z))$ ${\Leftrightarrow}{\forall}x{\forall}w{\exists}z({\lnot}A(x,w){\vee}{\lnot}B(x){\vee}C(y,z))$