前束范式谓词推理.pptVIP

前束范式 Logic 一阶逻辑 谓词公式的标准化形式: 前束范式 prenex normal form(PNF 前束合取范式 前束析取范式 2019/1/15 discrete math  前束范式作用 Logic 一阶逻辑 在定理的机器证明中,需要消除谓词公式 中的量词,因而需要将谓词公式中的量词前束 化,即把公式中的量词均提取到公式的前部。 即前束范式主要是对量词的位置有要求,而对 联接词无要求,这一点与命题逻辑不同。 2019/1/15 discrete math  Logic 前束范式 阶逻辑 定义:一个谓词公式,如果它的所有量词均 非否定地出现在公式的最前面,且它的辖域作 用于整个公式,则称为此为前束范式( prenex normal forms)。即前束范式形如 (Q1x1)(Qx2)、(Qkxk)B 其中Q(1s)为V或彐,x1为客体变元。B为 不含有量词的公式。 2019/1/15 discrete math  Logic 前束范式例子 一阶逻辑 前束范式的特点是,所有量词均非否定地 出现在公式最前面,且它的辖域一直延伸 到公式之末。 例如,xyvz(P(x2y)-Q(y,z))→R(xy)) 是前束范式。 而∨xP(x)AyQ(y),Vx(P(x)-yQ(x,y) 不是前束范式 2019/1/15 discrete math  Logic 量词移前的步骤 阶逻辑 前束范式存在定理::谓词逻辑中任意公式A 都有与之等价的前束范式。 转化方法: 把条件或双条件联结词转化 2、利用量词否定等价公式,把否定深入到命题 变元和谓词公式的前面。 3、换名。 4、利用量词作用域的扩张和收缩等价式,把量 词提到前面。 2019/1/15 discrete math  前束范式例子 Logic 一阶逻辑 求下面公式的前束范式: (1)yxF(x)∧1xG(x) (2)VXF(X)V1ExG(x) 2019/1/15 discrete math  求解前束范式例子(1) Logic 一阶逻辑 解(1)xF(x)∧彐xG(x) 台xF(x)∧η彐yG(y)(换名规则) 台VxF(x)∧Vy1G(y)(量词否定) 台x(F(x)∧∨y1G(y)(辖域扩张) 分xvy(F(x)∧-G(y)(辖域扩张) 或者 VxF(x)∧彐xG(x) 台VxF(x)∧Vx1G(x)(量词否定) 台Vx(F(x)∧ηG(x))(量词分配) 由此可知,(1)中公式的前束范式是不唯一的。 2019/1/15 discrete math  求解前束范式例子(2) Logic 一阶逻辑 2)yxF(x)V1彐xG(x) 令xF(x) VVX7 G(X)(量词否定) 令xF(x)VyGy)(换名规则) 令vx(F(x)√yG(y)(辖域扩张) 令→vxy(F(x)∨G(y)(辖域扩张) 问:(2)的下述求法是否正确? vxF(x)V玉xG(x) →VxF(x)∨xG(x) x(F(x)V1G(x)错 2019/1/15 discrete math  Logic 一阶逻辑 2019/1/15 discrete math  Logic 前束范式例子 一阶逻辑 例:求以下式的前束范式: (1)VxA(x)→丑xB(x) (2)VxA(x)∨xB(x) (3)xyy(z(P(xz)∧P(y)→zQxX,y,z) 解(1)xA(x)→彐xB(x)台彐X(A(x)→B(x) 即为所求前束范式。 或xA(x)→丑xB(x)xA(x)V彐xB(x) xA(xV彐xB(x) 冷丑(A(x)VB(x) 即为所求前束范式 2019/1/15 discrete math