逻辑运算程序_归纳逻辑程序设计初探200897

发布时间：2016-12-20 14:33

本文关键词：归纳逻辑程序设计初探，由笔耕文化传播整理发布。

了，而消解的主要原理来自于罗宾逊（J.A.Rob；2.2.2赫尔布兰德解释；前面我们说明了，为了证明A→B，只需证明经过反证；下面我们就介绍一个这样的论域，，即赫尔布兰德域；定义2.12集合H称为子句集S的赫尔布兰德域，如；H0=；{c∣c为S中出现的常元}；H1=H0∪{f（t1，t2，?，tn）∣t1，；因为子句集中没有常元，因此H0={a}；H1={a,

了，而消解的主要原理来自于罗宾逊（J.A.Robinson）在1965年提出的消解原理，这个原理是罗宾逊在赫尔布兰德（Herbrand）理论的基础上产生的。那么我们就先来了解一下赫尔布兰德理论中的核心概念——赫尔布兰德解释。

2.2.2 赫尔布兰德解释

前面我们说明了，为了证明A→B，只需证明经过反证法变换的一阶公式A∧?B是不可满足的即可。所谓不可满足就是指对于所有论域上所有可能的解释，A∧?B均取假值。而一阶逻辑公式的解释往往有无穷多种，研究所有论域上的所有解释是不方便的，也是不可能的。如果可以把一阶逻辑公式的子句集在任意域上的不可满足问题转化在一个比较简单的特殊论域上的不可满足问题。那么这个问题就简单很多。

下面我们就介绍一个这样的论域，即赫尔布兰德域。

∞

定义2.12 集合H称为子句集S的赫尔布兰德域，如果H= ∪ Hi，其中Hi递归定义如下： i = 0 {a} 当S中无任何常元出现时，H0由任意单个常元构成，如{a}，

H0=

{c∣c为S中出现的常元}

H1= H0∪{f（t1，t2，?，tn）∣t1，t2，?，tn ∈H0，f为S中出现的函数符号} H i +1 = Hi∪{ f（t1，t2，?，tn）∣t1，t2，?，tn ∈Hi，f为S中出现的函数符号} 例如：设子句集S={P(x)∨?Q(x), R(f(x)), ?P(y) ∨?R(x)}，那么这个子句集的赫尔布兰德域为：

因为子句集中没有常元，因此H0={a}

H1={a, f(a)}

H2={a, f(a), f(f(a)) }

???

H∞={a, f(a), f(f(a)), f(f(f(a))), ? }

为了讨论方便，我们需要以下术语：

定义2.13如果项、原子公式、文字、子句以及代入实例中没有变元，那么它们分别称为基项、基原子公式、基文字、基子句和基例。

根据这个定义，赫尔布兰德域中的元素，事实上是一阶语言中的一些基项。我们知道一阶逻辑公式在不同的论域上可以有不同的解释，那么在赫尔布兰德域上对一阶逻辑公式也要有解释。有如下定义：

定义2.14子句集S在其赫尔布兰德域H上的解释称为赫尔布兰德解释（用I（H）表示），

它满足如下条件：

（1）在I（H）下，常元映射到自身。

（2）对S中的任一n元函数f，I（H）(f)为赫尔布兰德域H上的函数，且对于t1,t2,?,tn

∈H，I（H）(f(t1,t2,?,tn))= f(t1,t2,?,tn)。

（3）对S中的任一谓词P，I（H）(P)是赫尔布兰德域H上的关系。

赫尔布兰德解释是把一阶语言中的基项解释为基项自身，解释之后这个被解释的基项就是赫尔布兰德域中的元素。这样，子句集的不可满足问题转化为S在其赫尔布兰德域上的不可满足问题，有如下定理：

定理2.2子句集S是不可满足的，当且仅当所有赫尔布兰德解释都不满足S。

如果S中有个体常元，则它的赫尔布兰德域是唯一的。

赫尔布兰德还给出了赫尔布兰德定理。这个定理在人工智能的发展中具有重要作用。因为本文重点讨论在机器上实现机器定理证明的消解定理，因此此处不再赘述赫尔布兰德定理，接下来我们重点介绍罗宾逊的消解定理。

2.2.3 消解原理

前面我们提到了，消解就是从子句中消去一些项的机械过程，目的是产生空子句，从一阶逻辑公式的不可满足性，证明待证定理。罗宾逊将消解定理定义如下：

定义2.11 令L1为一个正文字，L2为一个负文字，如果?L1=L2，则L1和L2形成一个互补对。

定理2.2（消解原理）：设C1，C2是子句集中的任意两个子句，如果C1中的文字L1与C2 中的文字L2形成一个互补对，则从C1和C2中分别消去L1和L2，并将这两个子句中余下的部分做析取构成一个新的子句C12，称这一过程为消解，所得到的子句C12称为C1和C2的消解式，称C1和C2 为C12的亲本子句。形式如下：

C1=A∨L1 ，C2=B∨L2

C12=A∨B

也可以表示为C12=（C1–{L1}）∪（C2– {L2}），这里“–”表示“集合差运算”。根据消解定理，消解式C12是其亲本子句C1和C2的逻辑结论。同时也可以得到一个推论，即把得到的消解式再放入子句集中，继续进行消解，直至得到空子句，从而程序停止，定理得到证明。

推论2.1 设C1和C2是子句集S中的子句，C12是C1和C2的消解式。如果把C12加入子句集S后得到新子句集S1，则S1和S是同可满足性的，即：S是不可满足的当且仅当S1是不可满足的。

在消解的过程中，还有一个问题时必须要注意的，由于在子句中可能存在个体变元和函数，所以从子句集中寻找子句的互补对就比较复杂了，因此，需要对子句执行一些操作，使得一阶逻辑公式可以与计算机的模式相匹配，这些操作就是置换和合一。

置换（substitution）又名替换或代换。目的是在若干看起来个体变元完全不相同的子句中，通过置换的手段使不同子句变元表达符号一致，从而便于找到消解式，以便能进行消解。置换可以简单地理解为在一个子句中，用置换项替换个体变元，本质上是变元到项的任意映射。正式的定义如下：

定义2.12 置换是形如{t1/x1，t2/x2，……，tn/xn}的一个有限集。其中，xi是变元，ti是项。不含任何元素的置换称为空置换，用ε表示。

例：有下述若干命题：

（1）所有不富有并且聪明的人是快乐的。

（2）喜欢音乐的人是聪明的。

（3）Peter喜欢音乐并且不富有。

（4）快乐的人过着激动人心的生活。

求证：Peter过着激动人心的生活。

证明：根据题干，给出谓词

根据题意，可列出以下一阶逻辑公式

可将条件和求证目标放在一起，并化为子句形式，可得：

（1） Rich(x)∨?Smart(x)∨Happy(x)

（2）?Music(x)∨Smart(x)}

（3）Music(Peter)

（4）? Rich(Peter)

（5）?Happy(x)∨Exciting(x)

（6）?Exciting(Peter)

对上述子句消解处理：

（7）?Happy(Peter) （（5）、（6）作置换{ Peter /x}然后消解）

（8）Smart(Peter) （（2）、（3）作置换{ Peter /x}然后消解）

（9）? Smart Peter)∨Happy(Peter) （（1）、（4）作置换{ Peter /x}然后消解）

