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