还剩18页未读，继续阅读
本资源只提供10页预览，全部文档请下载后查看！喜欢就下载吧，查找使用更方便
文本内容:
第章逻辑式程序设计语言12无论是命令式还是函数式程序都把程序看作是从输入到输出的某种映射当然命令式语言有时没有数据输出，但也要“输出”某些动作为了实现这种映射，程序要对数据结构实施某个算法过程，算法实现该程序功能算法又是以程序语言提供的控制机制实现计算逻辑所以，R.Kowalski说算法=逻辑+控制然而传统语言计算逻辑在程序员心里，隐式地体现在程序正文之中，为此程序正确性证明还要把它隐含的逻辑以断言形式地写出来自然人们会想到能不能把描述计算的理论基础命题演算和谓词演算直接变为程序设计语言这样，也许不必用求值来判定某件事情的真、伪，直接根据事实和规则判定真伪，“找出”解事实上，这是可行的，而且在人工智能的专家系统、语言理解、数据库查询中非常需要这种程序设计语言1970年诞生的Prolog长久不衰就是例证逻辑程序设计的基本观点是程序描述的是数据对象之间的关系，它的抽象层次更高而不限于函数映射关系关系也是联系，对象和对象、对象和属性的联系就是我们所说的事实事实之间的关系以规则表述，根据规则找出合乎逻辑的事实就是推理因此，逻辑程序设计范型是陈述事实，制定规则，程序设计就是构造证明程序的执行就在推理，和传统程序设计范型有较大的差异本章我们从逻辑程序设计理论基础，谓词演算导出逻辑程序语言的理论模型，并介绍逻辑程序设计语言Prolog的主要特征和实现要点谓词演算
12.1谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型，谓词演算在所有计算机理论的书籍中均有论述，本章仅简单复习，主要目的是引入术语
12.
1.1谓词演算诸元素用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质properties,以及对象间有些什么关系relations为了一般化还要有变量variable指明域上某个些对象，以及准确说明对象情况的量词quantifiers当然这个语言还需耍一些辅助的符号继承自初等集合论描述以公式Formulas表达，即描述一般命题的谓词谓词公式中各元素按一定逻辑规则变换即谓词演算predicate calculus以o下是谓词公式的示例mxp x一存在具有性质p的对象XVYpY一所有的Y,即域上任何对象，均具有性质pProlog是无类型的，程序是理论，可以对应多个模型（也可以没有），因而原子在不同模型中是不同的对象•变量大写字母开头的名字一个规则中同一变量名都将束定到同一对象上符号是变量的占位符，对于确有一变量但暂时不能指明时则补上,一个规则中，出现几次就束定几个变量•结构复合的数据结构，如记录类型可用函子（函数名）和括在括号中的成分（域）表给出〈函数名〉（〈成分〉，…，＜成分〉）例如，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返回表头或表尾变元•谓词预定义有=、\=、＜、=＜、＞、=＞o用户可定义自己的谓词，以小写字母给出谓词名机器是不理解谓词的语义的，它只知道匹配，所以，程序员应将谓词的意义记清并按它写程序谓词带参数，即项，但参数不能是谓词、函数和关系•运算符预定义了整数运算符+、-、*、/和mod,可以写成标准的函数式+（3,x）也可以写成中缀形式3+x,使用中缀形式时有通常的优先级，算术等式还有一种is的形式，如X is（A+B）modC,当Prolog处理这样的公式时，它用A,B,C的当前束定来执行这个计算其返回值束定于X,如is右边变量未束定值则返HI错误从纯语法意义上Prolog的项什么都可以表示＜项＞::=＜常量＞|＜变量＞|＜结构＞|（＜项＞）|＜表＞＜后缀算符〉|＜项＞＜中缀算符＞＜项＞|＜,项＞＜前缀算符》从语义角度，以下语法描述提供了处理时的语义概念:〈程序〉f〈子句〉〈子句〉f（〈事实＞|＜规则＞|＜查询＞）〈事实〉一〈结构〉〈规则〉一＜头＞:Y体＞〈头〉一＜结构〉＜体＞-＞＜目标＞，〈目标〉〈目标〉一/*形如p或q（T,…，）的字面量*/
12.
4.3Prolog程序结构Prolog程序由子句组成，如前所述，子句模型是Horn子句Horn子句本质上提供最基本的形式逻辑，即ifjhen条件推理，把多个子句放在条件中，当条件（即前题）土匀满足，then部分即结论如果条件为空，即只有以谓词表达的结论，就是断言，即事实条件子句即为规则为了简明，Prolog以‘-代替‘一以，代替，and，，以「代替，r」！代替cut和其它语言环境一样，系统配备了一批支持程序设计的预定义谓词相当于其它语言的内定义函数和其它语言一样，程序分两部分，定义和应用程序定义该程序所需的公理集，即事实和规则应用部分即查询，即写出待证的目标整个程序是一证明系统1事实与规则Prolog程序先定义公理集，我们看下例例12-8Prolog的规则和事实条件子句规则pretty XartworkXpretty XcolorX,red,flowerX.watchout XsharpX,_.无条件子句事实color rose,red.sharp rose,stem,sharp holly,leaf.flowerrose.flowerviolet artworkpainting Monet,haystack_at_Giverny.一般说来，一个谓词可以定义好几个规则来表达它如同每个规则用联接起来表达这个谓词，只有一个第一个满足该谓词的规则来解释对该谓词的调用所以可以写出一系列的规则来表达通用的条件语义结构规则可以递归，这样就可以实现算法需要的重复当然，递归谓词必须至少要有两条规则，一为归纳基础，一为递归步骤2查询Prolog中查询query是要求Prolog证明定理因为提出的问题就是证明过程的目标，所以查询也叫目标goal语法上查询是个由逗号分开的项表语义上是同时满足的谓词，逗号即and如果查询中没有变量，Prolog从已给定的规则和事实证明它，查询以开始，请看下例例12-9Prolog的查询-pretty rose.yes-pretty Y.Y=paintingMonet,haystack_at_Giverny.Y=rose,no-prettyW,sharpW,Z W=rose Z=stem no第一个查询问玫瑰美丽吗？”它到例12-8的事实库中找出玫瑰是花，颜色是红的，满足第二条规则，故查询结果是yes如果查询中包含变量，Prolog的定理证明系统将找出满足查询的实例集合，查询中的所有变量均隐含具有量词1也就是查询问的是否存在满足子句的对象它给出一个就等待，当程序员键入；，它就给出下一个直至没有，给出no例12-9中的-prettyY查询，它找到例12-8中第一条规则匹配，再找到最后一个事实匹配，找出丫=莫奈的油画《吉缰尼的草堆》第二次再查，找出玫瑰第三次查不出则给出no查询所包含的谓词项，它将自左至右依次处理仅当任何一谓词项均不满足才夭折本次处理过程在这种处理中，前项结果“好象”对后项有效和过程语言非常相似12-10最大公约数的欧基里得算法最大公约数欧基里得算法可用三条规则描述gcd A,0,A.gcd A,B,DAB,B0,R isA modB,gcdB,R,D.gcd A,B,DAB,gcd B,A,D.其中A,B是输入参数，D是输出参数第三条规则的执行，非常象ifAB thengcd B,A,Do当测试AvB为，真时调用谓词gcd B,A,D如果成功结果值束定于D第二条规则相当于执行了两次if测试，做一次赋值将A modB束定于R,再做一次谓词匹配，结果值束定于D
12.
4.4封闭世界内的演绎过程查询建立了演绎过程的目标，它以项的逻辑“与“连接给出Prolog逐一满足查询中的各个子目标子目标也可以是含变元的谓词，它首先到数据库中查变元个数目相同的规则头，如果找到，则暂时列出匹配的变元实例接着处理规则体的另一个子目标看找出的实例能否满足新的子目标，如果成功，继续匹配下一个子目标，直到所有子目标均满足因为各子目标是“与”的关系如果有某个子目标查遍数据库也找不到能满足的事实，该子目标失败，但不等于整个目标的失败，它就回溯到上一个子目标重选事实继续匹配这种回溯的执行过程和例题我们在第742节⑵中已介绍过了即使是整个目标最后失败，也不等于这个目标追求的命题是否定的,因为限于数据库存放的规则和事实有限，它是“封闭世界假说”之下的失败回溯是在树行模型之下以递归下降法自动进行的，也就是说，Prolog实现程序计算的算法相对固定程序员也就没有必要对程序作出什么显式的控制，它的程序控制是隐式的提高程序质量就在于程序员如何安排一个规则内条件的次序了，各规则之间的次序并不重要这是因为它采取的是深度优先，穷举搜索，不到整个数据库按规则子目标所有可能的组合全部查完是不能说出fail失败的
12.
4.5函数和计算Prolog解题是模型一个系统，从输入开始以某种给定的形式希望能导出输出对于其它语言这洽好是定义一个从输入到输出的函数，设计算法安排对数据结构的加工步骤，做过程式程序设计Prolog是公理化的语言，它只以公理化的方式描述输出结果，并用证明过程代替传统的计算过程，即它找出数据库中具有和所希望输出的对象有同样性质的对象，证明它们是一致的然而，作为一个程序设计语言它也要有最低限度的计算1函子完成逻辑设计中的计算Prolog为整数预定义了五种运算符，它们都是计算函数，所以，函子以结构形式出现，如中缀表示前缀表示X+Y*Z+X,*Y,ZA-B/C-A,/B,C中缀和前缀表达等效，前缀表达虽可按谓词理解，两变元具有+、-、*、/、mod关系，但它不求真值而有求值结果，所以，它不是谓词仅仅是一特殊的结构函数名V变元，…，〈变元〉函数求值的的结果一般通过谓词is〈变元〉,表达式封束定到变元上，也可以写成中缀它的意思是表达式复合的函子结构计算的值返回到变元之中，该变元以表达式的值实例化所以，若要做计算，一条规则中至少要有一个is子句，前述最大公约数程序的第二条规则gcd A,B,D;-AB,B0,R isA modB,gcdB,R,D.其中A modB就是计算余数的，计算后以返回值例化R,再代入后边的递归谓词用户定义的带数值计算的谓词，必须增加一个存放返回值的变量如求最大公约数的欧基里德算法是两数变元辗转相除，只要两个变元上式gcd A,B,D变元有3个，D就是为了返回值，是gcd的输出变元把函数改写为约束，很容易写出program程序，请看下例12-11求斐波那契数的Prolog程序斐波那契函数以下述公式生成以下数列1,1,2,3,5,8,13,21,…FibO=1Fib⑴二1Fibn=Fibn-1+Fibn-2编制Prolog程序时这样分析第
一、二式是事实也是公理，把结果值作为变元照写第三式说明，若n为斐波那契数，n-1和n-2的斐波那契必须成立，且这两个数之和是n的斐波那契数，nk于是有Prolog程序Fib0,
1.Fibl,
1.Fib n,fFibm,g,Fibk,h,m isn-1,k ism-1,f isg+h,nl.当有查询-Fib5,f时,f返回82逻辑程序的算法表达算法怎样用公理表达呢？我们拿一个最典型的Quicksort分类程序讨论分类在表上进行我们可以按快速分类写出它的公理quicksort未分类表，分类完的表从未分类表拿出第一元素，以它为基准，分成两个表，L1]quicksort小表，分类完小表，
[2]quicksort大表，分类完大表，[3Jappend分类完小表，基准元素和分类完大表，分类完总表
[4]这样把快速分类的总目标变成了四个子目标，第
二、三个子目标显然清楚，继续递归分类第四个是以连接谓词append把它们连成一个分完类的总表输出第一个子目标是将一个表分解为两个表，我们细化如下先构造一个“劈分”谓词，split基准元素，未分表，小于基元的表，大于基元的表前两变元输入，后两个输出谓词意义明显，但算法过程还没说清如何分于是，我们从待分类表拿出第一元素，若小于基元素放入小表，否则放入大表，接着再重复直至都成为空表最后的Prolog代码如下例:例12-12快速分类的Prolog代码rl split_,[],[]UD.r2split Pivot,[Head|Tail],[Head|Sm],LgHeadPivot,split Pivot,Tail,Sm,Lg.r3split Pivot,[Head|Tail],Sm[Head|Lg]PivotHead,split Pivot,Tail,Sm,Lg.r4quicksort[],[].r5quicksort[Head[]],Head.r6quicksort[Pivot|Unsorted]AllSorted:-split Pivot,Unsorted,Small,Large,quicksort Small,SmSorted,quicksortLarge,Lgsorted,append SmSorted,[Pivot|LgSorted],AllSortedo规则U,r4虽然是递归到头的一条公理，但也起到声明数据结构的作用请注意从表中取出元素的技巧，人为写上[Head|Tail]它将表的第一元素束定到名字Head,其余部分束定到Tail名字上，由此分出Pivot,Head直至递归分完规则r2,r3的V，谓词，是实现条件选择很典型的方法，规则r5是处理只有一项的表的特殊情况3逻辑和控制分离Prolog无通常意义的控制结构，也就是该程序动作次序显然也有和计算的子句逻辑没有必然的关系例如，把例12-12中，r4,r5,r6写在rl,r2,r3前面并不影响本程序的执行结果如有查询它总是从第一个规则到最后一个规则查找匹配但是，写得好与不好却影响效率为了效率总是把易于找到匹配的规则写在最上面控制优化可以大为改善效率程序逻辑和控制的无关性决定了逻辑程序设计方便易行先分析程序逻辑，解决正确性问题再分析程序效率，优化控制，使程序完善但要注意，一味追求高效会丧失易读性例如，例12-12中，rl,r4是到达递归边界的规则，完全可以放在r3,r6之后但rl,r4有表达数据结构的功用，如rl是有一个变量，三个表作变元的谓词公理一上来就是r2倒反看不清晰所以，例12-12是递归逻辑程序惯用的写法
12.
4.6cut和not谓词如前所述，超级归结依赖cut割断操作使归结证明人为截止，因为Prolog的归结模型只能完整地证明正命题，是否有解无法判定如果明知继续下去没什么意思了就人为截断显然，一旦提供了这个机制，它是一双面刃，用得不好会破坏证明系统的完整性1安全cut非形式解释cut,它如同一篱笆，由程序员任意置放在规则之中，以停止无意义的回溯例如，有如下规则P:-Q,R,S,!T,U,V证明系统首先查找Q、R、S的条件合一，Q满足R不满足则回溯改Q,如此下去直至S也满足，控制经！传到T,此时满足Q、R、S的变量实例均予冻结回溯只能在T、U、V之间，所有条件均满足本规则成功，否则失败，并不再回溯修改！号左边变量实例所谓安全cut即不可能导致可证明的目标失败，且大为改善效率例12-13安全cut示例求1到N的整数之和rl sum_toN,1N=1,!.r2sum_to N,RN1is N-l,sum_toN1,Rl,R isRl+N.当有查询-sum_tol,X〃匹配rlX=1;〃打7号由于有！不致无限查找第2个no-sum-to6,X//匹配M失败，匹配r2连续r2X=21;//直至成功，打号也不再找no其实本例rl写作事实sum-tol,
1.也可以求出，但本例写做规则，它就要找右端子句匹配,当用户键入；号时，如果没有！，它将无限运行以查找第二个满足sum」ol,X的解实际是不可能找到的2cut实现not操作在归结证明系统中，一般要求规则和查询都用非反条件，尽管not操作完全可以代替cut且程序行文中可读性更好，但用not时必须仔细，因为它是cut实现的，其定义如下rl notX:-X,!,fail.r2not_.其语义是若X为，假，则条件notX成功若X成功，notX失败其推理过程是•若X为假，匹配在未达到！时已失败，则匹配规则r2,由于r2什么变元都可以且总为成功，所以，notX是成功的•若X为真，匹配rl后，X为真，控制通过！传到fail,则rl失败于是回溯到！过不去,只好失败由于用了!就地失败，它不再匹配r2,故notX为假正是由于这个原因，谓词p和notnot p求值结果不能保证一样，有时notp和notnot p求值结果倒是一样的，以下是not谓词出毛病的例子例12-14不可靠的not谓词假定一规则test有以下定义test S,TS=T.运行以下查询时有-test3,5no-test5,5yes-not test5,5no-testX,3,R isX+
2.X=3R=5-not nottest X,3,R isX+
2.!error inarithmetic expression:not anumber由于第二次not外部的求值时用到上例规则rl,其中X是nottestX,3的结果值，故X+2不是数加2这个问题原因在于子句逻辑的不可判定性即我们有时可以证明理论T,有时可以证明它的反，notT,有时两者均不可证明如果是后者，说明定理只适用于某些模型而对另一些模型不能用我们不能因不能证出T为真而断言T为假，但Prolog确是这样，不能证明T为真则断言notT成功所以，使用not要特别小心3不安全的cut在人工智能领域的启发式策略中，证明树有时极其庞大，程序员就要割掉部分明知无解的推理树，有时由于机器太慢，树虽不大，时间太长还非这样做不可但程序员稍有疏忽就会酿成大错，把仅有的解都割了去这时就破坏了证明完整性cut使我们处于两难的境地，它的高效是以风险为代价得到的，如同60年代goto技巧对非结构化程序只要模型是超级归结，cut的两面性是不可以解决的评价
12.5PrologProlog提供一种证明风格的声明式程序设计，推理清晰，概括能力强，程序和数据没有明显分离在复杂的人工智能程序中，简明的表达有利于程序员写出好程序特别是逻辑和控制分开的正交性简化了正确性证明，因为程序员只需关注证明的逻辑部分，而优化控制提高效率并不影响证明的正确性Prolog程序具有自文档性，由于论域直接就是问题域，谓词清晰描述了论域对象的特征与关系，而实现是单一的递归下降匹配算法没有影响描述的过多实现细节，自文档性好是必然的它的非过程性和没有“隐藏的语义”使程序更具有安全性即程序员控制整个程序比较方便，且不需了解更多实现细节在程序员尚不清楚如何组织数据和计算过程的应用中，Prolog有极大优势，因为它证明的是后果而不是过程，且对程序的顺序性要求不严只陈述应如何如何，要如何如何，并未详细安排计算过程正是由于非过程性，它也成为7电在的并行程序设计语言的候选者，所以，当今在高度并发的连接机（Connection Machine）Jb,采用Prolog作为软件语言仅管由于编译技术的改进（有了编译的非解释型Prolog）,Prolog程序的效率由于依靠参数束定的合一匹配，它的效率仍不及传统过程语言也正是由于它的声明性质，程序员在优化算法时作用有限因为它的基本推理算法是确定的，且程序正文看不出计算过程，以不变的递归下降算法应万变，当然就没有过程式语言设计精巧算法效率高此外，Prolog的基本推理规则基于最简单的形式逻辑，if_then_else,所以它的功能过程式语言很容易实现，效率大为提高，只是表达不如Prolog清晰，所以，近年专家系统的开发工具不少以C语言实现，这样做还利于得到C语言环境工具的支持第二个不足是，一般复杂的大型系统一开始很难作为证明系统开发，程序不大运算量惊人而Prolog本身也只有局部量，天生来也不是大型软件开发的工具因此，Prolog只能作为逻辑程序设计的独枝存在，解决大型应用多范型语言是个出路小结
12.6•逻辑程序设计的基本观点是程序描述论域上对象的属性及其相互关系，对象和对象、对象和属性及其相互关系对象和对象、对象和属性的连系就是事实，事实之间的关系以规则表述根据规则找出合理的事实叫推理•谓词以公式表达对象及对象间的关系，谓词公式中的常量、变量、函数、谓词、查询按一定逻辑规则的变换（等价置换）即谓词演算•子句逻辑是经典逻辑的特例，任一谓词演算公式均可化为或连接的子句的集合（子句内部由与连接）•证明系统是应用公理演绎出定理的合法演绎规则的集合，公理即证明的前题是事实和规则的集合演绎也叫归约，是证明系统中合法规则的一次应用演绎的结果是从前题（公理）导出逻辑结论证明是一个语句序列，证明过程是要么使每个语句演绎成公理，要么演绎为前此导出的定理，反驳是反向证明一个语句是矛盾•一个语句若能从公理推演出来称定理，定理集合称理论理论不含相互矛盾的定理•理论要借助模型得到语义解释，模型即特定论域上的约定一般说来，一个理论可以有多个模型•命题演算是谓词演算的特例谓词演算对于真命题的证明是完整的，但是否能找到证明是不可判定的不存在，也不可能找到一个算法验证非真命题•经典逻辑从前题到结论的推理一般采取穷举证明技术，在实现上效率是根本问题，因为各公理组合实现的推理树往往是天文数字，即证明系统的组合爆炸问题•基于子句逻辑的归结证明技术以归结一合一方法证明反命题恒假来说明命题为真归结原理是将两个含有正逆命题的子句消解为更简单的归结式，如果归结得不出矛盾要无休止地归结下去直至空间耗尽反之原命题得证•对命题形式进一步限制（用Hom子句）和利用切断技术（cut操作）是能付诸实用的超级归结法它是Prolog的理论模型•逻辑程序设计的风格不是描述计算过程而是证明过程一般构造一个希望的解，证明它就是所希望的解构造过程就实施了计算第二个特点是描述性第三个特点是大量利用表的数据结构和递归•Prolog程序公理部分是事实和规则（无条件和条件子句），查询是求证目标它在封闭世界（限于规则和事实库）完成证明的演绎过程回溯是实现各子目标同时满足的唯一方法•子句逻辑的不可判定性要求规则和查询用非反条件，且慎用not操作•Prolog的优点是自文档性、非过程性、逻辑表达能力强描述性使程序清晰、具有潜在的并行性Prolog的缺点是只适合较小程序计算效率不高习题
12.1试述逻辑程序设计的基本风格与过程式程序函数式程序的同异答无论是命令式还是函数式程序都把程序看做是输入到输出的某种映射，为了实现这种映射，程序要对数据结构实施某个算法过程，算法实现该程序功能而算法又是以程序语言提供的控制机制实现计算逻辑但这种逻辑是在程序员心里，被隐式体现在程序正文中，为此，程序正确性的证明还要把它隐含的逻辑以断言形式地写出来而逻辑程序设计的范型是陈述事实，制定规则，程序设计就是构造证明程序的执行就是在推理它们的共同之处在于程序描述的都是数据对象之间的关系，只是逻辑式程序设计抽象层次更高，而不仅限于函数（映射）关系
12.2试述归结证明的基本思想为什么要超级归结？答归结法是命题演算中对合适公式的一种证明方法其基本思想为为了证明合适公式F为真，归结法证明F恒假来代替F永真归结原理是设有前提LVP和7LVR,则其逻辑结论是P VR,这个推理把两个子句合并消去一对正逆命题将新的子句再加入归结子句集中，继续归结若最终归结式为空则表示此次证明的逻辑结论是矛盾，原待证结论若不取反则恒真，命题得证使用超级归结的原因是由以上思想可知，如果得不出矛盾，那么归结法要无休止地做下去，中间归结式也越多，匹配查找次数越多，每一步都做长时间计算于是想出比这种原始归结更好的办法，即利用切断操作，并对子句形式进一步限制即为超级归结法超级归结实际上是将无条件Horn子句中的谓词符号和条件子句中的对应谓词符号合一
12.3何谓变量例化？在演绎过程中变量如何实例化？
12.4何谓命题演算，谓词演算，它们的同异
12.5谓词与关系的同异？答关系是泛指事物之间的相互关系，从逻辑程序设计的观点来看，关系包括事实（即对象和对象，对象和属性的联系）及规则（即事实之间的关系）两种，指数据对象具有的性质及不同对象的联系谓词是关系的特例，是因公式表达的对象间的关系，即某种事实，是表征某种对象性质的符号
12.6以下限定量词是否为真？若为真取反（）
[1]V YevenY（）
[2]3X evenX
[3]VXX=X+0
[4]3X VYX=Y+l
[5]VX3YX=Y*
112.7公理和理论有何不同答公理是用谓词演算公式来描述的事实理论是从某一公理集合导出的所有定理集合，所以理论是公理的演绎结果
12.8定义一个理论举出它有多个模型
12.9何谓证明系统？何谓反驳？证明系统是应用公理演绎出的合法演绎规则的集合，反驳是一个语句的反向证明，它证明一个语句是矛盾的，即不合乎规定的公理
12.10试证Horn子句的完整性
12.11给出事实和规则flower crocus,spring,white.flower voilet,spring,blue.flower iris,summer,blue.flower rosr,summer,red.flower marigold,summer,orange.tree holly.colorF,C:-flower F,S,C.，color Tgreen:-treeT.prettyF:-colorF,red.prettyF:-colorF,blue.grows X:-treeX.growsX:-flower X,Y,Z求能与以下子句合一的实例化集合
[1]flower F,spring,Y,pretty F.
[2]flower F,summer,Y,prettyF.
[3]flower E,Y,orange,prettyE.
[4]grows X,prettyX.答
[1]flower F,spring,Y,pretty FF=voilet,Y=blueNo
[2]flowerF,summer,Y,pretty FF二inis,Y=blue,F=rose,Y=redNo
[3]flowerE,Y,orange,prettyENo
[4]grousx,pretty xx=violetx=inisx=rose,No
12.12用prolog写出完整的矩阵相乘程序domainsVt=integer*Ut二integer*predicateform VectorVt,integerform MatrixUt,integer,integerMatrinx MultiUt,Ut,UtVmJfultiVt,Ut,UtVector MultiVt,Vt,integerMainfun UtClavsesformVector[H|T],X:-0readist H,form VectorT,X-l,formVector[],
0.Matrixjlulti[H|T],L2,[H3|T3]-Vm_MultiHl,L2,H
3.Matrix_MultiTl,L2,T
3.Matrix_Multi[],_,[].Matrix_Multi_,[],[].Vm_MultiLl,[H2|T2],[H3|T3]-Vector_MultiLl,H2,H
3.Vm_MultiLl,T2,T
3.Vm_Multi[],_,[].Vm_Multi_,[],口.Vector Multi[Hl|Tl,[H2|T2],[H3|T3]-S1=H1*H2,Vector MultiTl,T2,S2-S=S1+S
2.Vector Multi[],_,
0.⑴Mach fun-Readint X,ReadintY,X0,Y0,form MatrixLI,X,Y,form_MatrixL2,X,Y,Matrix_MultiLl,L2,L.
12.13总结prolog中cut的用法，怎样是安全的？怎样是不安全的？
12.14Prolog程序的模块性体现在哪些方面？
12.15写一个C语言的快速分类程序，比较例12-12的Prolog程序，你能得出什么结论int k
[30]Voidmain{int I;forI=0;K30;I++Scant C6%d,\k[I];Quick_sort0,30;，forI=0;I30;I++printf%d\n k[I];void quick_sortint m,int n{int temp:i,j,t;VXmYX=2*Y—对于所有的X都可以找到Y,其值为X的一半，其中的逻辑连接=”是中缀表示等效于=X,2*丫谓词公式各元素符号表示法在各教程中不尽相同，谓词演算的表示由以下元素组成1公式由一组约定的符号组成的序列，它包括常量指明域上的某个对象、变量域上任意对象、逻辑连接指明对象状态及对象间的关系，有数量上的,、＞=、=、＜、＜=、/=和逻辑上的V、
八、
1、
一、＜=＞、命题函数指明对象间的函数性质，谓词对象间约定的关系,量词逻辑连接的一种，指明对象状态一阶谓词演算系统中公式里不得嵌套谓词2常量指明论域universe ofdiscourse上的对象，也是数学对象通常一个逻辑系统要引入多个论域，一般有十进制整数域、真值域、字符域，可用不同的符号表达有区别的域常量可以看作是退化了的函数没有变元常量以字面量或小写字母表示3变量可束定到特定域上某个范围的对象上，在演算归约期间它可以例化为具体对象常量对象，变量是数学意义的，一旦束定整个演算期间不变，变量以大写字母表示4函数表征对象具有的映射关系，函数带参数，从变元域映射到结果值域可以是不同的域变元一般是常量、变量、函数结果值、变元在语法上都叫项term函数以小写标识符表示5谓词表征对象某种性质的符号，谓词带上一到多个变元对象即为断言assertion它断言这些对象具有谓词所指性质，谓词形如函数，当该变元确实具有所指性质时隐含真值，否则为假当谓词应用到的变元是常量或已被束定的变量上时，就叫做句子sentence或命题proposition,查询时能返回真假值当谓词应用到变量或包含变量的项上时，它依然是谓词但不能形成句子，只有例化才能判定真伪，形成句子谓词变元的个数称作目arity,故有单目、N目谓词之称例12-1N-目谓词的例子谓词目含义oddX1X是奇数fatherF,S2F是S的父亲divideN,D,Q,R4N除D得商Q和余数R谓词例化结果值odd2Falsedivide23,7,3,2Turefather changshan,changpingTruedivide23,7,3,N N未例化，不知真假6量词变量可以代表域中任何对象，量词可以指定某种集合，量词有两个，一为全称V、一为存在才，量词限定的变量名作用域是整个公式，它说明同名变量有些谓词经量词修饰后即没有变量，可成句子或命题例12-2量化谓词量化谓词VXoddX结果值BXoddX FalseVXX=2*Y+1-odd XTrueVXBYdivide X,3,Y,03X3Ydivide X,True3,Y,03XVYdivideX,3,Y,0FalseTrue,如X=3,Y=1False,但很难证明i=m;j二n;temp=k[i];do{do i++;whiletempk[i]i!=ndo j—;while tempk[i]j!=mifijt=k[i];k[i]=k[j];k[j]=t;}while ijt=k[m];k[m]=k[j];k[j]=t;quick_sortm,j-1quick_sortj+1,n;}.结论prolog解题是模拟一个系统从输入开始从某种给定的形式希望能导出输出对于其他的语言，这恰好是一个从输入到输出的函数设计算法，做过程式程序设计，prolog是公理化的语言，它是以公理化的方式描述输出结果，并用证明过程代替传统的计算过程证明一个全称谓词是比较难的，因为最可靠的证明方法是枚举例证，这对于论域大的公式就很困难了于是采取反证的方法，如能找出一个反例则原公式也是命题为假，这种假言推理的表示恰好将全称改为存在，全称量化的谓词取反例12-3量化公式取反量化谓词VXoddX3Xnot oddX
[1]3XoddX VXnotoddXVXX=2*Y+l-oddX3XnotX+2*Y+1-oddX3XnotX=2*Y+lor oddX3XX=2*Y+land notaddXVX3Y divide X,3,Y,03XVY notdivide X,3,Y,03X3Y divideX,3,Y,0VXVY notdivideX,3,Y,03XVY divideX,3,Y,0VXBYnot divideX,3,Y,0第［4］、［5］行实际就是通过谓词演算得到更加直观的等价式，因为局部not是极容易找出例证的7逻辑操作and,or,not,f蕴含=全等是最基本的逻辑运算符，然而，最本质的有andA,orV,not-i就够了，如A-B=not Aor B=-iA VBA=B=A andB ornot Aand notB=A AB V-iA A-iB命题演算即原子命题通过逻辑连接，等价变换，达到验证命题真理性的目的谓词演算以准确的谓词描述论域上对象的逻辑关系，通过等价变换达到证明一般命题真理性的目的命题演算是谓词演算的特例
12.L2谓词演算的等价变换等价变换即演绎推理，不同的逻辑连接有其等价变换的规则命题，谓词演算规则可以查有关文献本节演示一般谓词公式变换为子句的实例‘卜号为“可推出”［1］以八，v,「如上例消除f、二符号［2］化为前束范式，消除最外的「符号，即否定符号内移-3XpX pX［3］利用斯柯林变换消去存在量词如VX3Zc Z,X A bX|-VXc z,X AbX再如:VXaX AbX V3YcX,Y|-VXa XAbX V cX,gX
11.1其中gX是对任何一X可得到存在的Y［4］消除前束范式的全称量词既然设定所有变量均为全称，要不要符号都是一个意思，即都要搜索全域才能证实该变量，则1L1式为|-aX AbXVcX,gX
11.2［5］利用分配率PVQ/\R=PVQ八PVR化成合取范式，1L2式成为卜aX VcX,gX AbXVcX,gX
11.3经过以上变换任何一复合公式均可成为如下形式F=C1AC2A…Cn
11.42rLrL[fl]]]]1J45678且其中Ci称为子句，如果以，，代替，A，，且其次序无关可表达为集合形式F=CL C2,,Cn其中Ci内部没有其它逻辑连接符号，只有W若以/代，▼则有Ci=LI VL2V-Lv=Ll;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从公理集合中导出定理集称之为理论，有了理论我们要解释它的语义必须借助某个模型modelo因为形式系统只是符号抽象，借助模型我们可为每个常量、函数、谓词符号找到真理性的解释即定义每个论域，并表明域上成员和常量公理之间的关系公理的谓词符号必须派定为域中对象的性质，函数派定为对域中对象的操作不一致的理论就没有模型，因为无法找到同时满足相互矛盾定埋的解释公理集合一般情况下只是定义的部分偏函数和谓词，是问题域的一个侧面所以能满足该理论的模型往往不止一个如，下例是一“间隔数理论”为找出该理论的一个模型，先找一个论域，它必需要能解释给出的三个公理，常量T和2,函数符中，谓词interval例12-4一个最简单的理论公理集VXintervalX-not interval X+l VXnotinterval X+l-intervalX al2=1+1a2从间隔数公理可导出定理a3VXinterval X^intervalX+2VXinterval X+2f intervalXtlt2如果我们设定论域是整数，则T,2可解释为整数一和二，且中就是整数加符合公理a3,即加函数谓词interval间隔数在整数域上显然有两个子域odd奇数、even偶数都能够满足如果奇数都是间隔数，在本理论中偶数定然不是反之，奇数不是既然我们论述在整数域上,对任一整数我们倒反不能确定它是否为间隔数了，间隔数理论不能证明interval©,也不能证明notinterval为真命题这就是Milbert讨论过的可判定性decidability问题1936年Church和Turing证实谓词演算可判定性问题是没有解的，因为不存在也不可能证明一个算法能正确地验证非真命题对于真命题即使有算法过程存在，也要在无限长的时间才能做完证明然而，一旦我们断言interval或interval^是真命题，我们立刻可通过演绎证明按这个理论写出的每一个谓词为真这就是Goedel和Herbrandl930年证实的谓词演算具备的完整性completenesso它可以证明该理论所有模型里的每一语句为真谓词演算可用来开发每一逻辑真命题的形式证明系统甚至存在机械的证明方法Gentzen1936证明技术从谓词演算具有完整性，理论上可作出自动生成程序并证明按公理集合建立的任何理论,它们是公理集合的逻辑结论但实际做起来，要找到切题的证明如同大海捞针，效率难以容忍即使把问题限制在证明单个命题，关键仍然是效率如果我们从公理出发做出每一个步骤，在新的步骤上仍然要查找每一个公理找出可能的推理如此下去就形成一个庞大的树行公理集，每层的结点都是表示一个公理的语句，其深度和宽度随问题和最初给出的公理而定，一层一步骤，N层的树就是N步推理对于自动定理证明程序，只有穷举每条可能的证明步骤才能说它是完全的然而，穷举完所有路径马上遇到组合爆炸问题，无论是深度优先还是广度优先，百步演绎可能的路径数都是天文数字以下是证明路径示例例12-5试证65534是个好整数设谓词goodX表示X是好整数谓词PowtwoY,Z表示2的Y次方为Z,显然，powtwo0,1是事实若A是好整数与2作整数运算之后结果仍应为好整数若2P=A且p为好整数则A也是好整数，2P+=2*A也都是显然的公理所以有公理fl goodOf2powtwo0,1r3good A-2-good Ar4goodA+2-good Ar5good A*2-good Ar6goodApowtwoP,A,goodP七条公理中有两个事实5条规则,si good2fl和r4s2good4si和r5s3powtwol,2f2和r7s4powtwo2,4s3和r7s5powtwo3,8s4和r7s6powtwo4,16s5和s7s7good16s2,s6和r6s8powtwo5，32s6和r7s9powtwo6,64s8和r7slO powtwo7,128s9和r7sll powtwo8,256slO^Dr7sl2powtwo9,512sll和r7sl3powtwo10,1024§12和〃sl4powtwo11,2048sl3^r7sl5powtwo12,4096S14和r7sl6powtwo13,81926si5和17sl7powtwo14,16384§16和力sl8powtwo15,32768§17和17sl9powtwo16,65536sl8^r7s20good65536s7,sl9和r6s21good65534s20和r3得证r7powtwoP+l,A*2-powtwoP,A这个证明人工花了21步，机器怎以么下会证知明道过？程它:必须把每个事实和已证明的定理逐个代入到这5个规则中验证得出新的定理，每得出一个powtwop+l,A*2后要像第七步s7和第二十步s20一样把基和值分出来，连试探到计算至少要操作72L
4.7173X10I7次
4.72亿亿次
12.
2.4归结定理证明不加限制地写出公理，穷举证明显然不是一条自动证明的出路因为要机器自动查匹配演算到预期的合适公式，代价是极大的于是对谓词公式的写法加以限制，即在
12.
1.2节把任何公式化为子句逻辑的办法可以省去一大片的归约演算，即使如此，穷举证明计算量也相当可观一个技术是J.A.Robinson1965年提出的归结resolution法，归结法是命题演算中对合适公式的一种证明方法为了证明合适公式F为真，归结法证明「F恒假来代替F永真归结原理是设有前题LVP和「LVR则其逻辑结论是PVR,因为两个子句中含有一个命题的正逆命题L,iLo若L为真「L一定为假，P若为真，PVR也为真若L为假「L为真，P若为真，PVR也为真这个推理把两子句合一unification并消去一对正逆命题，故归结也译作消解归结证明的过程并称之归结演绎，其步骤如下
[1]把前题中所有命题换成子句形式[21取结论的反，并转换成子句形式，加入⑴中的子句集[31在子句集中选择含有互逆命题的命题归结用合一算法得出新子句归结式再加入到子句集［4］重复［3］,若归结式为空则表示此次证明的逻辑结论是矛盾，原待证结论若不取反则恒真命题得证否则继续重复［3］例12-6归结证明若有前题待证命题取反得新子句pl QV「P p5Pp2RV-iQ p6Up3SViRp4-nUViS取待证得PAU,它是八连接的两个子句P,U,把它们加到前题子句集，为p5,命题的反,p6o归结演绎如下图:pl-p5归结再与p2归结再与p3归结再与p4归结再与p6归结矛盾由于归结为空，则得证由本例可以看出两个问题，第一，归结法是由合一算法实现的所谓合一是找出行式匹配的两子句，将它们合一为归结式，相当于代数中的化简更广义的合一算法是找出两子句最通用的实例对于谓词演算即找出变量的实例，使两子句等价例如公式1公式2广义合一ppa,b PPX,Y X=a,Y=b;pa,bAqc,d pX,YAqZ,W X=a,Y=b,Z=c,W=dqp,gX,Y,X,Y qY,Z,hU,k,U U二Y二p,X=hp,kZ=ghp,k,p第二是如果得不出矛盾那么归结法要无休止地做下去，中间归结式出得越多，匹配查找次数越多，每一步都做长时间计算，显然，要想出比这种原始归结法的更好办法，即利用切断cut操作，并对子句形式进一步限制的超级归结法Hyperresolution
12.
2.5Horn子句实现超归结Horn子句是至多只有一个非负谓词符号的子句这就等于说，通过谓词演算一个语句只包含一个蕴含运算符连接前题和结论，前题是由A，连接的几个谓词，结论就是单一的谓词符号Horn子句形式示例如下
12.6其中只有一个非负谓词S,可作以下演算，先将S移向右方F SV^PV-iQV^RV-iT
12.7按德•摩根定律F SV^PAQARAT
12.8“即一,则F S-P AQ AR AT
12.9此即条件Horn子句，因为
12.9的意义是ifP/\QAR八T thenS显然，若S为空，则为无条件Horn子句，是一个断言事实超级归结实质上是将无条件Horn子句中的谓词符号和条件子句中的对应谓词符号合一找出所有子句中变量的实例集，使每一条件子句为真如果不满足则寻找新的实例回溯算法,如果满足了也要找出所有实例为了消去不必要的匹配以提高超级归结的效率，cut操作是必须的，它可以由程序员指定当找到一个解之后不再搜索其它解它本身是个无变元谓词，当执行到它时，不再回溯cut操作也可用于分情形动作控制与fail失败谓词联用，
12.4节还将举例逻辑程序的风格
12.3基于自动定理证明的逻辑语言，有其独特的程序设计风格，因为它不描述计算过程而是描述证明过程例如，有一个问题对数组A按升序排序，我们怎样编逻辑程序呢？我们只好构造一个和A那样大的数组B,而且它是排好升序的，我们证明命题“存在一个数组B它是数组A重排升序”为此，可以陈述更严谨一些B是A的重排，当且仅当B的元素就是A的元素，且i〈j于是，自动定理证明系统依靠环境，构造一个希望的解B,并证明它的存在构造的办法不外乎匹配查找，例化或置换证明是本题的主旨排序成了副产品！除了证明性风格而外，逻辑程序的第二个特点是描述性，请见下例例12-7求平均成绩的逻辑程序打开一分数文件scores,读入分数求和并用的数N除之得平均成绩，average:-seescoresgetinput Sum,N,seen scores,Av isSum/N,print Average=Av getinputSum,N:ratom X,not eof,getinput Sumi,Nl,Sum isSumi+X,NisNl+
1.getinput0,0:-eof.要使求平均成绩程序正确，必先打开see文件，从中得到输入，得N个数的总和记以N和Sum,关闭seen文件后求平均值Av,打印之至于如何得到Sum和N,细化谓词getinput_,_o若要getinput成立，先读入一原子Xratom是系统提供的谓词若未至文件末尾，读其余分数并求和getinput是递归定义，并相应断言Sum,N和Sumi,N1的关系如果已至文件结束标记eof则输入为0,0o这个程序为求平均分数给出三条规则，号即子句的/V连接,意即所有子句为真，左端谓词才成立这个程序是用Prolog写的，我们虽未介绍它的语法，一经简单解释我们即可读懂该程序它的风格是若要A成立，做B,做C,做D,…再细化，若要B做出则要做P,做Q,做R,…这与过程式语言自顶向下描述没什么差别，且比较自由，没有严格的顺序性当然程序执行还需有事实的陈述，以及需求证明的查询逻辑程序第三个特点是大量用表和递归实现重复操作，递归特别利于谓词描述，我们只要能说明特征谓词的一步动作为真，其余如法炮制，程序就设计完了，上例中，getinput,读一数X,求和并令门数加1,其余照做关于表与递归联用的例子，见
12.4节中Prolog的例子典型逻辑程序设计语言
12.4PrologProlog是典型的逻辑程序设计语言，它基于一阶谓词逻辑，直接陈述问题世界的事实、规则和目标，非常简明清晰，所以人们称之为自文档的Prolog的程序将逻辑和控制显式分离,它使程序正确性证明简化只涉及知识，即逻辑部分，程序的优化只涉及控制部分不影响程序正确性，是正交设计成功的范例
12.
4.1Prolog的环境Prolog很长一段时间都是交互式语言，它必须要有支持环境，即管理事实和规则的数据库，并为操纵它们提供元语言小的数据库可以文件形式联接上，大的库在键盘上调用输入函数consultfilename一旦进入系统，即可查看库内容用listing predicate_name或编辑它们用retractz,还可以扩充数据库用assertaX或assertzX联上数据库，程序员即可交互使用查询、测试假设、断言更多的事实为响应查询，Prolog系统执行它的证明过程并查找能满足查询变量的事实集查找成功，写出找到的事实，若程序员满意并打回车键后，系统给出“yes”并显示新提示，如果数据库查完还未找到要的事实则给出“no”，并显示新提示
12.
4.2数据对象和项Prolog的基本成分是对象常量、变量、结构、表、谓词、运算符、函数、规则•常量预定义有十进制整数，用户定义的常量叫原子，有小写字母开头的名字,。
个人认证
优秀文档
获得点赞 0
