|
【章节小结】
命题逻辑归结就是
从G=A1∧A2∧A3∧～B出发,利用归结推理规则寻找矛盾,从而证明定理A1∧A2∧A3∧→B成立。命题逻辑归结过程
1. 将证明A B化成G=A∧～B的不可满足的证明
2. 将G化成合取范式
3. 建立子句集
4. 使用归结法并把归结式送入到S中，直到得到空子句 ，定理得证。
空子句□是P,～P的归结结果，或说含有矛盾，这表明S是不可满足的，从而定理得证。
谓词逻辑的归结法，要比命题逻辑复杂的多。原因是出现了变量和量词。如何建立G=A∧～B的子句形S，办法是消去存在量词，保留全称量词，得到SKOLEM标准形。进而得到G的子句形S。要注意的是G的子句形S与G并不等价,但他们在不可满足意义下是一致的。一阶谓词逻辑归结过程
1．将A B的证明化成G=A∧～B的不可满足的证明
2．将G化成前束范式，消去G的存在量词,略去全称量词，得到G的Skolem形
3．建立子句集S
4．使用归结法并把归结式送入S中，直到得到空子句 ，定理得证。
定理若不成立，则归结过程不停机.
Herbrand定理的引入是为了证明归结法的完备性。对于不可满足性的证明是复杂的，这是由于个体变量论域D的任意性，以及解释的个数的无限性。通过引入基于S的Herbrand域来解决这个难题，结论是只要S在H域上不可满足，便知道S是不可满足的。Herbrand定理给出了一阶谓词逻辑的半可判定算法，意思是说，只有当定理是成立时，使用该算法方可证明定理。若定理不成立，算法不停机，无结果。Herbrand定理把谓词逻辑问题化成了有限步骤内可证明的命题逻辑问题，从而可给出了机器能够实现的算法。
一般说来，使用归结法证明定理效率是不高的，如何少做些归结仍能得到定理的证明是重要的。从而提出了归结过程的一些控制策略。如单元归结效率高，但并不完备。可以说，一种方法，虽不完备，但效率高，仍是可用的。
由于归结法的效率低，即便采用了各种控制策略的归结推理过程，仍然避免不了产生大量的不必要的归结式，使得归结法不能处理复杂问题，导致人们研究非归结方法。
Prolog语句都是Horn子句。Horn子句是一阶谓词公式的真子集，但有与一阶逻辑同样的表达能力。Prolog的解释过程是依归结法的。
【课后习题】
1. 写出下面命题的前束范式和Skolem标准形
～((
x)(
y)P(a,x,y)→(x)(～y)Q(y,b)→R(x)))2. 写出下面命题的H域
S={p(a),～p(x)∨p(f(x))}
3. 对于下面子句集，画出其语义树
S={P(x)∨Q(y),～P(a),～Q(b)}
4. 利用归结法，证明下面命题
(
x)P(x)→(x)((P(x)∨Q(x))→R(x))
(x)(y)(R(x)∧R(y))((
x)P(x)∧(x)Q(x))→(x)(P(x)∧Q(x))5.说明归结法完备性的含义