|
2.4 归结原理
虽然Herbrand 定理给出了推理算法，但这种方法需逐次生成基例集S0',S1', …再检验Si'的不可满足性，这常常是难以实现的。
 |
例: |
| S＝{P(x,g(x),y,h(x,y),z,k(x,y,z)),～P(u,v,e(v),w,f(v,w),x)} 有H0＝{a} S0'＝{P(a,g(a),a,h(a,a),a,k(a,a,a)),～P(a,a,e(a),a,f(a,a),a)} H1={a,g(a),h(a,a),k(a,a,a),e(a),f(a,a)}共含6个元素。 S1'：对S中文字P的变量x,y,z均可取值于H1的6个元素，从而对文字P可构成63种可能的形式。对文字～P的变量u,v,w,x也可取值于H1的6个元素。从而对文字～P可构成64种可能的形式。故S 有63+64=1512个元素。而S0'， S1'是可满足的基例集，必需建立S2'。由于变量最多的函数是k(x,y,z),三个变量都可取值于H1的6个元素，于是 H2：元素个数有63数量级 S2'：元素个数有(63)4数量级 由于S 是可满足的基例集，还要继续这个过程，建立S3',S4',直到S5'才是不可满足。然而S5'元素个数已达(1064)4＝10256的数量级上，这是当今计算机无法处理的。 |
这样简单的例子，直接使用Herbrand 定理都是不能处理的。也就是说Herbrand定理所给的算法尚不能直接应用。
1965年 Robinson 提出了归结原理，是对自动推理的重大突破。例如上面给出的例子，使用归结方法，只需做一次归结便可证明S是不可满足的。谓词逻辑下的归结方法比命题逻辑要复杂多，主要是需处理变量，为此尚要引入置换与合一概念后才能介绍归结法。