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