1.为证明A→B是定理(A, B为谓词公式), 等价的是证明A∧B = G是矛盾式, 这是归结法的出发点。

  2.建立子句集S。
  如何消去G中的量词, 特别是存在量词, 是建立子句集S的关键。
  办法是先将G化成等值的前束范式, 进而将这前束形化成SKOLEM标准形 (消去存在量词), 得仅含全称量词的公式G*, 曾指出G与G*在不可满足的意义下是一致的, 从而对G的不可满足性, 可由G*的不可满足性来求得。
  再将G*中的全称量词省略, G*母式(已合取范式化)中的合取词以∧","表示, 便得G的子句集S。而S与G是同时不可满足的,S中的变元视作有全称量词作用着。

  3.对S作归结。
  设C1、C2是两个无共同变元的子句, L1、L2分别是C1、C2中的文字, 如果L1和?L2有合一置换σ, 则
  (C1σ-{L1σ)∪(C2σ-{L2σ})
  称作子句C1, C2的归结式。
  如 C1 = P(x)∨Q(x)
  C2 = P(a)∨R(y)
  P(x)与P(a), 在合一置换{a/x}下将变元x换成a, 便为互补对可作归结了, 有归结式
  R(c1, c2) = Q(a)∨R(y)
  对子句集S的任两子句作归结(如果可作归结)。并将归结式仍放入S中。重复这过程。

  4.直至归结出空子句□, 证明结束。

  谓词逻辑的归结推理法。
  出发点:使用推理规则,技巧性较强,不便于机器实现。
  归结推理法步骤:
  1.证 A1∧A2∧…∧An →B 是定理,等价于证 G = A1∧A2∧…∧An∧┓B 是矛盾式。
  2.Skolem 化,将G化为前束范式。消去存在量词,得到仅含全称量词的前束范式G*(由于全称量词的前束范式保持不可满足的特性,故G与G*在不可满足的意义下是一致的)。
  3.略去全称量词,得到G*的子句集S。实用中可分别求出诸AiB的子句集。
  4.对S作归结。直至归结出空子句□。