2.3 谓词逻辑归结法基础
由于谓词逻辑与命题逻辑不同，有量词、变量和函数，所以在生成子句集之前要对逻辑公式做处理，具体的说就是要将其转化为Skolem标准形，然后在子句集的基础上再进行归结，虽然基本的归结的基本方法都相同，但是其过程较之命题公式的归结过程要复杂得多。
本节针对谓词逻辑归结法介绍了Skolem标准形、子句集等一些必要的概念和定理。
2．3．1 Skolem 标准形