逻辑式程序设计语言.doc

第12章 第12章 逻辑式程序设计语言 无论是命令式还是函数式程序都把程序看作是从输入到输出的某种映射。当然命令式语言有时没有数据输出，但也要“输出”某些动作。为了实现这种映射，程序要对数据结构实施某个算法过程，算法实现该程序功能。算法又是以程序语言提供的控制机制实现计算逻辑。所以，R.Kowalski说: 算法 = 逻辑 + 控制 然而传统语言计算逻辑在程序员心里，隐式地体现在程序正文之中，为此程序正确性证明还要把它隐含的逻辑以断言形式地写出来 。 自然人们会想到能不能把描述计算的理论基础命题演算和谓词演算直接变为程序设计语言。这样，也许不必用求值来判定某件事情的真、伪，直接根据事实和规则判定真伪，“找出”解。事实上，这是可行的，而且在人工智能的专家系统、语言理解、数据库查询中非常需要这种程序设计语言。1970年诞生的Prolog长久不衰就是例证。 逻辑程序设计的基本观点是程序描述的是数据对象之间的关系，它的抽象层次更高而不限于函数(映射)关系。关系也是联系，对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述，根据规则找出合乎逻辑的事实就是推理。因此，逻辑程序设计范型是陈述事实，制定规则，程序设计就是构造证明。程序的执行就在推理，和传统程序设计范型有较大的差异。 本章我们从逻辑程序设计理论基础，谓词演算导出逻辑程序语言的理论模型，并介绍逻辑程序设计语言Prolog的主要特征和实现要点。12.1 谓词演算 谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型，谓词演算在所有计算机理论的书籍中均有论述，本章仅简单复习，主要目的是引入术语。 12.1.1 谓词演算诸元素 用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质(properties)，以及对象间有些什么关系(relations)。为了一般化还要有变量(variable)指明域上某个(些)对象，以及准确说明对象情况的量词(quantifiers)。当然这个语言还需要一些辅助的符号(继承自初等集合论)。描述以公式(Formulas)表达，即描述一般命题的谓词。谓词公式中各元素按一定逻辑规则变换即谓词演算(predicate calculus)。以下是谓词公式的示例: $Xp(X)存在具有性质p的对象X。 Yp(Y)所有的Y，即域上任何对象，均具有性质p。 X$Y(X=2*Y)对于所有的X都可以找到Y，其值为X的一半，其中的逻辑连接”=”是中缀表示。等效于=(X，2*Y)。 谓词公式各元素符号表示法在各教程中不尽相同，谓词演算的表示由以下元素组成: (1)公式 由一组约定的符号组成的序列，它包括常量(指明域上的某个对象)、变量(域上任意对象)、逻辑连接(指明对象状态及对象间的关系，有数量上的、=、=、=、/=和逻辑上的、 、)、命题函数(指明对象间的函数性质)，谓词(对象间约定的关系)，量词(逻辑连接的一种，指明对象状态)。一阶谓词演算系统中公式里不得嵌套谓词。 (2)常量 指明论域(universe of discourse)上的对象，也是数学对象。通常一个逻辑系统要引入多个论域，一般有十进制整数域、真值域、字符域，可用不同的符号表达有区别的域。常量可以看作是退化了的函数(没有变元)。常量以字面量或小写字母表示。 (3)变量 可束定到特定域上某个范围的对象上，在演算(归约)期间它可以例化为具体对象(常量对象)，变量是数学意义的，一旦束定整个演算期间不变，变量以大写字母表示。 (4)函数 表征对象具有的映射关系，函数带参数，从变元域映射到结果值域(可以是不同的域)。变元一般是常量、变量、函数结果值、变元在语法上都叫项(term)。函数以小写标识符表示。 (5)谓词 表征对象某种性质的符号，谓词带上一到多个变元(对象)即为断言(assertion)。它断言这些对象具有谓词所指性质，谓词形如函数，当该变元确实具有所指性质时隐含真值，否则为假。 当谓词应用到的变元是常量或已被束定的变量上时，就叫做句子(senteuce)或命题(proposition)，查询时能返回真假值。当谓词应用到变量或包含变量的项上时，它依然是谓词但不能形成句子，只有例化才能判定真伪，形成句子。 谓词变元的个数称作目(arity)，故有单目、N目谓词之称。 例12-1 N-目谓词的例子。 谓词 目 含义 odd(X) 1 X是奇数 father(F，S) 2 F是S的父亲 divide(N，D，Q，R) 4 N除D得商Q和余数R 谓词例化 结果值 odd(2) False divide (23，7，3，2) Ture father (changshan，changping) True divide (23，7，3，N) N未例化，不知真假 (6)量词 变量可以代表域中任何对象，量词可以指定某种集合，量词有两个，一为全称、一为存在$，量词限定的变量名作用域是整个公式，它说明同名变量。有些谓词经量词修饰后即没有变量，可成句子或命题。 例12-2 量化谓词 量化谓词 结果值 Xodd(X) False $Xodd(X) True X(X=2*Y+1odd (X) True X$Ydivide (X，3，Y，0) False $X$Ydivide (X，3，Y，0) True，如X =3，Y=1 $XYdivide(X，3，Y，0) False，但很难证明 证明一个全称谓词是比较难的，因为最可靠的证明方法是枚举例证，这对于论域大的公式就很困难了。于是采取反证的方法，如能找出一个反例则原公式(也是命题)为假，这种假言推理的表示恰好将全称改为存在，全称量化的谓词取反: 例12-3 量化公式 量化谓词 取反 Xodd(X) $Xnot odd(X) 1 $Xodd(X) Xnot odd(X) 2 X(X=2*Y+1odd(X) $Xnot(X+2*Y+1odd(X) 3 $Xnot(X=2*Y+1)or odd (X) 4 $X(X=2*Y+1)and not add(X) 5 X$Y divide (X，3，Y，0) $XY not divide (X，3，Y，0) 6 $X$Y divide (X，3，Y，0) XY not divide (X，3，Y，0) 7 $XY divide (X，3，Y，0) X$Y not divide (X，3，Y，0) 8 第4、5行实际就是通过谓词演算得到更加直观的等价式，因为局部not是极容易找出例证的。 (7) 逻辑操作 and，or，not，(蕴含) (全等)是最基本的逻辑运算符，然而，最本质的有and ()，or()，not ()就够了，如: AB = not A or B = A B AB=(A and B) or (not (A and (not B) = ( A B) (A B) 命题演算即原子命题通过逻辑连接，等价变换，达到验证命题真理性的目的。谓词演算以准确的谓词描述论域上对象的逻辑关系，通过等价变换达到证明一般命题真理性的目的。命题演算是谓词演算的特例。12.1.2 谓词演算的等价变换 等价变换即演绎推理，不同的逻辑连接有其等价变换的规则。命题，谓词演算规则可以查有关文献。本节演示一般谓词公式变换为子句的实例。号为“可推出”。 1 以，如上例消除、符号。 2化为前束范式，消除最外的符号，即否定符号内移。 ($Xp(X)X( p(X) 3利用斯柯林变换消去存在量词。如： X$Z(c (Z，X) b(X)X(c (z，X) b(X) 再如: X(a ( X) b(X) $Y c (X，Y) X(a (X) b(X) c (X，g(X) (11.1) 其中g(X)是对任何一X可得到(存在)的Y。 4 消除前束范式的全称量词。既然设定所有变量均为全称，要不要符号都是一个意思，即都要搜索全域才能证实该变量，则(11.1) 式为: a(X) b(X) c (X，g(X) (11.2) 5利用分配率P(QR)=(PQ)(PR)化成合取范式，(11.2)式成为: (a(X) c (X，g(X) b(X) V c (X，g(X) (11.3) 经过以上变换任何一复合公式均可成为如下形式: F = C1C2 Cn (11.4) 且其中Ci称为子句，如果以，代替，且其次序无关可表达为集合形式: F = C1，C2， ,Cn 其中Ci内部没有其它逻辑连接符号，只有。若以;代则有: Ci=L1 L2 Lv = L1;L2;Lv (11.5) 因此，任一公式均可化为连接的子句的集合，证明连接的子句为真是很容易的，但证明整个公式为真则需所有子句均为真，即子句逻辑。12.2 自动定理证明 自1879年Frege正式研究符号逻辑以来，至本世纪30年代末的五十年期间，数理逻辑发展比较完备，它们一直用作基础数学的证明系统。电子计算机问世后，人们不仅借助计算机完成手工不能完成的证明工作(如1987年的四色定理证明)，更感兴趣的是用逻辑定理对程序作正确性的自动证明。本节简述证明系统的概念和模型。 12.2.1 证明系统 用谓词演算公式描述的事实即证明系统中的公理(axioms)，证明系统(proof system)是应用公理演绎出定理(theorems)的合法演绎规则的集合。所谓演绎，也叫归约(deduction)，是对证明系统中合法推理规则的一次应用。在一个简单的演绎步骤中，可以从公理导出结论(conclusion)，中间可利用以这些规则演绎出的定理。 证明(proof)是个语句序列，以每个语句得到证明而结束，即每个句子要么演绎成公理，要么演绎成前此导出的定理。一个证明若有N个语句(命题)则称N步证明，反驳(refutation)是一个语句的反向证明。它证明一个语句是矛盾的，即不合乎给定的公理。 同一命题的正向证明和反驳有时会有天壤之别，证明长度和复杂性差别很大。构造一个证明或反驳要有深入的洞察、联想还要有点灵感。写得好，脉络清晰，句子简明，反之臃肿晦涩。即使是较差的证明构造起来也要有点技巧。 一个语句若能从公理出发推演出来，则称合法语句，任何合法语句也叫做定理(theorem)。从某一公理集合导出的所有定理集合称为理论(theory)。一般说来，理论具有一致性，它不包含相互矛盾的定理。12.2.2 模型 从公理集合中导出定理集称之为理论，有了理论我们要解释它的语义必须借助某个模型(model)。因为形式系统只是符号抽象，借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个论域，并表明域上成员和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质，函数派定为对域中对象的操作。不一致的理论就没有模型，因为无法找到同时满足相互矛盾定理的解释。 公理集合一般情况下只是定义的部分(偏)函数和谓词，是问题域的一个侧面。所以能满足该理论的模型往往不止一个。如，下例是一“间隔数理论”为找出该理论的一个模型，先找一个论域，它必需要能解释给出的三个公理，常量1和2，函数符+，谓词interval。 例12-4 一个最简单的理论 公理集: Xinterval(X)not interval (X+1) (a1) Xnot interval (X+1)interval(X) (a2) 2=1+1 (a3) 从间隔数公理可导出定理: Xinterval (X)interval (X+2) (t1) Xinterval (X+2) interval(X) (t2) 如果我们设定论域是整数，则1，2可解释为整数一和二，且+就是整数加(符合公理a3)，即加函数。谓词interval(间隔数)在整数域上显然有两个子域odd(奇数)、even(偶数)都能够满足。如果奇数都是间隔数，在本理论中偶数定然不是。反之，奇数不是。既然我们论述在整数域上，对任一整数我们倒反不能确定它是否为间隔数了，间隔数理论不能证明interval(3)，也不能证明not interval(3)为真命题。这就是Milbert讨论过的可判定性(decidability)问题。1936年Church和Turing证实谓词演算可判定性问题是没有解的，因为不存在也不可能证明一个算法能正确地验证非真命题。对于真命题即使有算法过程存在，也要在无限长的时间才能做完证明。 然而，一旦我们断言interval(3)或interval(2)是真命题，我们立刻可通过演绎证明按这个理论写出的每一个谓词为真。这就是Goedel和Herbrand1930年证实的谓词演算具备的完整性(completeness)。它可以证明该理论所有模型里的每一语句为真。谓词演算可用来开发每一逻辑真命题的形式证明系统。甚至存在机械的证明方法(Gentzen 1936)。12.2.3 证明技术 从谓词演算具有完整性，理论上可作出自动生成程序并证明按公理集合建立的任何理论，它们是公理集合的逻辑结论。但实际做起来，要找到切题的证明如同大海捞针，效率难以容忍。 即使把问题限制在证明单个命题，关键仍然是效率。如果我们从公理出发做出每一个步骤，在新的步骤上仍然要查找每一个公理找出可能的推理。如此下去就形成一个庞大的树行公理集，每层的结点都是表示一个公理的语句，其深度和宽度随问题和最初给出的公理而定，一层一步骤，N层的树就是N步推理。 对于自动定理证明程序，只有穷举每条可能的证明步骤才能说它是完全的。然而，穷举完所有路径马上遇到组合爆炸问题，无论是深度优先还是广度优先，百步演绎可能的路径数都是天文数字。以下是证明路径示例。 例12-5 试证65534是个好整数 设谓词good(X)表示X是好整数。谓词Powtwo(Y，Z)表示2的Y次方为Z，显然，powtwo(0，1)是事实。若A是好整数与 2 作整数运算之后结果仍应为好整数。若2p=A且p为好整数则A也是好整数，2p+1=2*A也都是显然的公理。所以有: 公理 f1 good(0) f2 powtwo(0，1) r3 good(A-2)good(A) r4 good(A+2)good(A) r5 good(A*2)good(A) r6 good(A)powtwo(P，A)，good(P) r7 powtwo(P+1，A*2)powtwo(P，A)七条公理中有两个事实5条规则，以下证明过程: s1 good(2) f1和r4 s2 good(4) s1和r5 s3 powtwo(1，2) f2和r7 s4 powtwo(2，4) s3和r7 s5 powtwo(3，8) s4和r7 s6 powtwo(4，16) s5和r7 s7 good(16) s2，s6和r6 s8 powtwo(5，32) s6和r7 s9 powtwo(6，64) s8和r7 s10 powtwo(7，128) s9和r7 s11 powtwo(8，256) s10和r7 s12 powtwo(9，512) s11和r7 s13 powtwo(10，1024) s12和r7 s14 powtwo(11，2048) s13和r7 s15 powtwo(12，4096) s14和r7 s16 powtwo(13，81926) s15和r7 s17 powtwo(14，16384) s16和r7 s18 powtwo(15，32768) s17和r7 s19 powtwo(16，65536) s18和r7 s20 good(65536) s7,s19和r6 s21 good(65534) s20和r3 得证 这个证明人工花了21步，机器怎么会知道？ 它必须把每个事实和已证明的定理逐个代入到这5个规则中验证得出新的定理，每得出一个powtwo(p+1，A*2)后要像第七步s7和第二十步s20一样把幂和值分出来，连试探到计算至少要操作7 21=4.71731017次(4.72亿亿次)。12.2.4 归结定理证明 不加限制地写出公理，穷举证明显然不是一条自动证明的出路。因为要机器自动查匹配演算到预期的合适公式，代价是极大的。于是对谓词公式的写法加以限制，即在12.1.2节把任何公式化为子句逻辑的办法可以省去一大片的归约演算，即使如此，穷举证明计算量也相当可观。 一个技术是J.A.Robinson1965年提出的归结(resolution)法，归结法是命题演算中对合适公式的一种证明方法。为了证明合适公式F为真，归结法证明F恒假来代替F永真。归结原理是:设有前题LP和LR则其逻辑结论是PR，因为两个子句中含有一个命题的正逆命题(L，L)。若L为真L一定为假，P若为真，PR也为真。若L为假L为真，P若为真，PR也为真。这个推理把两子句合一(unification)并消去一对正逆命题，故归结也译作消解。归结证明的过程并称之归结演绎，其步骤如下: 1 把前题中所有命题换成子句形式。 2 取结论的反，并转换成子句形式，加入1中的子句集。 3 在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句(归结式)再加入到子句集。 4 重复3，若归结式为空则表示此次证明的逻辑结论是矛盾，原待证结论若不取反则恒真。命题得证。否则继续重复3。 例12-6 归结证明 若有前题 待证命题 取反得新子句 p1 QP PU p5 P p2 RQ p6 U p3 SR p4 US 取待证命题的反，得PU，它是连接的两个子句P，U，把它们加到前题子句集，为p5，p6。 归结演绎如下图: QP P p1-p5归结 Q RQ 再与p2归结 SR R 再与p3归结 S US 再与p4归结 U U 再与p6归结 矛盾 由于归结为空，则PQ得证。 由本例可以看出两个问题，第一，归结法是由合一算法实现的。所谓合一是找出行式匹配的两子句，将它们合一为归结式，相当于代数中的化简。 更广义的合一算法是找出两子句最通用的实例(对于谓词演算)即找出变量的实例，使两子句等价。例如: 公式1 公式2 广义合一 pp(a，b) pp(X，Y) X=a，Y=b; p(a，b)q(c，d) p(X，Y)q(Z，W) X=a，Y=b，Z=c，W=d q(p，g(X，Y)，X，Y) q(Y，Z，h(U，k)，U) U=Y=p，X=h(p，k) Z=g(h(p，k)，p) 第二是如果得不出矛盾那么归结法要无休止地做下去，中间归结式出得越多，匹配查找次数越多，每一步都做长时间计算，显然，要想出比这种原始归结法的更好办法，即利用切断(cut)操作，并对子句形式进一步限制的超级归结法(Hyperresolution)。12.2.5 Horn子句实现超归结 Horn子句是至多只有一个非负谓词符号的子句。这就等于说，通过谓词演算一个语句只包含一个蕴含运算符连接前题和结论，前题是由连接的几个谓词，结论就是单一的谓词符号。 Horn子句形式示例如下: PQSRT (12.6)其中只有一个非负谓词S，可作以下演算，先将S移向右方 SPQRT (12.7) 按德摩根定律 S(PQRT) (12.8) 即，则 S(P Q R T) (12.9)此即条件Horn子句，因为(12.9)的意义是if(PQRT) then S。显然，若S为空，则为无条件Horn子句，是一个断言(事实)。 超级归结实质上是将无条件Horn子句中的谓词符号和条件子句中的对应谓词符号合一。找出所有子句中变量的实例集，使每一条件子句为真。如果不满足则寻找新的实例(回溯算法)，如果满足了也要找出所有实例。 为了消去不必要的匹配以提高超级归结的效率，cut操作是必须的，它可以由程序员指定。当找到一个解之后不再搜索其它解。它本身是个无变元谓词，当执行到它时，不再回溯。cut操作也可用于分情形动作控制与fail(失败)谓词联用，12.4节还将举例。12.3 逻辑程序的风格 基于自动定理证明的逻辑语言，有其独特的程序设计风格，因为它不描述计算过程而是描述证明过程。例如，有一个问题: 对数组A按升序排序，我们怎样编逻辑程序呢？ 我们只好构造一个和A那样大的数组B，而且它是排好升序的，我们证明命题: “存在一个数组B它是数组A重排升序”为此，可以陈述更严谨一些: B是A的重排，当且仅当B的元素就是A的元素，且BiBj，ij。 于是，自动定理证明系统依靠环境，构造一个希望的解(B)，并证明它的存在。构造的办法不外乎匹配查找，例化或置换。证明是本题的主旨排序成了副产品！ 除了证明性风格而外，逻辑程序的第二个特点是描述性，请见下例: 例12-7 求平均成绩的逻辑程序 打开一分数文件scores，读入分数求和并用的数N除之得平均成绩。 average:-see(scores)， getinput (Sum，N)， seen (scores)， Av is Sum /N， print (Average = ，Av) getinput (Sum，N):-ratom (X)， not (eof)， getinput (Sum1，N1)， Sum is Sum1 + X， N is N11. getinput (0，0):-eof. 要使求平均成绩程序正确，必先打开(see)文件，从中得到输入，得N个数的总和记以N和Sum，关闭(seen)文件后求平均值Av，打印之。至于如何得到Sum和N，细化谓词getinput(_，_)。若要getinput成立，先读入一原子X(ratom是系统提供的谓词)。若未至文件末尾，读其余分数并求和。getinput是递归定义，并相应断言Sum ，N和Sum1，N1的关系。如果已至文件结束标记eof则输入为(0，0)。这个程序为求平均分数给出三条规则，号即子句的连接，意即所有子句为真，左端谓词才成立。 这个程序是用Prolog写的，我们虽未介绍它的语法，一经简单解释我们即可读懂该程序。它的风格是: 若要A成立，做B，做C，做D，再细化，若要B做出则要做P，做Q，做R，这与过程式语言自顶向下描述没什么差别，且比较自由，没有严格的顺序性。当然程序执行还需有事实的陈述，以及需求证明的查询。 逻辑程序第三个特点是大量用表和递归实现重复操作，递归特别利于谓词描述，我们只要能说明特征谓词的一步动作为真，其余如法炮制，程序就设计完了，上例中，getinput，读一数X，求和并令门数加1，其余照做。 关于表与递归联用的例子，见12.4节中Prolog的例子。12.4 典型逻辑程序设计语言Prolog Prolog是典型的逻辑程序设计语言，它基于一阶谓词逻辑，直接陈述问题世界的事实、规则和目标，非常简明清晰，所以人们称之为自文档的。Prolog的程序将逻辑和控制显式分离，它使程序正确性证明简化(只涉及知识，即逻辑部分)，程序的优化(只涉及控制部分)不影响程序正确性，是正交设计成功的范例。 12.4.1 Prolog的环境 Prolog很长一段时间都是交互式语言，它必须要有支持环境，即管理事实和规则的数据库，并为操纵它们提供元语言。小的数据库可以文件形式联接上，大的库在键盘上调用输入函数consult(filename)。一旦进入系统，即可查看库内容(用listing (predicate_name)或编辑它们(用retract(z)，还可以扩充数据库(用asserta(X)或assertz(X)。 联上数据库，程序员即可交互使用。查询、测试假设、断言更多的事实。为响应查询，Prolog系统执行它的证明过程并查找能满足查询变量的事实集。查找成功，写出找到的事实，若程序员满意并打回车键后，系统给出“yes”并显示新提示，如果数据库查完还未找到要的事实则给出“no”，并显示新提示。12.4.2 数据对象和项 Prolog的基本成分是对象(常量、变量、结构、表)、谓词、运算符、函数、规则。 常量 预定义有十进制整数，用户定义的常量叫原子，有小写字母开头的名字，Prolog是无类型的，程序是理论，可以对应多个模型(也可以没有)，因而原子在不同模型中是不同的对象。 变量 大写字母开头的名字。一个规则中同一变量名都将束定到同一对象上。符号_是变量的占位符，对于确有一变量但暂时不能指明时则补上_，一个规则中，_出现几次就束定几个变量。 结构 复合的数据结构，如记录类型可用函子(函数名)和括在括号中的成分(域)表给出: (，)例如，course (C_no，C_name，Teacher，Precno) 表 表是最频繁使用的数据结构。以方括号表示， (空表)，Head | Tail(递归定义的一般表)X,Y,Z(定长表)a，b | Z(表头为常量，表尾为变量Z)。表中元素叫项(term)可以是原子、表、空。 表的规格说明有两种形式，它们等效: X，Y，Z (x，y，(z， ) Head，Tail (Head，Tail) / 指出连接关系 开端表(open)是表尾长度可变的表。证明过程中，开端表可以和任何与其表头有相同常量的表匹配(合一)。 选择子函数head(X)，tail(X)可操纵表X返回表头或表尾变元。 谓词 预定义有=、=、=、=。用户可定义自己的谓词，以小写字母给出谓词名。机器是不理解谓词的语义的，它只知道匹配，所以，程序员应将谓词的意义记清并按它写程序。谓词带参数，即项，但参数不能是谓词、函数和关系。 运算符 预定义了整数运算符+、-、*、/和mod，可以写成标准的函数式+(3，x)也可以写成中缀形式 3 + x，使用中缀形式时有通常的优先级，算术等式还有一种is的形式，如X is(A+B)mod C，当Prolog处理这样的公式时，它用A，B，C的当前束定来执行这个计算其返回值束定于X，如is右边变量未束定值则返回错误。 从纯语法意义上Prolog的项什么都可以表示: :=|()| | 从语义角度，以下语法描述提供了处理时的语义概念: ( | | ) : - ， /*形如p或q(T，)的字面量*/12.4.3 Prolog程序结构 Prolog程序由子句组成，如前所述，子句模型是Horn子句。Horn子句本质上提供最基本的形式逻辑，即if_then条件推理，把多个子句放在条件中，当条件(即前题)均满足，then部分即结论。如果条件为空，即只有以谓词表达的结论，就是断言，即事实。条件子句即为规则。 为了简明，Prolog以 :- 代替 以 ，代替 and ，以 ; 代替 or ， ！代替cut。 和其它语言环境一样，系统配备了一批支持程序设计的预定义谓词(相当于其它语言的内定义函数)。 和其它语言一样，程序分两部分，定义和应用。程序定义该程序所需的公理集，即事实和规则。应用部分即查询，即写出待证的目标。整个程序是一证明系统。 (1) 事实与规则 Prolog程序先定义公理集，我们看下例: 例12-8 Prolog的规则和事实 条件子句(规则) pretty (X) :- artwork(X) pretty (X) :- color(X，red)，flower(X). watchout (X) :- sharp(X，_). 无条件子句(事实) color (rose，red). sharp (rose，stem). sharp (holly，leaf). flower(rose). flower(violet) artwork (painting (Monet，haystack_at_Giverny). 一般说来，一个谓词可以定义好几个规则来表达它。如同每个规则用or联接起来表达这个谓词，只有一个(第一个满足该谓词的)规则来解释对该谓词的调用。所以可以写出一系列的规则来表达通用的条件语义结构。 规则可以递归，这样就可以实现算法需要的重复。当然，递归谓词必须至少要有两条规则，一为归纳基础，一为递归步骤。(2)查询 Prolog中查询(query)是要求Prolog证明定理。因为提出的问题就是证明过程的目标，所以查询也叫目标(goal)。语法上查询是个由逗号分开的项表。语义上是同时满足的谓词，逗号即and。如果查询中没有变量，Prolog从已给定的规则和事实证明它，查询以?-开始，请看下例: 例12-9 Prolog的查询 ?- pretty (rose). yes ?- pretty (Y). Y=painting (Monet，haystack_at_Giverny). Y=rose. no ?-pretty(W)，sharp(W，Z) W=rose Z=stem no 第一个查询问”玫瑰美丽吗？” 它到例12-8的事实库中找出玫瑰是花，颜色是红的，满足第二条规则，故查询结果是yes。 如果查询中包含变量，Prolog的定理证明系统将找出满足查询的实例集合，查询中的所有变量均隐含具有量词$，也就是查询问的是否存在满足子句的对象。它给出一个就等待，当程序员键入 ; ，它就给出下一个直至没有，给出no。例12-9中的?- pretty(Y)查询，它找到例12-8 中第一条规则匹配，再找到最后一个事实匹配，找出Y=莫奈的油画吉缦尼的草堆。第二次再查，找出玫瑰。第三次查不出则给出no。 查询所包含的谓词项，它将自左至右依次处理。仅当任何一谓词项均不满足才夭折本次处理过程。在这种处理中，前项结果“好象”对后项有效和过程语言非常相似。 例12-10 最大公约数的欧基里得算法 最大公约数欧基里得算法可用三条规则描述: gcd (A，0，A). gcd (A，B，D) :- (AB)，(B0)，R is A mod B，gcd(B，R，D). gcd (A，B，D) :- (AB)，gcd (B，A，D). 其中A，B是输入参数，D是输出参数。第三条规则的执行，非常象if(AB) then gcd (B，A，D)。当测试(AB)为真时调用谓词gcd (B，A，D)。如果成功结果值束定于D。 第二条规则相当于执行了两次 if 测试，做一次赋值(将A mod