下面继续学习消解原理
简化的做法是：若α=α1∧α2，先将α1、α2分别化成前束范式，然后对α1、α2分别求出斯柯伦范式ß1、ß2，最后将ß1∧ß2的量词左移得到α的斯柯伦范式（即前束范式）。
例3.8 求斯柯伦范式。
①
x
yzuvwA（x，y，z，u，v，w）
（用a替代x，删除x）
=yzuvwA（a，y，z，u，v，w）
（用f（y，z）代替u，删除u）
=yzvwA（a，y，z，f（y，z），v，w）
（用h（y，z，v）代替w，删除w）
=yzvA（a，y，z，f（y，z），v，h（y，z，v））
②α=y1x1P（x1，y1）∧x2y2Q（x2，y2）
=x1P（x1，a1）∧x2Q（x2，f（x2） ）
（先分别化成斯科伦范式）
=x1x2（P（x1，a1）∧Q（x2，f（x2）））
（前束合取范式）
4．子句集
原子公式的定义：不能再分解的谓词公式。具体定义为：
①原子命题是原子公式。
②如果t1，…，tn（n≥1）是项，P是谓词，则P（t1，…，tn）是原子公式。
③其它表达式都不是原子公式。
一个原子公式和原子公式的否定。P称为正文字，～P称为负文字，P与～P称为互补文字（互补对）。
子句：由文字的析取组成的公式。不包含任何文字的子句，表示为NIL。空子句是永假的（不可满足的）。
子句集是由子句构成的集合。
二、求取子句集的步骤
求取子句集的步骤包括以下9步：
1．消去“蕴含”连结词。
2．减少“非”连结词的辖域（将“～”连结词直接作用到原子公式前）。
3．对变量标准化（约束变元改名）。
4．消去存在量词（引入斯科伦函数）。
5．化成前束范式。
6．将母式化成合取范式。
7．消去全称量词。
8．消去合取连结词。
9．更改变量名，得到子句集。
下面分别对这9个步骤进行介绍。
1．消去“蕴含”连结词
使用的公式：
A<=>B=（A=>B）∧（B=>A）
A=>B=～A∨B
2．减少“非”连结词的辖域
将“～”连结词直接作用到原子公式前，使得每一个“非”联结词最多只能作用于一个原子公式（谓词符号）。
使用的公式是：
～（～A）＝A
～（A∨B）=～A∧～B
～（A∧B）=～A∨～B
～（x）A（x）=（x）（～A（x））
～（x）A（x）=（x）（～A（x））
到现在为止，谓词公式只包含三种连结词：“合取”∧、“析取”∨和“非”～
3．对变量标准化
对约束变元改名，使得所有的约束变元名都不相同，保证每一个量词都有自己唯一的约束变元。
4．消去存在量词
消去存在量词的规则：
①以一个斯科伦函数代替每一个带存在量词的约束变元，斯科伦函数的变元是（左边）带全称量词的约束变元，而且这些全称量词的辖域必须包括被消去的存在量词的辖域。
②如果要消去的存在量词不在任何一个全称量词的辖域内，则用常量来代替。
斯科伦函数和常量的符号必须是未在谓词公式出现过的。
例如，如下面谓词公式α引入斯科伦函数，消去存在量词，需要注意的是x1的辖域不包含y2的辖域。
α=y1x1P（x1，y1）∧x2y2Q（x2，y2）
变换后
α=x1P（x1，a1）∧x2Q（x2，f（x2））
5．化成前束范式
将全称量词移到谓词公式的左边，使得每一个量词的辖域包括该量词后面的整个谓词公式。举例如下:
（θx）A（x）∨R=（θx）（A（x）∨R）
（θx）A（x）∧R=（θx）（A（x）∧R）
（θ1x）A（x）∨（θ2z）B（z）=（θ1x）（θ2z）（A（x）∨B（z））
（θ1x）A（x）∧（θ2z）B（z）=（θ1x）（θ2z）（A（x）∧B（z））
需要说明的是A（x），B（z），R中允许含有与x，z不同的自由变量
