高级人工智能逻辑教材

高级人工智能第二章人工智能能逻辑2.1重要的形形式工具具------逻辑2.2非单调逻逻辑2.3默认逻辑辑2.4限定逻辑辑2.5自认知逻逻辑2.6真值维护护系统2.7情景演算算的逻辑辑基础2.8动态描述述逻辑逻辑的历历史Aristotle———逻辑辑学Leibnitz———数理逻逻辑GottlobFrege(1848-1925))——一一阶谓词词演算系系统,《《符号论论》20世纪纪30年年代，数数理逻辑辑广泛发发展重要的形形式工具具──逻逻辑在本世纪纪30年代以后后，数学学方法广广泛渗透透与运用用于数理理逻辑，，使得数数理逻辑辑成为数数学领域域中与代代数、几几何等并并列的学学科之一一。现代数理理逻辑可可以分为为逻辑运运算、证证明论、、公理集集合论、、递归论论和模型型论。关于知识识的表示示与推理理智能行为为的基础础是知识识，尤其其是所谓谓的常识识性知识识。人类类的智能能行为对对于知识识的依赖赖主要表表现在对对于知识识的利用用，即利利用已经经具有的的知识进进行分析析、猜测测、判断断、预测测等等。。人类利利用知识识可以预预测未来来，由已已知的情情况推测测未知的的情况、、由发生生的事件件预测还还未发生生的事件件等等。。但是，，当人们们希望计计算机具具有智能能行为时时，除了了告诉计计算机如如何像人人一样地地利用知知识以外外（对于于知识进进行推理理），一一个更为为基础和和先行的的工作是是如何使使计算机机具有知知识（对对于知识识进行表表示），，即在计计算机上上如何表达人人类的知知识。关于知识识的表示示与推理理多数的基基于逻辑辑的智能能系统使使用一阶阶逻辑或或者它的的一些扩扩张形式式。一阶阶逻辑的的优点是是它具有有相当强强的表达达能力。。有的人人工智能能专家坚坚信所有有的人工工智能中中的知识识表示问问题完全全可以在在一阶逻逻辑的框框架中得得以实现现。一阶阶逻辑在在表达不不确定性性知识时时其表达达能力也也是很强强的。例例如，xP((x)表达在所所考虑的的论域中中存在一一个具有有性质P的对象，，而具体体的是哪哪一个对对象具有有此性质质则是待待确定的的；再如如，PQ表示P和Q这两个性性质之间间有一个个是成立立的，至至于到底底是哪一一个成立立则是根根据具体体的情况况而定的的。关于知识识的表示示与推理理有人坚信信从本质质上看,一阶逻辑辑对于知知识表示示是足足够的,但从实际际应用的的角度看看,为方便、、清楚和和简洁起起见,知识表示示不一定定非得从从一阶逻逻辑出发发。事实实上，人人们从实际际应用出出发已经经发明和和建立了了许多适适用于不不同目的的的逻辑辑系统。。

(1)为了表示示关于认认知的有有关概念念，如相相信、知知道、愿愿望、意意图、目目标、承承诺等等等，人们们引进了了刻划各各种认知知概念的的模态逻辑辑；

(2)为了刻划划智能系系统中的的时间因因素，人人们在逻逻辑系统统中引进进时间的的概念，，提出了了各种时序逻辑辑；关于知识识的表示示与推理理(3)为了描述述各种不不确定的的和不精精确的概概念，人人们引进进了所谓谓模糊逻辑辑；模糊逻逻辑是直直接建立立在自然然语言上上的逻辑辑系统，，与其它它逻辑系系统相比比较，它它考虑了了更多的的自然语语言的成成分。按按照其创创始人Zadeh的说法就就是词语语上的计计算，表表示为一一个公式式,即，fuzzylogic＝computingwithwords；

(4)人类的知知识与人人类的活活动是息息息相关关的，人人类正是是在各种种活动和和行为中中获得知知识的。。因此，，行为或或者动作作的概念念在智能能系统中中是一个个关键的的概念。。动作的的概念与与一般逻逻辑中的的静态的的概念很很不相同同，它是是一个动动态的概概念，动动作的发发生影响响着智能能系统的的性质。。对于动动作的考考虑，给给人工智智能界带带来了许许多难题题，如框框架问题题、量词词问题等等等。为为了刻划划动作的的概念，，人们引引进了一一些新的的逻辑体体系来刻刻划它。。

关于知识识的表示示与推理理(5)计算机对对于人类类进行决决策时进进行若干干方面的的支持已已经成为为计算机机应用的的一个重重要方面面。人类类在决策策时，对对于各种种方案和和目标有有一定的的偏好和和选择。。这时““偏爱””就成为为了一个个基本的的概念。。为为了表述述和模拟拟人类在在决策时时的选择择的规律律和行为为，对于于“偏爱爱”这个个词的研研究就是是不可避避免的。。于是，，基于管管理科学学的所谓谓的偏爱爱逻辑被被提出并并加以研研究。

(6)时间是智智能系统统中最重重要的几几个概念念之一。。人类使使用各类类副词来来对时间间概念加加以描述述。例如如，“一一会儿””“相当当长”““断断续续续地””“偶尔尔”等等等,这一类词词在我们们的日常常生活中中比比皆皆是。含含有这些些词的句句子显然然是很难难用经典典的时序序逻辑来来刻划的的,于是有人人引进了了一种逻逻辑系统统专门刻刻划这类类句子。。其基本本思想是是利用数数学中积积分的思思想，通通过对时时间的某种像像积分那那样的表表示和运运算来形形式化这这些句子子。逻辑系统统一个个逻辑系系统是定定义语言言和它的的含义的的方法。。逻辑系统统中的一一个逻辑辑理论是是该逻辑辑的语言言的一个语句集集合，它它包括：：逻辑符号号集合：在所有该该逻辑的的逻辑理理论中均均出现的的符号；；非逻辑符符号集合合：不同的逻逻辑理论论中出现现的不同同的符号号；语句规则则：定义什么么样的符符号串是是有意义义的；证明：什么样的的符号串串是一个个合理的的证明；；语义规则则：定义符号号串的语语义。逻辑程序语言逻辑符号保留字或者符号非逻辑符号用户自定义的符号(变量名，函数名等)语句规则构造一个程序的语句规则语义规则定义程序做什么的语句规则推理规则、公理和证明没有逻辑与程程序语言言的对比比在语语法上，，如果存存在一个个从假设设到的证明，，则记为⊢，称由可推导出出的，或或可证明的的。如果果在没有有任何假假设下是可推导导出的，，则记为为⊢，称为可证明明的。称一一个假设设是不协调的的，如果存存在一个个语句使得和的否定均均可由推导得出出。称一一个逻辑辑系统是是一致的，或相容的(consistent)，如果不存存在逻辑辑系统的的公式A，使得⊢A与⊢¬A同时成立。证明明(语法)一个个证明是一个语语法结构构，它由由符号串串根据一一定的规则组组成。它它包括假假设和结结论。在公公理化逻逻辑中，，逻辑给给出一个个逻辑公理理和推理规则的集合。。推理规规则是可可以从一一个语句句的集合合得到另一语句句的集合合。公理化逻逻辑中的的证明就就是一个个语句序序列，使使得其中的每每个语句句要么是是逻辑公公理，要要么是一一个假设设，要么是由由前面的的语句通通过推理理规则得得到的。。证明语言言的解释是在某个个论语(domain))中定义非非逻辑符号。语语句的语语义是在在解释下下定义出出语言L的真假值值。如果果I是L的一个解解释，且且在I中为真，则记记为I⊨，称作I满足，或者I是的一个模型。类似似地，给给定一个个语句和一个语语句，如果对对每个解释释I，有I⊨蕴含I⊨，换言之，，如果I是的一个模模型则I也是的一个模模型，则则记为⊨，我们称为的一个逻辑结果果。解释释(语义)可靠性(reliable)一个逻辑辑是可靠靠的，如如果它的的证明保保持真假假值，即在任何何解释I下，如果果I是的模型，，且可由推导出，则I也是的一个模模型。即即，一个个逻辑是是可靠的的，如果对任任何语句句集合和语句，⊢蕴涵⊨。可靠性和和完备性性完备性(complete)一个逻辑辑是完备备的，如如果任何何永真语语句是可可证的。。即，对任任何语句句集合和语句，⊨蕴涵⊢。如果一个个逻辑是是完备的的，则该该逻辑的的证明系系统已强强到可以推出出任何永永真式。。Gődel完备性定定理：一阶逻辑辑是完备备的可判定的的一个个逻辑称称为是可判定的的(decidable))，如果存在在一个算法法对逻辑辑中的任任一公式式A，可确定⊢A是否成立。否则则，称为为是不可判定定的(undecidable)。如果上述述算法虽虽不一定定存在，，却有一一个过程程，可对对该系统统的定理理做出肯肯定的判判断，但但对非定定理的公公式过程程未必终终止，因因而未必必能作出出判断。。这时称称逻辑是是半可判定定的。可判定性性一阶逻辑辑是不可可判定的的，但它它是半可可判定的的。

