第章逻辑和定理证明.doc

第7章 逻辑和定理证明 逻辑是一种强有力的问题求解范型，与其它问题求解范型一样，逻辑既有诱人的优点，也有烦人的弱点。 传统逻辑是成熟的，并为科学界所熟知。逻辑是严密的，一旦问题领域能用逻辑建模、问题的界限就会变得明了，问题的属性能够得到深刻的理解。特别是，我们能够知道模型的限制性。 过份强调逻辑规范化，使AI研究集中在数理逻辑上，会忽略很多有价值的、与数学不相容的问题求解技术。 AI与逻辑有天然的联系： 它们都是研究思维规律的科学。 机械定理证明是AI的一个分支，同时也是逻辑的一个重要的研究课题。 AI中的许多问题求解范型，如反向链方法和正向链方法，能够用逻辑进行精确的刻划。 AI程序设计语言－－PROLOG是面向逻辑，它有坚实的逻辑基础。 AI的研究提出的很多问题，成为逻辑的发展动力，开创了逻辑研究的很多分支：时态逻辑、模态逻辑，非单调逻辑等。 AI研究和逻辑研究相互影响，相互促进。 本章的主要内容为： 归结定理证明； 在逻辑中引入状态算子，试图解决计划问题； 约束传播证明。 7.1 基本概念 7.1.1 概念定义 定义 项（term） 1）常量符号是项。 2）变量是项。 3）若f是n元函数符号，ti是项，则f(t1, ..., tn)是项。 4）任何项都是由上述规则产生。 定义 原子（atom） 若P是n元谓词符号，t1, ..., tn是项，则P(t1,..., 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}，不包含任何文字的短句称为空短句，空短句的真值为假（F）。 定义 短句集合（Clause set） 由一个或多个短句组成的集合称为短句集合，一般用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中的一个对象。 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是可满足的（一致的），当且仅当存在解释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是不可满足的。 2）P(( P是有效的。 3）P (Q是可满足的。 其中，P和Q是公式。 例子，将下列两条规则符号化： Rule I3 if x有羽毛 then x是鸟 Rule I4 if x会飞