谓词公式化为子句集
基本定义
谓词公式化为子句集的步骤
定理3.1
基本定义
原子谓词公式：一个不能够再分解的命题。
原子谓词公式及其否定统称为文字，P称为正文字#P称为负文字，P与#P为互补文字。
子句:任何文字的析取式，任何文字本身也都是子句。
子句集：由子句构成的集合。
空子句（NL)：不包含任何文字的子句。
由于空子句不包含任何文字，那么任何解释都不会使其为真，故说其永假。
谓词公式化为子句集的步骤
（1）消去谓词公式中的"->“和”<->"符号。
（2）把否定符号移到紧靠谓词的位置上
（3）变量标准化
约束变元改名
（4）消去存在量词
若出现在全称量词的辖域之外，则直接固化，如果在辖域内，那么转化为Skolem函数。Skolem函数是全程变量的函数。
（5）化为前束型
把所有的全称量词都移到公式的前面。
（6）化为Skolem标准型
（7）略去全称量词
（8）消去合取词，把母式用子集表示
用逗号代替合取词。
（9）子句变量标准化
子句集中的一个字句的变元要改为不同的名字
定理3.1