归结方法可推广到谓词逻辑,困难在于出现了量词、变元,证明过程同命题逻辑,只不过每一步骤都要考虑到有变元,从而带来复杂性。
  使用推理规则的推理演算过于灵活,技巧性强,而归结法较为机械,容易使用计算机来实现。

一、归结证明过程

  1.为证明A→B是定理(A, B为谓词公式), 等价的是证明A∧B = G是矛盾式, 这是归结法的出发点。
  2.建立子句集S
  3.对S作归结。
  4.直至归结出空子句□, 证明结束。