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。实用中可分别求出诸Ai 与
B的子句集。4．对S作归结。直至归结出空子句□。
