1.为证明A→B(可称作定理)是重言式, 依定理2.8.2等价于A∧
B是矛盾式。
使用归结证明法,就是从A∧
B出发。
2.建立子句集S
将A∧
B化成合取范式。如
P∧(P∨R)∧(
P∨
Q)∧(
P∨R)
形式, 进而将所有子句(析取式)构成子句集合S:
S = {P, (P∨R), (
P∨
Q), (
P∨R)}
即以集合来描述这合取范式,这种表示法对归结过程的阐明是方便的。
3.对S作归结
进而对S的子句作归结(消互补对), 如子句P∨R与
P∨
Q作归结, 得归结式R∨
Q(这新子句便为归结式)。并将这归结式仍放入S中。重复这过程。
4.直至归结出矛盾式□
使用归结证明法, 就是要证明子句集S是不可满足的。如在归结过程中, 出现归结式P以及归结式
P, 使是矛盾, 以□表示。证明结束。