资源描述：
《第章逻辑和定理证明》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、第7章逻辑和定理证明逻辑是一种强有力的问题求解范型，与其它问题求解范型一样，逻辑既有诱人的优点，也有烦人的弱点。l传统逻辑是成熟的，并为科学界所熟知。逻辑是严密的，一旦问题领域能用逻辑建模、问题的界限就会变得明了，问题的属性能够得到深刻的理解。特别是，我们能够知道模型的限制性。l过份强调逻辑规范化，使AI研究集中在数理逻辑上，会忽略很多有价值的、与数学不相容的问题求解技术。AI与逻辑有天然的联系：l它们都是研究思维规律的科学。l机械定理证明是AI的一个分支，同时也是逻辑的一个重要的研究课题。lAI中的许多问题求解范型，如反向链方法和正向链方法，能够用逻辑进行精
2、确的刻划。lAI程序设计语言－－PROLOG是面向逻辑，它有坚实的逻辑基础。lAI的研究提出的很多问题，成为逻辑的发展动力，开创了逻辑研究的很多分支：时态逻辑、模态逻辑，非单调逻辑等。lAI研究和逻辑研究相互影响，相互促进。本章的主要内容为：l归结定理证明；l在逻辑中引入状态算子，试图解决计划问题；l约束传播证明。7.1基本概念7.1.1概念定义定义项（term）1）常量符号是项。2）变量是项。3）若f是n元函数符号，ti是项，则f(t1,...,tn)是项。4）任何项都是由上述规则产生。定义原子（atom）若P是n元谓词符号，t1,...,tn是项，则P(t
3、1,...,tn)是原子。若项t1,...,tn都不含变量，则P(t1,...,tn)是命题。定义合式公式（wff）1）原子是公式（原子也称为原子公式）。2）若G和H是公式，则┐G，GÚH，GÙH，G®H，G«H是公式。3）若G＝G[x]，则"xG[x],$xG[x]是公式。4）任何合式公式都是由上述规则产生。定义文字（literal）文字是原子或原子之非。设P为原子，则P，┐P都是文字。定义短句（clause）短句是文字的析取式。设L1,...,Ln是文字，则L1ÚL2Ú...ÚLn是短句。有些情况下，也将短句表示为文字的集合{L1,...,Ln}，不包含任
4、何文字的短句称为空短句，空短句的真值为假（F）。定义短句集合（Clauseset）由一个或多个短句组成的集合称为短句集合，一般用S表示短句集合。若S={C1,C2,...,Cn}，C1,...,Cn中出现的所有变量为x1,x2,...,xm，则S="x1..."xm(C1ÙC2Ù...ÙCn)即，S中的变量都是全称量化的，所有变量的出现都是受约的。S的短句用“与”联接词连接。定义解释（interpretation）合式公式G的解释I由下列方法构成：1）规定一个由对象构成的非空定义域D。2）对G中的每个常量符号，赋予D中的一个元素，即G中的每个常量指称D中的一个
5、对象。3）对G中的每个n元函数符号f,以及任意d1ÎD,...,dnÎD，规定D中的一个元素d，使得f(d1,...,dn)=d，即定义f：Dn®D。4）对G中的每个n元谓词符号P，以及任意d1ÎD,...,dnÎD，规定命题P(d1,...,dn)的真值，即定义P：Dn®{T,F}。5）"xG[x]为真，当且仅当对任意dÎD，使G[d]为真。$xG[x]为真，当且仅当存在dÎD，使G[d]为真。定义有效公式（valid）公式G是有效的，当且仅当在任意解释I下，G的真值为真。定义可满足的公式（satisfiable）公式G是可满足的（一致的），当且仅当存在解释
6、I，在I下G的真值为真。定义不可满足的公式公式G是不可满足的（不一致的），当且仅当在任意解释I下，G的真值为假。使公式G为真的解释称为G的模型。不可满足的公式，不存在模型。若解释I使G为真，则称I满足G。定义逻辑`推论设F1，...，Fn和G为公式，称G为F1，...，Fn的逻辑推论，当且仅当对任一解释I，若I满足F1ÙF2Ù...ÙFn，则I也满足G。设F1，...，Fn和G为公式，G是F1，...，Fn的逻辑推论，当且仅当公式F1Ù...ÙFn®G是有效的。或当且仅当公式F1Ù...ÙFnÙØG是不可满足的。例子，容易验证下列断言成立：1）PÙØP是不可满
7、足的。2）PÚØP是有效的。3）P®Q是可满足的。其中，P和Q是公式。例子，将下列两条规则符号化：RuleI3ifx有羽毛thenx是鸟RuleI4ifx会飞x产蛋thenx是鸟解：令feathers(x)表示x有羽毛，bird(x)表示x是鸟，flies(x)表示x会飞，lays_eggs(x)表示x产蛋。则，规则I3可符号化为"x(feathers(x)®bird(x))规则I4可符号化为"x((flies(x)Ùlays_eggs(x))®bird(x))例子，将下列语句符号化1）每个人都是要死的。2）孔夫子是人。3）孔夫子是要死的。解：令human(x
8、)表示x是人，Congfuzi表示孔夫