哲学逻辑辑手册1983-89年间出版版了4卷本哲哲学逻辑辑手册(HandbookofPhilosophicalLogic)2001年开始出出版第2版，约为为18卷，迄今已已经出版版12卷。该书书由英国国伦敦皇皇家学院院计算机机系的多多夫·加贝（DovM.Gabbay）教授和德德国路德德维希-麦克米兰兰大学信信息与语语言处理理中心的的冈瑟（F.Guenthner）教授共同同主编。。已经出版版的前12卷内容高阶逻辑辑冲冲突多值逻辑辑模糊逻辑辑概率论条条件件句模态逻辑辑动态逻辑辑容错逻辑辑优先先逻辑图形逻辑辑偏逻辑直觉主义义逻辑非单调推推理信念逻辑辑自由逻辑辑时序逻辑辑相干逻辑辑量子子逻辑蕴涵逻辑辑时态态逻辑问问题逻逻辑道道义逻辑辑弗协调逻逻辑目目标导导向演绎绎认认知逻逻辑加标演绎绎系统（逻辑新新框架理理论）等等现代逻辑辑学与计计算机科科学、计计算语言言学和人人工智能能的关系系表逻辑辑自自然然语程程序人人工逻逻辑指指令与直直数据据库复复杂性智智能体体未未来来展望望言处理控控制智智能编编程陈陈式语语言理理论理理论理理论论时序逻辑辑√√√√√√√√√√√√√√√广泛应用用模态逻辑辑√√√√√√√√√√√√√√√非常活跃跃算法证明明√√√√√√√√√√√√√√√非单调推推理√√√√√√√√√√√√√意义重大大概率和模模糊√√√√√√√√√√√√√目前主流流直觉主义义逻辑√√√√√√√√√√√√√√√主要替代代者高阶逻辑辑，λ-演算√√√√√√√√√√√更具中心心作用经典逻辑辑片断√√√√√√√√√√√前景诱人人资源和子子结构逻逻辑√√√√√√√纤维化和和组合逻逻辑√√√√√√√√√√√可自我指指称谬误理论论在在适当当语境逻辑动力力学√√√动态逻辑辑观论辩理论论游戏√前景光明明对象层次次/元层次√√√总起中心心作用机制:溯因缺缺省相相干√√√逻辑的一一部分与神经网网络的联联系极极重要，，刚开始始时间-行动-修正模型型√√√一类新模模型加标演绎绎系统√√√√√√√√√逻辑学的的统一框框架命题逻辑辑命题是可可以确定定其真假假的陈述述句。Bolle提出出了布尔尔代数。。语言:¬，；公公式，原原子公式式公理模式式:◆(A(BA))◆((A(BC))((AB)(AC)))◆(((¬A))(¬B)(BA))推理规则则:分离规则则(modusponens，MP规则)谓词逻辑辑(一阶逻辑辑)Frege谓词词演算语言:¬，，，，，(，)；常元，，变元，，函词，，谓词；；公式公理模式式:◆(A(BA))◆((A(BC))((AB)(AC)))◆(((¬A)(¬B))(BA))◆vAAtv(t对A中变元v可代入)◆v(AB)(vAvB)◆AvA(v在A中无自由出现现)推理规则则:分离规则则谓词逻辑辑与命题题逻辑的的区别谓词逻辑辑给出了了原子语语句的内内部结构构，将原原子公式式看作是是事物直直接的关关系；它引入了了“推广广”(泛化)，加强了了逻辑的的表示能能力和推推理能力力。这样样，我们们可以说说某种性性质对某某个对象象是成立立的，或或对所有有的对象象成立，，或不对对任何对对象成立立。逻辑程序序设计消解原理理(归结结原理))Horn逻辑Prolog逻逻辑程序序设计语语言归结原理理例：C1=¬P∨Q∨RC2=P∨Q则C1与C2消解后的的结果为为：Q∨R若子子句集S能导出空空子句⊓(有否证证)，则则称S是不可满满足的。。反证证法：S⊢AiffS¬A⊢⊓Horn逻辑文字：原子公公式(正正文字))或原子子公式的的否定((负文字字)。P,Q,¬R子句：若干文文字的析析取。¬P∨Q∨RHorn子句：子句句L1∨L2∨…∨Ln中如果至至多只含含一个正正文字，，那么该子子句称为为Horn子句。Horn子句P∨¬Q1∨¬Q2∨…∨¬Qn通常表示示为：PQ1,Q2,…,,QnHorn子句的类类型：◆过程：PQ1,Q2,…,,Qn◆事实：P◆目标：Q1,Q2,…,,Qn◆空子句：：⊓例:◆过程：AT(dog,,x)AT(Zhang,,x)◆事实：AT(Zhang,,train)◆目标：AT(dog,,train)首先目标标中过程程调用AT(dog,,train)与过程程名AT(dog,x)匹配，合合一为{{train/x}，调用用过程AT(Zhang,x)，从而而产生新目目标AT(Zhang,,train)，与事实匹配配，产生生目标⊓。因而调调用成功功，输出出“是””。PrologProlog((Programminginlogic)语语言是以以Horn子句句逻辑为为基础的的高级程程序设计计语言。。1972年，法法国马赛赛大学的的Alain..Colmerauer提提出了Prolog的的雏型。。1975年，Prolog被用于问问题求解解系统。。此后，它它在许多多领域获获得了应应用，如如关系数数据库、、定理证证明、智智能问题题求解、、计算机机辅助设设计、规规划生成成等领域域。Prolog的构成事实：关于对象象性质和和关系的的事实语语句；student(john))，married((tom,mary))规则：关于对象象性质和和关系的的定义规规则语句句；它与事实实的不同同在于，，规则所所定义的的性质、、关系依依赖与其它它的性质质和关系系，因此此规则呈呈蕴涵语语句形式式。B:—A““如果A则B”bird(x):—animal((x)，has(x,feather))问题：关于对象象性质或或关系的的询问。。?—student(john))?—married(mary，，x)Prolog语言的基基本文法法Prolog语言的最最基本语语言成分分是项(term)，一个项或者是是常量，或者是是变量，或者是是一个结构。常量：是指对象象和对象象之间的的特定关关系的名名；整数，如0，22，1586等；原子，如John，student，，likes，，sister-of变量：表示任意意的对象象，它与与FOL中的变元元相同；；Prolog中变量可可以用大大写字母母，下划划线，以以及由它它们开头的字字母串。。如X,Y,Answer,_value等。结构：是常量和和变量的的序列，，它由一一个函子子(函词词或谓词))和该函函子的自自变量所所组成。。如：likes(john,X)married(mary,jack)例：(1)likes(bell,sports)(2)likes(mary,smith))(3)likes(mary,sports)(4)likes(jones,,smith)(5)friend(john,X):—likes(X,sports),,likes(X,smith)((规则)(6)??—friends(john,Y)((问题)(事实)(7)??—likes(X,sports),,likes(X,smith)(8)??—likes(bell,smith))((bell/X)(7)??—likes(X,sports),,likes(X,smith)(8)??—likes(mary,smith))((mary/X)Y=mary，John与Mary是朋友Prolog的执行方式式搜索：在程序中中自上而而下地搜搜索事实实和规则则；匹配：将目标中中的项与与事实和和规则进进行匹配配；回溯：当目标中中一项失失败时，，如果目目标中有有已经成成功的的的项(应应在失败败项的左左边)，，那末就就重新调调用这些些成功项项中最右右边的一一个，谋谋求新的的成功。。Prolog的基本特特点Horn子句逻辑辑是Prolog的基础。。Prolog既是一种种逻辑程程序设计计语言，，又是一一个逻辑辑系统。。Prolog是一种描描述性语语言，它它是一种种面向问问题的语语言，你你只需要要告诉它它要做什什么，即即给出问问题的形形式描述述，而不不需要知知道应该该如何做做。Prolog完全依靠靠匹配、、回溯来进行搜搜索。Prolog的的求解过过程是一一个寻求求否证的的消解过过程。Prolog也使用元元语言种种的谓词词，有很很强的描描述能力力。Prolog采用统一一的数据据结构———项，，它包含含控制成成分，且且有专门门进行数数值计算算和符号号处理的的模块。。逻辑程序序设计PROLOGBA1,…,,AnB?A1,…,,An单调逻辑辑在现有知知识的基基础上，，通过严严密的逻逻辑论证证和推理理获得的的新知识识必须与与已有的的知识相相一致。。A，ABB推理系统统的定理理集合随随着推理理过程的的进行而而单调地地增大。。单调性：：(1)∈Th()(2)若若1⊆2，则Th(1)⊆Th(2)(3)Th((Th(())＝＝Th()((不动动点)非单调逻逻辑推理系统统的定理理集合并并不随着着推理过过程的进进行而单单调地增增大，新新推出地地定理很很可能会会否定、、改变原原来地一一些定理理，使得得原来能能够解释释地某些些现象变变得不能能解释了了。新规则：：(4)⊬¬P(不动点点)非单调逻逻辑推理系统统的定理理集合并并不随推推理过程的进进行而单单调地增增大,新推出的的定理很可可能会否否定、改改变原来来的一些些定理,使得原来来能够解解释的某某些现象变得不能解解释了。。非单调逻逻辑推理系统统的定理理集合并并不随推推理过程的进进行而单单调地增增大,新推出的的定理很可可能会否否定、改改变原来来的一些些定理,使得原来来能够解解释的某某些现象变得不能解解释了。。t1<t2F(t1)F(t2)非单调逻逻辑鸟会飞鸵鸟是鸟鸟所以,鸵鸟会飞飞非单调推推理1John在时刻t1是活着的的2Dell在时刻t2>t1把子弹装装进枪膛膛3Dell在时刻t3>t2举枪对John射击4问题：John在时刻t4>t3还是活着吗吗？非单调逻逻辑设表示示推理规规则集,则单调逻逻辑语言言Th()={{A|A}}(1)Th())(2)if12,thenTh(1)Th((2))(3)Th(Th()))==Th())(不动点)(4)ifP,thenMP其中M模态词默认逻辑1980年，Reiter提提出了默默认缺省省逻辑((DefaultLogic)。。“一般情情况下鸟鸟是会飞飞的”“鸵鸟不不会飞”” “企企鹅不会会飞”默认规则一个个默认规规则是如如下形式式的规则则：(x):称为前提提条件i(x):称为缺省省条件，，或检验验条件(x):称为结论论为简便，，通常情情况下可可以省略略检验条条件中的的M。规则的使使用：如果果规则的的前提条条件满足足，且现现有的知知识导不不出检验条条件的否否定¬i(x)，则可以得得出结论论成立。。默认理论论一个个默认理论论由两个部部分组成成，即默认规则集D和公式集集W，一般用二二元组来来表示＝<D,W>若D中的规则则是闭规规则时，，则为闭缺省省理论。。定义：设＝<D,W>为一闭缺缺省理论论，为关于D的一个算子子，作用于任任意的命命题集合合S，而其值值为满足下列三三个性质质的最小小命题集集合(S)：(1)W(S)(2)Th(((S))==(S)，其中中Th(((S))=={A|(S)⊢A}(3)如如果D中有规规则，，且∈(S)，¬1,…,,¬m∉S，那么∈(S)默认理论的扩扩充定义：对命题题集合E，如果(E)=E，则E称为关于于D的算子的不动点(fixpoint))。此时时称E为默认理论＝<D,W>的一个扩充(extension)。例1：设D＝{ }，W＝，计算默认理论＝<D,W>的扩充。＝<D,W>有唯一的的扩充E＝Th({¬B,¬F})。例2：设D＝{}}，W＝{B,CF∨A,A∧C¬E}，计算算默认理论＝<D,W>的扩充。＝<D,W>有三个扩扩充E1＝Th(W{A,C})E2＝Th(W{A,E})E3＝Th(W{C,E,G})封闭默认认理论的的扩展设封闭默默认理论论=<D,W>,为关于D的一个个算符，，作用于任任意的命命题集合合S，其其值为满满足下列列三个性性质的最最小命题题集合(S):

(1)W(S);;

(2)Th(((S)))=(S);;这里里，Th((S)))为命题题集{A|(S)A};

(3)如如果有默默认规则则

封闭默认认理论的的扩展命题集合合E称为为关于D的算符符的固定点点，如果果(E)==E,,此时时又称E为=<D,W>$的的一个个扩充。。有了扩充充的概念念，便可可定义非非单调的的“推出出”概念念。

如果命题题A包含含在默认认理论的一个扩扩充中，，那么称称A在中可推出出，记为为|。扩充E必须①①含有有所有的的已知事事实;②在关关系|下是封闭闭的;③其前前提被E满足足,默默认条件件与E相容容的任意意默认的的结论必必须也在在E中。。

封闭默认认理论的的扩展具有扩展展的存在在条件将将显得十十分重要要。下面面我们讨讨论三种种情况。。

(1)不不含任任何默认认的理论论<{}},W>::这种种理论退退化到一一阶逻辑辑理论,,在这里它它虽有唯唯一的一一个扩展展Th((W),,但对对默认推推理毫无无意义和和作用。。

(2)一一个默默认理论论<D,W>称为为规范默默认理论论，如果果D中默默认规则则均有如如下形式式:封闭默认认理论的的扩展如果一个个理论中中的所有有默认都都是规范范的,则则该理论论称为规规范理论论。由于于每个规规范默认认的结论论与其合合理条件件相同,,因而而这种缺缺省不会会导致不不一致性性,不不会证伪伪其它已已用过的的默认的的合理条条件。因因此我们们说规范范默认理理论是行行为良好好(well-behaved))的的理论,,并且且可以证证明:任任何规规范默认认理论必必定至少少有一个个扩充。。封闭默认认理论的的扩展(3)半半规范范默认理理论((SeminormalDefaultTheory)::虽然然规范默默认理论论至少有有一个扩扩充,从从而保保证了系系统知识识库W的一一致性。。然而现现实世界界中许多多事物、、现象是是无法用用规范默默认表示示的,而而用如如下形式式的默认认则可有有效地进行处处理:封闭默认认理论的的扩展为了保证证半规范范默认理理论具有有一个扩扩充,必必须对对它的默默认加以以限制,,Reiter给出了了一个半半规范默默认理论论至少具具有一个个扩充的的充分条条件,这这个条条件要求求封闭的的半规范范默认理理论是有有序的..。有序序性建立立在一个个偏序关关系上,这这个偏序序要求::如果果在推导导β的过过程中用用到了αα,则则αβ。Etheringthon在这这种基础础上给出出了求算算偏序关关系及其其扩充的的算法,,并讨讨论了算算法的收收敛性问问题。限定推理理1980年，McCarthy提出了一一种非单单调的推推理——限定推理理(Circumscription))。基本思想想：从某些些事实A出发能够够推出具具有某一一性质的的P的对象就就是满足足性质P的全部对对象。只只有当发发现其它它对象也也具有该该性质时时，才修修改这种种看法。。限定逻辑辑限定逻辑辑CIRC是一种极极小化逻逻辑。下下面，从从一个基基于极小模型型定义的的命题限限定出发发，给出出限定的的基本定定义,进而给出一一阶限定定的基本本结果，，并将它它推广。。定义2.1设设L0是一个命命题语言言，p1,p2是在命题题语言L0中的两个赋赋值。称称p1小于p2，记为p1p2,当且仅当当对任一一命题变元元x,如果p1(x)==l,则p2(x)==l。限定逻辑辑定义2.2设设A是一个公公式，称称A的一个赋赋值p是极小的，当且且仅当不不存在A的其它赋赋值p'使得p'p。显然,是一个偏偏序关系系。p1p2表示p1包含的真真命题比比p2少。极小小赋值包包含的真真命题极极小。定义2.3极小后承承M。设A,B是两个公公式，AMB当且仅当当B在所有A的极小模模型中都都为真。。极小模型型是非单单调的，，它以命命题的极极小化作作为优先先模型的的准则。。限定逻辑辑定义2.4设设A是一个包包含命题题集P={{p1,p2,....,pn}的公式，，一个A的赋值p称为Z-极小赋值值，当且且仅当不不存在A的其它赋赋值p‘使得pp’,定义如下下：设p1,p2是两个赋赋值，p1Z-p2当且仅当当对任一一zZ,若p1(Z)==l,则p2(Z)==l。

限定逻辑辑定义2.5命题限定定P或CIRC(A,P)。设A是一个包含命题题集的公公式，是一个公公式，AP当且仅当在所有A的p-极小赋值值中都为为真。定理2.1Ap当且仅当当AP

限定逻辑辑定义2.6令令L是一个一一阶语言言，T是一个L的公式，，它包含谓词词元组集集。设M[T]]和M*[T]是公式T的两个模模型。定义M*[T]优先于M[T]],记为M*[T]M[T]]，当且仅当当(1)M和M*有相同的的对象域域，(2)除外，公式式T中所有的的其它关关系和函函数常数数在M和M*都有相同同的解释释，(3)在M*中的外延延是在M中的子集集。限定逻辑辑

