4.1.2 消解推理规则     
　　令L1为任一原子公式，L2为另一原子公式；和具有相同的谓词符号，但一般具有不同的变量。已知两子句L1∨α和～L2∨β如果L1和L2具有最一般合一者σ，那么通过消解可以从这两个父辈子句推导出一个新子句(α∨β)σ。这个新子句叫做消解式。它是由取这两个子句的析取，然后消去互补对而得到的。
    下面举出几个从父辈子句求消解式的例子:
(a) 假言推理   (b) 合并
父辈子句
   
消解式
     
(c) 重言式    
父辈子句

 
消解式
     
(d) 链式(三段论)   (e) 空子句(矛盾)
父辈子句
 
消解式
    　　从以上各例可见，消解可以合并几个运算为一简单的推理规则。