Computer Science and Application 计算机科学与应用, 2011, 1, 51-56 doi:10.4236/csa.2011.12011 Published Online September 2011 (http://www.hanspub.org/journal/csa/) Copyright © 2011 Hanspub CSA The Study of Resolution Principle Based on Predicate Logic Youyun Ao School of Computer and Information, Anqing Teachers College, Anqing Email: youyun.ao@gmail.com Rece iv e d: May 12th, 2011 ; re v is e d: Jul. 11th, 20 11; ac ce pted: Jul. 25th, 2011. Abstract: Resolutio n principle based on predication logic is an effective approach to implementing machine reasoning or automated reasoning, and applying it can prove theorems and extract answers to questions. This paper analyzes the theoretical basis of resolution principle based on predicate logic, and discusses some methods and procedures of applying resolution principle based on predicate logic to theorem proving and problem’s answer extracting. Keywords: Predicate Logic; Resolution Principle; Artificial Intelligence; Knowledge Representatio n 基于谓词逻辑的归结原理研究 敖友云 安庆师范学院,计算机与信息学院,安庆 Email: youyun.ao@gmail.com 收稿日期:2011 年5月12 日;修回日期:2011 年7月11 日;录用日期:2011年7月25 日 摘 要:基于谓词逻辑的归结原理是实现机器推理或自动推理的有效途径,利用它可以证明定理和提 取问题答案。分析了基于谓词逻辑的归结原理的理论基础,并论述了将基于谓词逻辑的归结原理应用 于定理证明和问题答案提取的方法及步骤。 关键词:谓词逻辑;归结原理;人工智能;知识表示 1. 引言 谓词逻辑是在命题逻辑的基础上发展而来的,通 过引入量词,它比命题逻辑能更有效地表示和求证复 杂问题。谓词逻辑采用形式化语言系统,通过一定的 推理规则和控制策略,研究前提和结论之间的蕴涵关 系。谓词逻辑具有严格的理论基础,可以保证推理过 程和结论的正确性,同时它的形式化语言接近人类的 自然语言,容易为人类所理解和接受[1]。 经典的演绎推理系统具有证明过程自然、易于理 解、推理规则丰富、推理过程灵活等优点,但也存在 推理过程中容易产生组合爆炸、证明方法难以判定等 缺点[2,3]。Robinson[4]于1965年借助演绎推理反证法的 思想提出了归结原理,它是一种形式单一、处理规则 简单,可以在机器上实现的逻辑推理技术。归结原理 的提出,为人类提供了一种简单易行的方法实现定理 的证明和问题的求解,使定理证明可以在机器上机械 现实,是自动推理的重大突破[5,6]。 本文从理论基础、求证问题的方法及步骤方面对 基于谓词逻辑的归结原理进行了研究。论文的组织结 构如下:第 2节分析了基于谓词逻辑的归结原理的理 论基础;第 3节讨论了将基于谓词逻辑的归结原理应 用于定理证明和问题答案提取的方法及步骤;最后对 全文进行了总结。 2. 基于谓词逻辑的归结原理的理论基础 2.1. 归结原理的基本思想 根据谓词公式和其对应的子句集在不可满足的意 义下是等价的,为了证明谓词公式是不可满足的,可 敖友云 基于谓词逻辑的归结原理研究 52 | 以转化为证明其对应的子句集是不满足的。Robinson 归结原理的基本思想描述如下[4]:首先将待证明问题 的结论的否定和问题的前提表示成谓词公式,然后将 这些谓词公式转化为一个相应的子句集 S,接下来按 一定的归结策略检验子句集 S中是否含有空子句□, 若含有空子句,则表明子句集 S是不可满足的,问题 得到证明;否则继续在子句集 S中选择合适的子句对 进行归结,并将归结式并入子句集 S中,直至推出空 子句或不能继续归结为止。 Robinson 归结原理中的子句(clause) 是指任何文 字的析取式,而空子句指的是不含任何文字的子句, 记为□或 NIL,子句集 S中各子句之间是合取关系, 只要其中有一个子句是不可满足的,则整个子句集 S 就是不可满足的。因为空子句是不可满足的,所以在 归结过程中若出现空子句,则整个子句集 S就是不可 满足的。归结原理的完备性是指子句集 S是不可满足 的,当且仅当存在一个从 S到空子句的归结过程。 2.2. Skolem函数 引入 Skolem 函数的目的是消去谓词公式中的存 在量词。通常,谓词公式包含量词和母式两部分,在 消去存在量词时要区分下列两种情况[7]:1) 若要消去 的存在量词不位于任何一个全称量词的辖域内,则选 用一个未曾出现在母式中的新常量去替代母式中受该 存在量词约束的变量,然后删去该存在量词;2) 若要 消去的存在量词位于一个或多个全称量词的辖域内, 则选用一个未曾出现在母式中的新函数去替代母式中 受该存在量词约束的变量,而该新函数的变量就是这 些全称量词所约束的变量,然后删去该存在量词。例 如,下列谓词公式: ,, ,,xyzuvPxyzQxuv 消去存在量词后得到: ,,,, ,,yzPayzQafyzg yz 其中 a为常量, , 和xa ,ufyz ,vgyz为 Skolem 函数。 通常,把消去存在量词时用到的新常量和新函数 统称为 Skolem 函数,而把消去谓词公式中全部存在 量词后得到的谓词公式称为 Skolem 范式。由于在消 去存在量词时所用的 Skolem 函数可以不同,因此消 去存在量词后得到的 Skolem 范式并不唯一。一般地, 一个谓词公式与其 Skolem 范式并不等值,但若一个 谓词公式是不可满足的,则其 Skolem 范式也一定是 不可满足的,即引入 Skolem 函数并不影响原谓词公 式的不可满足性。 2.3. 置换与合一 设 和为两个不同的子句, 1 C2 C1 L 和2 L 分别为 和中的两个文字,且 1 C 2 C1 L 和2 L 同属于一个谓词,不 妨设 1 L 是原子,而 2 L 是原子的否定。若 1 L 和2 L 中存 在对应个体项不相同时,需要进行置换,解决匹配问 题,才能使得推理继续进行。称 11 ,,n txn tx 为 有限集上的一个置换(substitution)[8],其中 ij xx ji , ij,1,2,,n , 为常量、变量或函数, i t ii tx表示用 替代,t i ti xii x ,i,且不允 许循环出现在另一个 中。例如,集合 1, 2,,n i xj t , g axfxy和 b z,,yfaxc 是两个置换, 而集合 , g yxfxy不是一个置换。 置换可以进行合成运算,置换的合成也是置换。 设有置换 11 ,, nn tx tx , 11 ,, mm uyuy , 则 与 的合成(记为 )也是一个置换[9],通过下列 方法得到:首先求出集合 11 11 ,y i x ,, ,mm tx txuuy nn i ,然后从中删去以 下两种元素:当 t 时,删去元素 1, 2, ii tx ,ni;当 12 ,,, j n y xx x时,删去元 素 1, 2,, jj uyjm。例如,设置换 , f yxz y, ,,axbyyz ,则置换的合 成 , f bx yz。 置换的目的是为了合一,而合一通过置换使得 1 L 和2 L 保持一致。设 1 L 和2 L 存在一个置换 ,使得 12 L L ,则称 1 ,2 L L 是可合一的, 称为合一置 换(unification)。若 1 ,2 L L 有合一置换 ,且 对12 , L L 的任意合一置换 都存在置换 使得 ,则称 是1 ,2 L L 的最一般(最简单)合一置换,记作 。 两个公式的合一置换未必唯一,但它的最一般合一置 换一定是唯一的。例如,置换 mgu ,cxby 是 b,,Pax, ,a,xff yP的一个合一置换,而它的 最一般合一置换为 by 。 2.4. 二元归结 在合一置换的基础上可以对两个子句进行归结, C opyright © 2011 Hanspub CSA 敖友云 | 基于谓词逻辑的归结原理研究 Copyright © 2011 Hanspub CSA 53 化为相应的子句,一般步骤如下[9]: 得到归结式。设 和为两个不同的子句, 1 C2 C1 L 和2 L 分 别为 和中的两个文字且无公共变量。若 1 C2 C1 L 和2 L 存在最一般合一置换 ,则称 12 12 C L 1 L2 CC 1 C2 C 为 和的二元 归结式(resolvent),而称子句 和为归结式的亲 本子句。文字 1 C2 C C12 1 L 和2 L 称为归结式上的文字[9]。例如, 子句 P xQ y x Rf 和的二元归结式 为 ,其中 Qfy R x yPf f yx 。 1) 消去蕴涵符号 和双向蕴涵符号 。反复使 用联结词化归律,用 ,,替代公式中的 和 。 2) 减少否定符号的辖域。反复使用双重否定律、 摩根定律、量词转换律,将每个否定符号 移到仅靠 谓词的位置,使得每个否定符号最多只作用于一个谓 词。 3) 变量标准化。在一个量词的辖域内,把谓词公 式中受该量词约束的变量全部用另外一个未曾出现过 的任意变量代替,使不同量词约束的变量具有不同的 名字。 在对子句进行归结时若 1 L 和2 L 具有公共变量,则 需要先对 1 L 或2 L 中的变量进行换名,才能通过合一置 换对 和进行归结。例如, ,,是不可满足 的。 1 C CP 1 2 C x 1 CPfx 2 12 ,C SC L Px和 2 L Pf 2 x1 C分别 和中的两 个文字,若先对 2 C L 进行换名为 4) 化为前束范式。把所有的量词依顺序全部移到 公式的前面。 2 L Pfy 12 C ,则通 过对 和进行归结,得到空子句□,从而证明S 是不可满足的。归结过程中得到的归结式 是其亲 本子句 和的逻辑结论。为了证明子句集 S是不可 满足的,只要对其中可归结的子句对进行归结,并把 归结式并入子句集 S中,或者用归结式替代它的亲本 子句,然后将原问题转化为判定新子句集是不可满足 的。 1 C2 C 1 C2 C 5) 消去存在量词。利用 Skolem函数消去谓词公 式中的存在量词,将谓词公式化为 Skolem 范式。 6) 消去全称量词。消去全称量词,剩下谓词公式 中的母式部分。 7) 把母式化为合取范式。反复使用分配律把母式 化为合取范式。 8) 消去联结词 。在母式中消去所有合取联结 词,把母式用子句的形式表示出来。 9) 更改变量名称。有时称为变量分离标准化,对 子句中的某些变量重新命名,使得任意两个子句中不 出现相同的变量名。例如,下列谓词公式: 2.5. 提取子句 利用推理规则和运算法则可以将任一谓词公式转 ,,xPxyPy PfxyyQxy Py 可以转化为子句: ,PxPyPf xy 限制策略是指通过对参加归结的子句进行某些限制, 以减少归结的盲目性,提高归结的效率。常用的限制 策略包括线性归结策略、支持集策略、输入归结策略、 单文字子句策略、祖先过滤策略、语义归结策略和宽 度优先策略等。在实际应用中通常把几种归结策略结 合起来使用,以提高归结的效率和完备性。 ,Pz Qzgz Pw Pgw 2.6. 归结策略 归结过程中使用的归结策略直接影响归结的效率 和完备性。归结策略研究的是解决如何选择合适的子 句对进行归结,以尽量减少不必要的归结的问题。归 结策略大致可分为两类[9]:删除策略和限制策略。删 除策略是指在归结过程中随着归结的不断进行,子句 集中的子句越来越多,通过删除子句集中某些无效的 子句,以节省存储空间和减少搜索子句对的时间,提 高归结的效率。常用的删除策略包括重言式删除策略、 单文字删除策略、纯文字删除策略和包孕删除策略。 3. 基于谓词逻辑的归结原理的使用方法 及步骤 3.1. 证明定理 利用归结原理证明定理的过程称为归结反演 (resolution refutation)。归结反演的证明过程可以用步 骤进行描述,也可以用归结反演证明树的形式来表达 [10]。归结反演的证明步骤如下[4]: 敖友云 基于谓词逻辑的归结原理研究 54 | 1) 定义谓词并把待证明的问题的前提和结论分 别表示成谓词公式 F和G,并否定结论公式 G得到 ; G 2) 将谓词公式 F和转化为一个子句集 S; G 3) 利用归结原理对子句集 S中的子句进行归结, 并把新得到的归结式并入子句集 S中,如此反复进行, 若子句集 S中出现空子句□,则停止归结,此时 G得 证。 例如 4.1[7] 已知下列前提: (1) 马库斯(Marcus)是一个人。 (2) 马库斯是一个庞贝人(Pompeian)。 (3) 所有的庞贝人都是罗马人(Romans)。 (4) 凯撒(Caesar)是统治者(ruler)。 (5) 所有的罗马人要么忠于凯撒要么憎恨凯撒。 (6) 每个人都忠于某人。 (7) 人们仅设法暗杀他们不忠的统治者。 (8) 马库斯设法暗杀凯撒。 求证结论:马库斯憎恨凯撒。 使用归结反演的证明步骤如下: 步骤 1:定义谓词:表示 x是人; man x P ompeianx表示 x是庞贝人; R oma lo n x yalto 表示 x是罗 马人;表示 x是统治者;表示 x 忠于 y;表示 x憎恨 y; ruler x hate x ,y ,x y ,ytryassassinatex表 示x暗杀y。用谓词公式表示前提: (1) man Marcus (2) P ompeian Marcus (3) x PompeianxRomanx (4) ruler Caesar (5) , , xRoman xloyalto xCaesar hatexCaesar (6) ,xyloyaltox y (7) sin ,, xymanxrulery tryassasatex yloytaltox y (8) sin ,tryassasateMarcusCaesar 用谓词公式 G表示结论: ,hateMarcusCaesar 并用谓词公式 表示结论的否定: G (9) ,hateMarcus Caesar 步骤 2:将上述前提谓词公式和结论谓词公式 G 的否定转化为子句集。 (1) man Marcus (2) P ompeian Marcus (3) P ompeianxRomanx (4) ruler Caesar (5) , , R omanxloyalto xCaesar hatexCaesar (6) ,loyalto x fx (7) sin , , manxrulerytryassasatex y loytaltox y (8) ,tryassassinateMarcusCaesar (9) ,hateMarcus Caesar 步骤 3:利用归结原理对对上述子句集进行归结 推理。 (10) R omanMarcus ,Marcus Caesarloyalto (9)与(5) 归结, M arcus x (11) P ompeian Marcus ,Marcus Caesarloyalto (10)与(3) 归结, M arcus x (12) ,loyaltoMarcus Caesar (11)与(2)归结 (13) man Marcusruler Caesar ,sinateMarcus Caesartryassas (12)与(7) 归结, , M arcus x Caesary (14) ruler Caesartryassassinate , M arcus Caesar (13)与(1) 归结 (15) ,tryassassinateMarcusCaesar (14)与(4) 归结 (16) □ (15)与(8)归结 上述归结推理使用了线性归结策略,即每次归结 得到的归结式直接参加同另一个子句进行的下一次归 结,线性归结策略具有完备性。 3.2. 提取问题答案 归结反演不仅可以用于定理证明,而且可以用来 提取问题的答案,其思想与定理证明类似,但具体有 不同的方法。 3.2.1. 保留合一信息法 在归结反演的过程中,通过保留使用的合一置换 信息,以便在归结反演结束时提取问题的答案。 C opyright © 2011 Hanspub CSA 敖友云 基于谓词逻辑的归结原理研究55 | 例如 3.2 如果艾伦(Allen)在哪里 Fido 就跟到哪 里,那么艾伦在图书馆,Fido 会在哪里? 使用保留合一信息法提取问题答案的步骤如下: 步骤 1:定义谓词: ,ATxy表示 x在y处。 前提:(1) ,,xATAllen yATFido y (2) ,ATAllenlibrary 结论 G: , Z ATFido Z 结论的否定 :(3) G , Z ATFido Z 步骤 2:将上述前提谓词公式和结论谓词公式 G 的否定转化为子句集。 (1) ,,ATAllen yATFidoy (2) ,ATAllenlibrary (3) ,ATFido Z 步骤 3:利用归结原理对对上述子句集进行归结 推理。 (4) (3)与(1) 归结, ,ATAllen y y Z (5) □ (4)与(2)归结, library y 然后利用归结反演过程中保留的合一信息提取问 题答案,其过程如下: ,ATFidoZ yZ ,ATFido y library y ,ATFido libr ary,ATFidolibr ary ,由语句 便可得 Fido 在图书馆。 3.2.2. 目标公式否定的子句的重言式法 这种方法在两个方面对归结反演的证明过程进行 了修改[10]:一个是并入子句集 S的是目标公式否定的 子句与目标公式的子句的析取式,而不是目标公式的 否定的子句;另一个是,在求得目标语句时就停止归 结,而不是要等到出现空子句。对于例 3.2 采用这种 方法提取问题答案的步骤如下: 步骤 1:定义谓词: ,ATxy表示 x在y处。 前提:(1) ,,xATAllen yATFido y (2) ,ATAllenlibrary 结论 G: , Z ATFido Z 结论的否定 :(3) G , Z ATFido Z 步骤 2:将上述前提谓词公式和结论谓词公式 G 的否定转化为子句集。 (1) ,,ATAllen yATFidoy (2) ,ATAllenlibrary (3) ,,ATFido ZATFido Z 步骤 3:利用归结原理对对上述子句集进行归结 推理。 (4) ,ATAllen yATFidoy , (3)与(1)归结, y Z (5) ,ATFido library (4)与(2)归结, library y 由语句 ,ATFido library可得 Fido 在图书馆。 3.2.3. 目标公式否定的子句与谓词 ANSWERZ的 析取式法 这种方法也在两个方面对归结反演的证明过程进 行了修改:一个是并入子句集 S的是目标公式否定的 子句与谓词 ANSWER Z的析取式,而不是目标公式 的否定的子句;另一个是,在求得答案 Z时就停止归 结,而不是要等到出现空子句。对于例 3.2 采用这种 方法提取问题答案的步骤如下: 步骤 1:定义谓词:表示 x在y处。 ,ATxy 前提:(1) ,,xATAllen yATFido y (2) ,ATAllenlibrary 结论 G: , Z ATFido Z 结论的否定 G :(3) , Z ATFido Z 步骤 2:将上述前提谓词公式和结论谓词公式 G 的否定转化为子句集。 (1) ,,ATAllen yATFidoy (2) ,ATAllenlibrary (3) ,ATFidoZANSWERZ 步骤 3:利用归结原理对对上述子句集进行归结 推理。 (4) ,ATAllen yANSWERZ (3)与(1)归结, y Z (5) ANSWER library (4)与(2 )归结, library y 所以本题的答案为 Fido 在图书馆。 4. 结束语 谓词逻辑是一种有效的知识表示方法和高级知识 推理工具。它既有严格的理论基础,又能在机器上处 理精确性知识,而它的表达方式和人类自然语言又非 常接近。因此,用谓词逻辑表示知识容易为人们所理 解和接受。Robinson归结原理是一种可以在机器上机 C opyright © 2011 Hanspub CSA 敖友云 | 基于谓词逻辑的归结原理研究 Copyright © 2011 Hanspub CSA 56 械实现的逻辑推理技术,是实现自动推理证明的主要 途径。本文分析了基于谓词逻辑的归结原理的基本思 想、相关的推理技术及归结策略,并通过实例讨论了 利用基于谓词逻辑的归结原理证明和求解问题的方法 及步骤。研究基于谓词逻辑的归结原理在机器上的实 现技术;利用基于谓词逻辑的归结原理证明和求解一 系列实际生活或生产中的问题;进一步扩充基于谓词 逻辑的归结原理并用于处理不确定性知识等都是有意 义的研究方向。 参考文献 (References) [1] C. L. Ch ang, R. C. Lee. S ymbolic log ic and mec hani cal t heorem provi ng. New York: Acad em ic Press , 1973. [2] 卢延鑫. 经典逻辑 在人工 智能 知识推 理中 的应用[J]. 软件导 刊, 2008, 7(1): 22-24. [3] 潘美芹, 丁志军, 王永丽. 谓词逻辑推理中证明方法的判定 [J]. 山东科技大学学报(自然科学版), 2005, 24 (4 ): 84-86. [4] J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 1965, 12(1): 46-54. [5] 肖启莉, 肖启敏. 归 结原理 及其应用 [J]. 计算机与数字工程, 2007, 35(5): 183, 187. [6] 杨球, 孙宝林. 归结原理及其在数学定理证明中的应用[J]. 武汉交通科技大学学报, 2000, 24(4): 417-420. [7] E. Rich, K. Knight. Artificial intelligence (Second Edition). New York: McGraw Hill, 199 1. [8] 刘云霞, 王迤冉, 宋玉杰. 谓词逻辑描述下的归结推理方法 [J]. 周口师范学院学报, 2003, 20(2): 63-66. [9] 王文杰, 史忠植. 人 工智能 原理辅导 与练习[M]. 北京: 清华 大学出版社, 2007. [10] D. Luckham, N. J. Nilsson. Extracting information from resolu- tion proof trees . Artificial Intelligen ce, 1971, 2(1): 27-54. |