一个理论论T的模型M称为优先先的，当当且仅当当不存在在T的其它模型型M'使得M'M。定义2.7Mm是的最小模模型，当当且仅当当MMm,M==Mm

限定逻辑辑例如设设论域D={1,2}}T=xy(P((y)Q(x,y)))=[(P(1))Q(1,,1)))((P((2)Q((1,2))]][(P((1)Q((2,1))((P(2)Q(2,2)))]M:P(1)P(2))Q((1,1)Q(1,2))Q((2,1)Q(2,2))TTFTFTM*:P((1)P(2)Q(1,,1)Q((1,2)Q(2,,1)Q((2,2)FTFTFT自认知逻逻辑Moore考虑自认认知理论论T对于一组组初始前前提A是可靠的的，当且仅当当T中的每一一个自认认知解释释器是一一个T中的自认认知模型，其其中全部部A的公式为为真。一一个理想想的理性性主体的的信念必须满满足下列列条件：：(1)设P1,....,PnT,andP1,....,PnQ,则QT。(2)设PT,则BPT。(3)设PT,则~BPT。自认知逻逻辑在这种情情况下，，主体不不能再得得到更进进一步的的结论，，因此，Moore称上述理理论为稳稳定自认认知理论论。当然然，下列条件也也成立：：(4)如果BPT,则PT。(5)如如果果~BPT,则则PT。真值维护护系统TMS1979年，Doyle提出了一一种非单单调推理理系统——真值维护护系统(TruthMaintenanceSystem)真值维护护系统是是大型推推理系统统的的一一个子系系统，实现知识识库中信信念(belief))的修改与与维护。。其基本本问题有：必须在不不完全的的、有限限的信息息基础上上作出假假设的决决策，使使得该假假设成为为知识库库的信念念；当这些决决策的结结论被以以后的事事实证明明为错误误时，如如何对其其信念进进行修正正。基本数据据结构:结点：表示信信念理由：表示信信念的原原因信念既包包括已知知的知识识，也包包括假设设的知识识。基本操作作：新结点的的形成——将信念赋赋予该结结点；新理由的的加入——把某个信信念与该该结点联联接起来来实现过程程：默认假设设的形成成；相关性回回溯过程程。信念知识识表示每一个命命题或规规则均称称为结点点，它分分为两类类：IN-结点：相信为真真OUT--结点：不相信为为真，或或无理由由相信为为真，或当前没没有任何何有效的的理由。。每个结点点附有理理由表，，表示具具体结点点的有效效性：支持表SL：所在结点点的信念念的原因因，理由由；条件证明明CP：出现矛盾盾的原因因。(SL(<<IN--结点表>)(<<OUT--结点表>))IN-结点表中中的IN-结点表示示知识库库中的已已知知识识;OUT--结点表中中的OUT--结点表示示这些结结点的否否定。例1:(1)现在是夏夏天(SL())()))(2)天气很潮潮湿(SL(1)()))结点(1)不依赖于于任何别别的结点点中的当当前信念念或默认信念念,因而这种种结点称称为前提提;结点(2)则依赖于于当前结结点(1)的信念.所以，与与一阶逻逻辑不同同的是,TMS可以撤消消前提,并可以对对知识库库作适当当修改.（1）支持表表SL例2:(1)现在是夏夏天(SL())()))(2)天气很潮潮湿(SL(1)(3))(3)天气很干干燥若结点(1)是是IN,结点(3)是是OUT,,则结点(2)才为IN.若在某个时时刻出现现结点(3)的证据,则结点(2)就变为OUT,,因为它不不再有一一个有效效的证实实.象结点(2)这样的结点称称为假设设,它与非空空的OUT结点表的的SL证实有关.OUT结点(3)是结点(2)的证实的的一部分分.但如果结结点(3)不存在,就不能这这样表示示了.在TMS中,它仅利用用证实来来维持一一个相容容的信念念数据库,而它本身身并不产产生证实实.(CP<<结论><IN-假设><OUT--假设>)如果结论论结点为为IN-结点,以及下列列条件成成立:(1)IN假设中的的每个结结点都是是IN-结点;(2)OUT--假设中的的每个结结点都是是OUT--结点.那么条件件证明CP是有效的.一般说来来,OUT--假设总是是空集.TMS要求假设设集划分成两个个不相交交的子集集,分别为不不导致矛矛盾的假假设和导致矛盾盾的假设设.通常只要要在IN-假设中的的结点为为IN,OUT--假设中的结点为为OUT,,则结论结结点为IN.（2）条件证证明CP默认假设设令{F1,F2,…,,Fn}表示所有有可能的的侯选的的默认假假设结点集集,G表示选择择默认假假设的原原因的结结点,即由G引起在{F1,…,,Fn}中进行缺缺省选择择.这样我们们结合结结点Node(Fi)以如下理理由:(SL(G)(F1,…,,Fi-1,Fi+1,…,,Fn))而选取Fi为默认假设设.如果不存存在任何何其它关关于如何何进行选选择的信信息，则可以认认为除Fi之外其它它任何时时候选都都不是可可信的．．这样Fi为IN,其它Fj(ij)均为OUT..但如果接接收到一一个有效的的理由支支持某个个其它的的侯选Fj,则Fj就为IN,而导致Fi的假设失败败而变为为OUT..相关回溯溯当知识库库中出现现不一致致时,TMS将寻找并并删除已已做的一个个不正确确的默认认逻辑,恢复一致致性.它包括三三个步骤:(1)从产生的的矛盾结结点开始始,回溯跟踪踪该矛盾盾结点的理由充充足的支支持以寻寻找矛盾盾的假设设集,并从中去去掉至少一个个假设信信念以消消除矛盾盾.(2)构造一个个结点记记录矛盾盾产生的的原因.(3)从从S中选取假假设A(即不合理理假设),并证实列列在其理由充充足的支支持条件件中的一一个OUT--结点.(4)矛盾(SL(1,3))()))(周三14:00没有空会会议室)例3:(1)会议日期期为星