前束范式 定义设A为一个一阶逻辑公式,若A具有如下形式 Q1x1Q2x2…QB,则称4为前束范式,其中Q(1≤k) 为V或彐,B为不含量词的公式 例如,Vxy(F(x)-→>(G()∧H(xy) Vx-(F)AG(r) 是前束范式,而 Vx(F(x)→>彐y(G()∧H(xy)) x(F(x)∧G(x) 不是前束范式
6 前束范式 例如，xy(F(x)→(G(y)H(x,y))) x(F(x)G(x)) 是前束范式, 而 x(F(x)→y(G(y)H(x,y))) x(F(x)G(x)) 不是前束范式， 定义 设A为一个一阶逻辑公式, 若A具有如下形式 Q1 x1Q2 x2…Qk xkB, 则称A为前束范式, 其中Qi (1ik) 为或，B为不含量词的公式
公式的前束范式 定理(前束范式存在定理)一阶逻辑中的任何公 式都存在与之等值的前束范式 注意: 公式的前束范式不惟 求公式的前束范式的方法:利用重要等值式、 置换规则、换名规则、代替规则进行等值演算
7 公式的前束范式 定理（前束范式存在定理）一阶逻辑中的任何公 式都存在与之等值的前束范式 注意: 公式的前束范式不惟一 求公式的前束范式的方法: 利用重要等值式、 置换规则、换名规则、代替规则进行等值演算
换名规则与代替规则 换名规则:将量词辖域中出现的某个约束出现的 个体变项及对应的指导变项,改成另一个辖域中未 曾出现过的个体变项符号,公式中其余部分不变, 则所得公式与原来的公式等值 代替规则:对某自由出现的个体变项用与原公式 中所有个体变项符号不同的符号去代替,则所得公 式与原来的公式等值
8 换名规则与代替规则 换名规则: 将量词辖域中出现的某个约束出现的 个体变项及对应的指导变项，改成另一个辖域中未 曾出现过的个体变项符号，公式中其余部分不变， 则所得公式与原来的公式等值. 代替规则: 对某自由出现的个体变项用与原公式 中所有个体变项符号不同的符号去代替，则所得公 式与原来的公式等值
公式的前束范式(续) 例求下列公式的前束范式 (1)_3x(M(x)∧F(x) 解3x(M(x)F(x) 台x(M(x)-F(x)(量词否定等值式) Vx(M(x)→-F(x) 两步结果都是前束范式,说明前束范式不惟
9 公式的前束范式(续) 例 求下列公式的前束范式 (1) x(M(x)F(x)) 解 x(M(x)F(x)) x(M(x)F(x)) （量词否定等值式） x(M(x)→F(x)) 两步结果都是前束范式，说明前束范式不惟一