定义

原子谓词公式：一个不能再分解的命题
如：花是红的、雪是白的

文字：原子谓词公式及其否定
P称为正文字，非P称为负文字，P和非P为互补文字

子句：任何文字的析取式称为子句，文字本身也是子句。
如：P或Q，P或(非Q)

空子句：不包含任何文字的子句，表示为NIL。
空子句是永假的，不可满足的

一般过程

1. 消去蕴含和等价

2. 移动否定符号

3. 变量标准化

4. 消去存在量词

5. 化为前束型

6. 化为Skolem标准型

7. 略去全称量词

8. 消去合取词，把母式用子句集表示

9. 子句变量标准化

不同的子句用不同的变元