2.4.3 归结过程
  谓词逻辑的归结过程与命题逻辑的归结过程相比,其基本步骤相同,但每步的处理对象不同。谓词逻辑需要把由谓词构成的公式集化为子句集,必要时在得到归结式前要进行置换和合一。
  ·具体的谓词逻辑归结过程如下:
  ·写出谓词关系公式
  ·用反演法写出谓词表达式
  ·化为SKOLEM标准形
  ·求取子句集S
  ·对S中可归结的子句做归结
  ·归结式仍放入S中,反复归结过程
  ·得到空子句
  ·命题得证