（10）? Smart(Peter) （（7）、（9）消解）

（11）Smart(Peter) ∧? Smart(Peter)? □ （（8）、（10）消解，得到空子句）

所以Peter过着激动人心的生活。

以上这个例子很好地揭示了置换和消解过程。所谓合一（unify）是指通过置换，使得不同的表达式变为相同的表达式的算法。

定义2.13 设有表达式集{E1，E2，……，En}和置换θ，使E1θ=E2θ= …=Enθ，便称E1，E2，……，En是可合一的，且θ称为合一置换（不是唯一的）。5

例如：集合{P(x),P(f(y))}是可合一的，因为置换θ={f(a)/x, a/y}使得P(x)θ=P(f(a))= P(f(y))θ=P(f(a))。因此θ是合一置换。

定义2.14 若E1，E2，……，En有合一置换σ，且对E1，E2，……，En的任一合一置换θ，都存在一个置换λ，使得θ=σλ，则称σ是E1，E2，……，En的最一般合一置换，记作mgu。

根据最一般合一置换，前面的消解式也可以表示为：

C12=（C1σ–{L1σ}）∪（C2σ– {L2σ}）

置换与合一的作用除了进行模式匹配之外，还有简化推理过程的作用，因为在机器定理证明过程中，推理中子句数量往往成指数级增长，包括产生的大量冗余的子句，降低了推理的效率，因此要删除或减少这些冗余。

