原 创 性 声 明本人声明:所呈交的硕士学位论文，是本人在指导教师的 指导下，独立进行研究工作所取得的成果。除文中己 经注明引 用的内容外， 本论文不包含任何其他个人或集体己经发表或撰 写过的作品成果。对本文的研究做出重要贡献的个人和集体， 均已 在文中以明确方式标明。 本人完全意识到本声明的法律结 里 h 太人 7 -k 相_学 位 论 文 作 者 签 名 : 均奔务日期:; ?- “ 3 年5月 / ， 日关于论文使用授权说明本人同意学校有权保留并向国家有关部门送交学位论文 的 复 印 件 ， 允 许 论 文 被 查 阅 和 借 阅 ( 同 氢 不 同 意 ) 学 校及国家有关机构有权公布论文的全部或部分内容，并采用影 印、 缩印或其他复制手段保存论文。论 “ 作 者 签 “ : 汤 料指 导 教 师 签 名 : b t A日期: y o o 4 . 0 5 . 1 0 日期: ? w 3 . G s- , ! o内 容 提 要定理机器证明是许多基于逻辑的 推理系统的核心，因此提高自 动定理证明系统 的 效率具有重要的意义，表方法由于其适用于非经典逻辑的推理而受到 重视，结合 了 其它推理方法中的剪枝技术的表方法， 在解决一阶逻辑的问 题时也显示了很强的 优势。本文从实 现一个高效的系统出发。 对表方法进行了深入细致的分析，设计并 实现了基于 表方法的一阶定理证明系统。本文首先概述了 表方法的发展，详细分析 ， 了 用于连接表方法的各种剪枝技术，井着重给出了 本文所实现系统中 使用的超表方 ; 法和采用s u p e r p o s i t i o n 方法的 超表方法。 本文还介绍了 基于表方法的定理证明系 统的 丧 计 与 实 现 ， 并 以T P T P 问 题 库 中 的 问 题 对 系 统 进 行 了 测 试 。 铡 试 结 果 表 明 该 系 .统能够在给定的时间内证明大部分输入公式的不可满足性，该系统和一些著名的 A T P 系统在速度上的差异表明该系统还需要加强剪枝技术的应用.第一童 引言第一章 引言1 . 1 研究背景及意义在人工智能应用的许多方面，例如演绎数据库和基于模型的诊断等应用中， 其 知识表示方法采用的都是基于逻辑的方法，这些应用系统的推理部分都要求能够判 断在给定的逻辑框架中，某个结论是否成立。由此，定理机器证明实现效率的提高 对于提高这些应用系统的性能具有重要的意义。每年一次的自 动演绎会议 ( C A D E )旨 在交流在自 动演绎的各方面的 最新进展， 为了促进自 动定理证明 ( A T P ) 系统的发展，同时亦举行 C A D E 自 动定理证明系统 竞赛 ( C A S C ) 来评价正确的、 全自 动的、 经典的一阶逻辑A T P 系统。 C A S C中出 现 了各种高效的证明系统。例如基于归结方法的 。 t t e r，基于表方法的 E 0 . 6和 E - S E T H E O c s p 0 2 等. 表 推 理方 法由 于 其 推理规 则 简单. 不 要求输 入的 公 式 一定 是 合 取范式，因而适用于合取范式形式复杂的非经典逻辑，由 此受到重视，但用于经典 一阶逻辑时却效率不高。 将其它推理方法中提高效率的技术引入到子句表中，得到 的基于表方法的一阶定理证明器在性能上可以 和基于归结方法的一阶定理证明 器相媲美。上个 世纪 九十 年代以 来，出 现了 一些高效的 基于表方 法的 定理证明 系 统， 它们有:德国慕尼黑工业大学的D C T P 非连接方法的表证明器)和S E T N E O -,德国卡尔鲁厄大学的3 r .W 和L E A N T A P ,前者用于多值逻辑问 题，同 时可以 处理含 等词的一阶逻辑问题，后者是用于非经典逻辑的 表证明器。1 . 2 本文主要工作本文以 研究定理证明中的表方法并加以 实现为目 标， 研究了用于改进表方法的 各种剪枝技术，设计实现了基于表方法的一阶定理证明系统。该系统采用面向 对象 的 程序设计方法， 采用C +语言实 现， 实现了 对搜索过程的更精确的 控制。 系统具 有灵活的控制性、可移植性、可扩充性等特点。该系统通过实现超表演算来证明一 阶 逻 辑公 式的 不 可 满 足 性， 通过 采用s u p e r p o s it io n 方 法的 超 表方 法来 证明 含等 词的 一 阶逻辑公式的 不可满足性.本文第二章介绍了 表方法发展的历史及应用于子句表的各种剪枝技术:第三 章 详 述了 系 统 的 两 个 模 块的 关 键 技 术: 超 表 演 算 和s u p e r p o s i t io n 方 法以 及 其中 用 到的 广 义公式技术; 第四章首先给出了基于表方法的定理证明系统的设计， 然后讨论了系 统实现的相关技术，并用实验测试数据说明了系统的性能指标;最后是结语和工作展望。第二童 基于表方法的一阶定理证明第二章 基于表方法的一阶定理证明2 . 1 表方法的发展表方法是将所要证明的公式的语法结构和语义结合起来的 证明方法， 证明过程 直观、易于理解. 表方法不要求输入的公式一定是合取范式形式，因而适用于合取 范式形式复杂的非经典公式的不可满足性证明， 这也是表方法受到重视的原因之一。 然而，以一般公式形式为输入的表方法用于一阶逻辑公式的证明时，效率和其它证 明方法相差很多，后来出 现了以 合取范式形式为输入的表方法以及一些改进技术， 以此为基础的一阶定理证明器在速度上超过了基于归结方法的证明器。2 . 1 . 1 基本的表方法一 阶 逻 辑公 式 按照 其 语法结 构可以 分为以 下四 类m0铆A，X，Ya、a:，X，Yx Y 一 Y XB ， ( x n Y )x V YX 一 Y，xxxX 八 Y ，( xV Y )， ( X一 )Y )， ，X￥丫( a ) b b ( a )( Vx ) P ( x ) P ( a )( 日 x ) P ( x ) P ( a )，( 3 x ) P ( x )，P ( a )、( d x ) P ( x )， P ( a )令S = S i, ， S a 是 一 阶 逻辑公 式的 集合， 其 中S j( 1 1 一 规则:如果存在一个。 类型的公式在分枝 B 上， 那么生成结点n的唯一 儿子结点n , ， 结点n L 的唯一儿子结点 处 ，分别令该公式的Q L 和a ， 子公式为结点 n .和n 2 的相关公式。2 . 0 规则:如果存在一个e 类型的公式在分枝B 上， 那么生成结点n 的两个 儿子结点n ， 和m ， 分别令该公式的p ， 和p : 子公式为结点n , 和n的相关公式。3 . Y 规则:如果存在一个Y 类型的公式在分枝B 上， 那么生成结点 n 的唯一一 2-第二章 基于表方法的 一阶定理证明儿子结点n , ， 令该公式的Y ( a ) 子公式为结点n , 的相关公式， 其中a 可以 取值为任意 的项。4 .占 规则:如果存在一个6 类型的公式在分枝 B 上，那么生成结点n的唯一 儿子结点n ， 令该公式的8 ( a ) 子公式为结点n : 的相关公式， 其中a 是一个从未在当 前的树的结点中出现过的常量.对于分枝B 和在B 上的公式5 ，如果S 是Y 类型的公式。那么可以 在分枝B 上 对S 应用Y 规则任意次，否则，只能对S 应用相应的规则一次。分枝B 称为是封闭的， 如果有公式S 和，S 都在分枝B 上. 表T 称为是封闭的， 如果T 的树的所有分枝都是封闭的。如果一阶逻辑公 式的 集合S 是不可满足的， 那么一定存在一个S 的 封闭的表T 一场, 其中 G“ 二L , V . . . . . . V i - , ( 1 称为S 中的文字出现。子句公式集合 S是恰当的.如果不存在集合中一个公式是集合中另外一个公式 的子公式的情况，而且S 中不包含重言式。对于有n 个元素的恰当的子句公式集合5 ，5 的一个路径是n 个文字出现，分别 来自 不同的公式。S 的路径的任何子集称为S 的子路径。 S 的连接是S 的一个两个元 素的子路径( , 1 , 其中x 和L 是有相同 谓词符号的 文字， 一个 文字是负文字，另外一个不是。 连接中的文字出 现互为对方的对偏，此时，子句 c : 和C z 称为 连接的。 S 的 路径或子路径称为互补的， 如果它包含一个连接做为子集， 且 连接中的文字有相同的原子。如果恰当的子句公式集合 S的所有路径都是互补的，则S 称为是互补的.命题D I : 恰当的 基 子句公式集合S 是不 可满 足的， 当 且仅当S 是互补的。例如， 对于不可满足的基子句公式集合 S = ( P ,， P V Q ,，Q ， 它的两条路径是 ( , , 和 , , ) ， 这两条路径都第二章 荃于表方法的一阶定理证明是互补的， 所以s 是互补的。有多种 方法检查 路径的 互补性，比 如最自 然的 就是使用表 方法。连接方法的另外一个重要原则就是使用连接的集合作为路径检查的 控制机制， 这一点在表方法中 没有对应的部分。连接表将连 接 做为 一种 路径 检 查的 控 制结 构，由 此3 f 出了 连 接 表(3子句表T ， 如果T的 每个非根结点的非叶结点N 都有一个结点N 做为其后继 结点之一， 其中 结点N 的相关文字和结点N 的相关文字是互补的，则T 为连接表。命题(3 : 如果基 子句公 式集合s 不 可满足， 那么存在s 的 封闭 的 连接表.然而， 连接表演算却不是证明流畅的，为了 得到封闭的表， 需要进行回溯。强连拱一 个 连 接 , 称为 强的(9 ( 或强 连 接) ， 如果L = - K 并且K 是C : 中唯一在C ， 中 有互补文字的 文字。强连接中的文字出 现互为彼此的 强对偶。 两 个子句公式是强连接的，如果它们是连接的，并且它们间的所有连接都是强的。对于子句来说， 强连接可以 如下解释:如果 C , ”和 C 3 分别是包含基子句公式 C . 、C r 中出 现的所有文字的子句，那么 C ， 和 C Y 的强连接意味着 C , 和 C : 只有一个 基归结式C , C不是重言式。子句表丁 称为是强连接的 ( 或强连接表) ，如果 T 是连接的。并且对于任何两个 相邻的表子句公式C 】 和c Z ，它们都是强连接的。子句表T 中 表子句公式C , 和C 称为是相邻的。 如果子句C , 和C z 分别是表的某个 分枝上相邻两个结点的相关文字所在的子句。命 题， : 强 连 接 与 正 规 性 相 容。例如， 两个子句公式 P ( a ) V - Q ( a ) VP ( b ) V P ( a ) 和， P ( a ) V - Q ( a ) V - Q ( b ) V，P ( a ) V，Q ( b ) V， P ( a ) 是强连接的。2 . 2 . 2 连接表的剪枝下面介 绍的 几种剪枝技术(9 (4 ) 都是在命题逻辑中 来进行说明 的。f a c t o r i z a t i o n这种方法在模型排除和连接演算中最先提出。 在一个封闭的表中， 考虑标记有 相同文字的结点N % ,假设 N z 的所有祖先结点也是 N , 的祖先结点，那么在 N , 下面 可以 重用N 2 下面的 封闭的部分表T ，得到的仍然是一个封闭的表。N : 一般说来是N ， 的兄弟结点或者是N ， 的祖先的兄弟结点。( N , )第二章 荃于表方法的一阶定理证明注意， 上图中不能再令 N . 重用 N , 的推导部分，否则便出现循环重用，为避免 这种情况而引入了一个序关系。对于子句表T 和一个作用在其结点上的f a c t o r i z a t i o n 依赖关系包含两个最