目标公式含有全称量词的情况

    当目标公式含有全称量此量化的变量时,目标公式的否定式中会出现Skolem函数,结果会与要求不符。这一点从下面的例子可以看出。        

        例1 已知事实为

    (1)对所有的x,x是p(x)的孩子。

              ("x)c(x,p(x))

    (2)对所有的x、y,如果x是y的孩子,则y是x的父辈。

              ("x)("y)[c(x,y)®P(y,x)]

     解答问题:

    (3)对任何一个x,谁是x的父辈?

              ("x)($y)P(y,x)

     目标公式的否定式为

              ($x)("y)[ØP(y,x)] 

     目标公式否定式的子句形式为

               ØP(y,A)

     其中A为没有自变量的Skelom函数(即常量)。此例的修改证明树如图442-1所示。解答语句为P(p(A),A)。解答过程中出现的常量A与问题中的“任何一个x”不符。事实上可以证明,在解答提取过程中,可以用新变量代替来自目标公式否定式的子句中的Skolem函数,这些新变量经过替换过程仍会出现在解答语句中。在本例中,经过用新变量代替后的修改证明树如图442-2所示,最后的解答为P(p(t),t)。

             

                   图442-1 例1的修改证明树

           

                   图442-2 例1中变量替换后的修改证明树

    例4 给出子句:

        P(z,u,z)P(A,u,u)

目标公式为

        ($x)("z)($y)P(x,z,y)

目标公式否定式的子句形式为

         ØP(x,g(x),y)

反演树和修改证明树如图442-3所示,其中Skolem函数g(x)用变量w代替,得到的解答子句为

         P(z,w,z)ÚP(A,w,w)

除了变量名外,这个解答与给出的子句是完全相同的。 

                    

                          图442-3 例4的反演树和修改证明树

    习题

    一个积木世界的状态由下列公式集描述:

        ONTAbLE(A)  cLEar(E)

        ONTAbLE(c)  cLEar(D)

        ON(D,c)     HEAVY(D)

        ON(b,A)     WOODEN(b)

        HEAVY(b)    ON(N,E)

给出这些公式所描述的状态草图。

    下面语句提供了有关描述这个积木世界的一般知识:

    每个在任一积木块之上的大的蓝色积木块是在一个绿色积木块之上。

    每个重的木制积木块是大的。

    所有顶上没有东西的积木都是蓝色的。

    所有木制积木块都是蓝色的。   

    以单文字后项的蕴含式的集合表示这些语句。给出能求解“哪个积木块是在绿色积木块上”这个问题的一致解图。

                                                                         返回