以上就是合一消解系统的基本内容，它是机器定理证明的基础，也是我们后面要讨论的归纳逻辑程序设计的逻辑基础。其消解的过程可以概述如下：

合一消解的过程6如下：

（1）写出一阶逻辑公式；

（2）将一阶逻辑公式用反证法形式写出；

（3）将由（2）得到的公式转化为合取得Skolem标准型；

（4）求取（3）的子句集S；

（5）对S中可消解的子句做消解；

（6）由（5）得到的消解式仍放入S中，重复消解过程；

（7）得到空子句；

（8）定理得证。

下面我们来介绍子句逻辑的另一个重要的系统，霍恩子句推理系统，这个系统是形成归纳逻辑程序设计基础的重要系统。

2.3 霍恩子句推理系统

前面我们已经看到，一阶逻辑具有很强的表述能力，使得一阶逻辑的消解定理在进行机器定理证明、问题求解等方面发挥了重要的作用。为了使问题的描述更加简明、自然，5

6 E是表达式，θ是置换，Eθ是对表达式E进行置换θ后得到的结果。马少平朱小燕/著人工智能清华大学出版社 2004年8月第一版，107页

并具有一定的过程意味，需要使推理过程程式化，这就需要一个重要的工具，即霍恩子句，这个子句因逻辑学家A.霍恩（Horn）对其性质作了详尽的研究，故而得名。关于子句的定义前面已经讲过了，下面我们就定义什么是霍恩子句以及由此发展出的逻辑程序设计。

2.3.1 霍恩子句

前面我们定义了子句是若干文字的析取，因此子句C1=P1∨P2∨??∨Pm∨?Q1∨?Q2∨??∨?Qn可以表示为C2=Q1∧Q2∧??∧Qn→P1∨P2∨??∨Pm。如果我们可以约定这个蕴涵式的前件的文字间恒为合取，而后件的文字间恒为析取，那么可以将C2改写为C3= Q1,Q2,?,Qn→P1,P2,?,Pm。这里我们由于技术上的原因，将这个C3改写成为：

（1） C=P1,P2,?,Pm←Q1,Q2,?,Qn。其中“P1,P2,?,Pm”这部分称为子句头，

“Q1,Q2,?,Qn”称为子句体。

当m=0时，（1）可以写成：

（2） C=←Q1,Q2,?,Qn。

当n=0时，（1）可以写成：

（3） C=P1,P2,??,Pm←。

这样的子句蕴涵表达形式使得问题的描述更接近问题的自然描述，使得许多问题的形式表述可以直接用子句形式写出。

霍恩子句是一类特殊的子句，它被定义为至多包含一个正文字的子句。即当上面的子句（1）中，m=1时的子句，表示为：P←Q1,Q2,?,Qn。因此，霍恩子句必须是以下4种形式之一：

① P←Q1,Q2,?,Qn （n不等于0），

② P← （上式中n=0），

③ ←Q1,Q2,?,Qn （n不等于0），

④ □ (上式中n=0)。

其中，我们把①这种形式的霍恩子句称为一个过程，②这种形式的霍恩子句称为一个事实，而把③称为目标，④则称为停机语句，表示程序执行终止。

2.3.2 逻辑程序设计

可以看出，霍恩子句形式简明，逻辑意义清晰，最重要的是其消解过程可以与计算机程序的执行过程统一起来，因此研究者们开始将霍恩子句逻辑直接作为程序设计语言。传统的程序设计来说，算法的逻辑意义往往被程序复杂的控制成分所掩盖，使程序的正确性难以得到证明。而且通常的高级程序设计语言属于过程性语言，需要在程序执行前详细规定运行步骤。科瓦尔斯基对传统的算法或对用通常高级语言编写的程序提出了一个著名的分析公式，即算法＝逻辑＋控制。其基本思想是要从根本上改变程序设计的方法：用户只

下载地址：归纳逻辑程序设计初探200897.Doc

　　【】