消解原理的基础知识
    (1) 谓词公式、某些推理规则以及置换合一等概念。
    (2) 子句:由文字的析取组成的公式(一个原子公式和原子公式的否定都叫做文字)。
    (3) 消解:当消解可使用时,消解过程被应用于母体子句对,以便产生一个导出子句。
    例如,如果存在某个公理E1∨E2和另一公理～E2∨E3,那么E1∨E3在逻辑上成立。这就是消解,而称E1∧E3为E1∨E2和～E2∨E3的消解式(resolvent)。

自动控制网www.eadianqi.com版权所有

一、子句集的求取

本文来自www.eadianqi.com

1.步骤
    (1) 消去蕴涵符号
    只应用∨和～符号,以～A∨B替换A=>B。
    (2) 减少否定符号的辖域
    每个否定符号～最多只用到一个谓词符号上,并反复应用狄•摩根定律。
    (3) 对变量标准化
    在任一量词辖域内,受该量词约束的变量为一哑元(虚构变量),它可以在该辖域内处处统一地被另一个没有出现过的任意变量所代替,而不改变公式的真值。合适公式中变量的标准化意味着对哑元改名以保证每个量词有其自己唯一的哑元。
    (4) 消去存在量词
    用Skolem函数代替存在的x,就可以消去全部存在量词,并写成:
        (y)P[g(y),y]
    从一个公式消去一个存在量词的一般规则是以一个Skolem函数代替每个出现的存在量词的量化变量,而这个Skolem函数的变量就是由那些全称量词所约束的全称量词量化变量,这些全称量词的辖域包括要被消去的存在量词的辖域在内。Skolem函数所使用的函数符号必须是新的,即不允许是公式中已经出现过的函数符号。例如: 本文来自www.eadianqi.com
        (y)(x)P(x,y)被〔(y)P(g(y),y)〕代替,其中g(y)为一Skolem函数。
    如果要消去的存在量词不在任何一个全称量词的辖域内,则用不含变量的Skolem函数即常量。例如,(x)P(x)化为P(A),其中常量符号A用来表示人们知道的存在实体。A必须是个新的常量符号,它未曾在公式中其它地方使用过。
    (5) 化为前束形
    把所有全称量词移到公式的左边,并使每个量词的辖域包括这个量词后面公式的整个部分。所得公式称为前束形。
    (6) 把母式化为合取范式任何母式都可写成由一些谓词公式和(或)谓词公式的否定的析取的有限集组成的合取。这种母式叫做合取范式。
    (7) 消去全称量词
    消去明显出现的全称量词。
    (8) 消去连词符号∧
    用{A,B}代替(A∧B),以消去明显的符号∧。反复代替的结果,最后得到一个有限集,其中每个公式是文字的析取。任一个只由文字的析取构成的合适公式叫做一个子句。

自动控制网www.eadianqi.com版权所有

本文来自www.eadianqi.com

2.例
    将下列谓词演算公式化为一个子句集
        (x){P(x){(y)[P(y)P(f(x,y))]∧～(y)[Q(x,y)P(y)]}}

本文来自www.eadianqi.com

3.说明
    并不是所有问题的谓词公式化为子句集都需要上述9个步骤。对于某些问题,可能不需要其中的一些步骤。

二、消解推理规则 自动控制网www.eadianqi.com版权所有

1.消解式
    令L1为任一原子公式,L2为另一原子公式;L1和L2具有相同的谓词符号,但一般具有不同的变量。已知两子句L1∨α和～L2∨β,如果L1和L2具有最一般合一者σ,那么通过消解可以从这两个父辈子句推导出一个新子句(α∨β)σ。这个新子句叫做消解式。它是由取这两个子句的析取,然后消去互补对而得到的。 自动控制网www.eadianqi.com版权所有

2.消解式求法
    (1) 假言推理
    (2) 合并
    (3) 重言式
    (4) 空子句(矛盾)
    (5) 链式(三段论)

自动控制网www.eadianqi.com版权所有

三、含有变量的消解式
    为了对含有变量的子句使用消解规则,必须找到一个置换,作用于父辈子句使其含有互补文字。

自动控制网www.eadianqi.com版权所有

四、消解反演求解过程 自动控制网www.eadianqi.com版权所有

1.基本思想
    把要解决的问题作为一个要证明的命题,其目标公式被否定并化成子句形,然后添加到命题公式集中去,把消解反演系统应用于联合集,并推导出一个空子句(NIL),产生一个矛盾,这说明目标公式的否定式不成立,即有目标公式成立,定理得证,问题得到解决,与数学中反证法的思想十分相似。

2.消解反演
    反演求解的步骤
    给出一个公式集S和目标公式L,通过反证或反演来求证目标公式L,其证明步骤如下:
    (1) 否定L,得～L;
    (2) 把～L添加到S中去;
    (3) 把新产生的集合{～L,S}化成子句集;
    (4) 应用消解原理,力图推导出一个表示矛盾的空子句NIL。
    反演求解的正确性
    设公式L在逻辑上遵循公式集S,那么按照定义满足S的每个解释也满足L。决不会有满足S的解释能够满足～L的,所以不存在能够同时满足S与～L的解释。如果一个公式集不能被任一解释所满足,那么这个公式是不可满足的。因此,如果L在逻辑上遵循S,那么{～L,S}是不可满足的。由于空子句不可被满足,因此,如果L在逻辑上遵循S,那么由并集{～L,S}不断消解最后将产生空子句;反之,可以证明,如果从{～L,S}的子句消解得到空子句,那么L在逻辑上遵循S。 本文来自www.eadianqi.com

3.反演求解过程
    步骤
    (1) 把由目标公式的否定产生的每个子句添加到目标公式否定之否定的子句中去。
    (2) 按照反演树,执行和以前相同的消解,直至在根部得到某个子句止。
    (3) 用根部的子句作为一个回答语句。
    分析
    答案求取涉及到把一棵根部有NIL的反演树变换为在根部带有可用作答案的某个语句的一颗证明树。由于变换关系涉及到把由目标公式的否定产生的每个子句变换为一个重言式,所以被变换的证明树就是一棵消解的证明树,其在根部的语句在逻辑上遵循公理加上重言式,因而也单独地遵循公理。因此被变换的证明树本身就证明了求取办法是正确的。
    例:储蓄问题
        前提:每个储蓄钱的人都获得利息。
        结论:如果没有利息,那么就没有人去储蓄钱