4.1.4 消解反演求解过程
4.1.1 基本思想     
　　把要解决的问题作为一个要证明的命题，其目标公式被否定并化成子句形，然后添加到命题公式集中去,把消解反演系统应用于联合集，并推导出一个空子句(NIL)，产生一个矛盾，这说明目标公式的否定式不成立，即有目标公式成立，定理得证，问题得到解决。这与数学中反证法的思想十分相似。
4.1.2 消解反演
　　1.反演求解的步骤
　　给出一个公式集S和自标公式L，通过反证或反演来求证目标公式L，其证明步骤如下：
  (1)否定L，得～L；
 (2)把～L添加到S中去；
(3)把新产生的集合｛～L，S｝化成子句集；
(4)应用消解原理，力图推导出一个表示矛盾的空子句NIL。
　　2.反演求解的正确性
　　 设公式L在逻辑上遵循公式集S，那么按照定义满足S的每个解释也满足L。决不会有满足S的解释能够满足～L的，所以不存在能够满足并集S∪｛～L｝的解释。如果一个公式集不能被任一解释所满足，那么这个公式是不可满足的。因此，如果L在逻辑上遵循S，那么S∪｛～L｝是不可满足的。可以证明，如果消解反演反复应用到不可满足的子句集，那么最终将要产生空子句NIL。因此，如果L在逻辑上遵循S，那么由并集S∪｛～L｝消解得到的子句，最后将产生空子句；反之，可以证明，如果从S∪｛～L｝的子句消解得到空子句，那么L在逻辑上遵循S。
　　3.反演求解的举例 
　　 下面举个例子来说明消解反演过程：
 

前提：每个储蓄钱的人都获得利息。

结论：如果没有利息，那么就没有人去储蓄钱。

证明：令S(x,y)表示"x储蓄y" 
 

M(x)表示“x是钱”

I(x)表示“x是利息”

E(x，y)表示“x获得y”
 

于是上述命题写成下列形式：
 

 

结论：
 

 

用化为子句集的九步法，可把前提和结论化为下列的子句集：
  S’={～S(x,y)∨～M(y)∨I(f(x)),～S(x,y)∨～M(y)∨E(x,f(x))}
 

其中，y=f(x)为Skolem函数。而,

～L＝

＝{～I(z),S(a,b),M(b)}

以下按上述的四个步骤来对问题进行反演求解：

 

(1) 否定L，即有 ～L ＝ {～I(z),S(a,b),M(b)}
 

(2) 把 face="宋体">～ L添加到S’中去，即

 

S’=｛～L，S’｝={～S(x,y)∨～M(y)∨I(f(x)),～S(x,y)∨～M(y)∨
 

E(x,f(x)),～I(z),S(a,b),M(b)}
 

(3) 把新产生的集合S’化成子句集,即

 

S’= {～S(x,y)∨～M(y)∨I(f(x)),～S(x,y)∨～M(y)∨ E(x,f(x)),
 

～I(z), S(a,b), M(b) } 
  (4) 应用消解原理，力图推导出一个表示矛盾的空子句NIL。
    该消解反演可以表示为一棵反演树，如图4.1所示，其根节点为NIL。因此，储蓄问题的结论获得证明。　
　　　　　　　　　　　　　　　　　　　　　　　　　　
　　　　
4.1.3 反演求解过程
    从该例子可以看出，用反演树求取对某个问题的答案，其过程如下：
  (1) 把由目标公式的否定产生的每个子句添加到目标公式否定之否定的子句中去。
(2) 按照反演树，执行和以前相同的消解，直至在根部得到某个子句止。
(3) 用根部的子句作为一个回答语句。
    答案求取涉及到把一棵根部有NIL的反演树变换为在根部带有可用作答案的某个语句的一颗证明树。由于变换关系涉及到把由目标公式的否定产生的每个子句变换为一个重言式，所以被变换的证明树就是一棵消解的证明树，其在根部的语句在逻辑上遵循公理加上重言式，因而也单独地遵循公理。因此被变换的证明树本身就证明了求取办法是正确的。下面讨论一个简单的问题，作为例子：
     “如果无论约翰(John)到哪里去，菲多(Fido)也就去那里，那么如果约翰在学校里，菲多在哪里呢?”
    很清楚，这个问题说明了两个事实，然后提出一个问题，而问题的答案大概可从这两个事实推导出。这两个事实可以解释为下列公式集S：
  (x)[AT(JOHN,X)=>AT(FIDO,X)]
和
  AT(JOHN,SCHOOL)
    如果我们首先证明公式
  (x)AT(FIDO,X)
    在逻辑上遵循S，然后寻求一个存在x的例，那么就能解决“菲多在哪里”的问题。关键想法是把问题化为一个包含某个存在量词的目标公式，使得此存在量词量化变量表示对该问题的一个解答。如果问题可以从给出的事实得到答案，那么按这种方法建立的目标函数在逻辑上遵循S。在得到一个证明之后，我们就试图求取存在量词量化变量的一个例，作为一个回答。对于上述例题能够容易地证明(x)AT(FIDO,X) 遵循S。我们也可以说明，用一种比较简单的方法来求取合适的答案。
     消解反演可用一般方式得到，其办法是首先对被证明的公式加以否定，再把这个否定式附加到集S中去，化这个扩充集的所有成员为子句形，然后用消解证明这个子句集是不可满足的。图4.2表示出上例的反演树。从S中


的公式得到的子句叫做公理。注意目标公式(x)AT(FIDO,X)的否定产生
 
(x)[～AT(FIDO,X)]

其子句形式为
  ～AT(FIDO,x)

对本例应用消解反演求解过程，我们有：
  (1) 目标公式否定的子句形式为 :～AT(FIDO,x)
  把它添加至目标公式的否定之否定的子句中去，得重言式
  ～AT(FIDO,x)∨AT(FIDO,x)
  (2) 用图4.3的反演树进行消解，并在根部得到子句:AT(FIDO，SCHOOL)
  (3) 从根部求得答案AT(FIDO，SCHOOL)，用此子句作为回答语句。因此，子句
  AT(FIDO，SCHOOL)就是这个问题的合适答案，见图4.3。