归结方法可推广到谓词逻辑,困难在于出现了量词、变元,证明过程同命题逻辑,只不过每一步骤都要考虑到有变元,从而带来复杂性。
使用推理规则的推理演算过于灵活,技巧性强,而归结法较为机械,容易使用计算机来实现。
一、归结证明过程
1.为证明A→B是定理(A, B为谓词公式), 等价的是证明A∧
B = G是矛盾式, 这是归结法的出发点。
2.建立子句集S
。
3.对S作归结。
4.直至归结出空子句□, 证明结束。