明的有效方法， 前推和后推两种思维方法也适用于其他逻辑系统的 自动证明。
关键 词 ：命 题逻 辑 ；启发 式方 法 ；试探 法 ； 自 然推 理 法 ；可 读证 明 中 图分类 号 ：Ｔ １１ Ｐ８ 文献标 志码 ：Ａ 文章编 号 ：１０ —６５ ２ １）２４ ２．４ ０ １３９ （０ １ １—４９０
ＧＵ ａ ． ｕ Ｏ Ｙｕ ｎ ｈ ａ
（ ｃｏｌｆＡ ｔｍ ｔ ｎ ｎ ｅｓｙｏ ｌ ｔ ｎｃＳｉ ｃ Ｔｃｎ ｌ ｙｏ ｈｎ Ｃ ｅｇ ｕ６ ３ ， ｈｎ ） Ｓｈｏ ｏ ｕｏ ａｉ ，Ｕ ｉ ｒｔ Ｅｅ ｒ ｉ ｃ ｎｅ＆ ｅ ｏｏ Ｃ ｉ ｏ ｖ ｉ ｆ ｃｏ ｅ ｈ ｇｆ ａ， ｈｎｄ １７ Ｃ ｉａ １ １
１ 相 干命题 逻辑 系统
系统 中的联结 词一 解释 为相 干蕴涵 。相 干蕴涵不仅 顾及
别是 ： 假设规则 、 引入规则一，蕴涵消去规则一Ｅ、 复规 蕴涵 、 重
则、 重述规则 、 析取 引入规则 Ｖ， 析取消去规则 ＶＥ、 、 合取 引入
规则 ＾ 、 ，合取消去规则 ＾ 、 Ｅ 分配规则 、 引入 规则 一 、 否定 ，换质
ｌ ㈨ Ａ
１ Ａ ０ （ ６
形式定理 （ 括公理 ） 证 明结 束 ， 包 ， 否则转 下一 步 ； 立 Ａ和各 建 推 理规 则的映射 表 ， 根据 推理规 则将 Ａ “ 分解 ” 或转换 。对于
“ 分解” 或转换得到 的新 的公式 ， 重复 以上两个步骤 ， 当最 终的 新公式 是已知定 理和前提时 ， 得证 。 可见 ， Ａ的求证 可以归结为对一个 或两个新公 式 （ 对 记为
Ａ只有一个孩子 Ｂ， Ａ的左孩子为空 ， 则 右孩子为 Ｂ。对 Ｂ和 ｃ 的求证 又可以归结为另外的新 公式 ， Ａ的求 证过程 可以视做 以
计 算 机 应 用 研 究
第２ ８卷
ｏｅ ， ｒｌ Ａ）系统 Ｎ （ Ｒ中的定理 Ａ记为 Ｉ Ａ 一 。对 系统 Ｎ Ｒ的详细
描述参 见文献 ［ １ 。 １ ］
元素使用推理规则产生新公 式加入 Ｐ， 直到得 到 且 ，Ａ） （ 为 空。若 Ａ得证 ， 就得到以 Ａ为根节 点的证 明树 。算法根据系统 Ｎ Ｒ的 １ ３条推理规贝 产 生新公式 ， ０ 具有 正确性 。 自然推理 系统 Ｎ Ｒ是完备 的 ， 由于初始假 设公式集合 中只包 含公式 的子公 但
ｌ ㈦ Ａ
Ｉ 。 （Ａ＾ ６ ＝ ）
，
（
）ａ －） Ｕｂ （ ｎ
（ ｈ ａ ｂ ｛） １ Ｕ －ｎ ）
图 ２ 换质位规则情形 １
图 ３ 换 质 位 规则 情 形 ２
３３ 序 列 整理 ．
日和 Ｃ 的求证 ， ） 与新公式构成二叉树 中的父子节点关 系。若
ｄｉ１ ．９ ９ ｊｉ ｎ １０ —６ ５ ２ １ ．２ ０ ７ ｏ：０ ３ ６ ／．ｓ ． ０ １３ ９ ．０ １ １ ．０ ｓ
Ｈｅ ｒｓ ｃ ｍｅｈ ｄ ｏ ｅ ｅａｉ ｇ ｒ ａ ａ ｌ ｒ ｏｓｉ ｒｐ ｓｔ ｎ ｌｌｇｃ ｕ ｉｔ ｔ ｏ ｓｆｒｇ ｎ ｒｔ ｅ ｄ ｂｅ ｐ ｏ ｆ ｎ ｐ ｏ ｏ ｉ ｏ ａ ｏ ｉ ｉ ｎ ｉ
可读证 明的成 就主要在几何 方面。受手工证明的启发 ， 文将 本 探讨后推试探 法和前推 自然推理法 实现 相干命 题逻 辑系统
的可 读 证 明 。
１ ２ 自然推理 系统 Ｎ ． Ｒ 自然演绎逻辑的创 始人 是 德 国逻 辑学 家 Ｇ ｎ ｅ ｅｔ ｎ和波 ｚ
兰逻辑学 家 Ｊｓｏ ｓｉ两人都认 为 自然演绎 的核 心是 引入似 ａｋｗ ｋ ，
系统 Ｒ的公理 、 推理规则 和导 出规则 可 以参考文 献 ［ １ ， １ ］
在此 不 一 一 列举 。
不 同的逻辑 系统各 有优 劣 ， 侧重 点都 在 于判定 而 不是 可读证 明。一些著名 的科 学家认 为 ， 机器证 明的基本思想是 以量 的复 杂代替质 的困难 ， 凶此机器 生成 可读 证 明有相 当的难度 ， 目前
（ ）～、 一 、 、 ， 别解 释 为否 定词 、 取 词 、 干蕴 ｂ Ｖ、 （ ） 分 析 相
涵、 左括号 和右括号 ， 中否定词和析取词是真值联结词 。 其
ｂ 形成规则 ： ） （ ） ．Ｐ ， ａｐ ， …是公式 ； （ ） Ａ和 Ｂ是公式 ， ～ （ ｂ若 则 Ａ、ＡＶＢ 和 （ —Ｂ 是公式 。 ） Ａ ）
设然后撤除假设的做法 。公 理系统的证明过程是从 公理出发 ，
根 据 少 量 的 推 理 规 则 推 出一 系 列 定 理 。与 之 不 同 ， 自然 演 绎 系
统可 以没有公理 ， 而是通过 引入假设作 为推理 的出发点 。系统 Ｎ Ｒ是公理 系统 Ｒ对应 的 自然 推理 系统 ， １ 其 ３条推理 规则 分
收 稿 日期 ：２ １ 一５２ ；修 回 日期 ：２ １－６ ２ ０ １Ｏ ． ３ ０ １Ｏ —７
作者简介 ： 郭远华 （９８ ）男 ， １７－ ， 湖北天 门人 ， 博士， 主要研 究方向为 自 动推理 、 神经 网络 、 图像处理（ｙｕ２０＠１６ｃｒ ｇｈａ０３ ２ ．ｏ ） ｎ
・
４３ ・ ４０
国传统数 学中的机械化思想出发 ， 创立 丁几何定 理机器证明的 吴方法 Ｊ ｈ ｕ等人 在 １９ 。Ｃ ｏ ９２提出了基于几何不变量 的消
才得 以避免形形色色 的蕴涵怪论 。相干命题 逻辑 系统的主要 代表是系统 。
１ １ 相干命题 逻辑系统 只 ． ａ 初始符号 ： ）
（ ） ．Ｐ ， ， ａｐ ， … 解释 为可数个命题变元 ；
Ａｂ ｔ ａ ｔ Ｔ ｉ ｐ ｐ ｒｄ ｓ ｕ ｓ ｄ ａ ｔｍａ ｅ ｌ ｅ ｅ ａ ｉ ｇ ｒａ ａ ｌ ｒｏ ｓｆｒｒ ｌ ｖ ｎ ｅ ｐ ｏ ｏ ｉ ｏ ａ ｏ ｉ ｓ ｓｅ Ｔ ｉ ａ ｅ ｓ ｒ ｃ ： ｈ ｓ ａ ｅ ｉ ｓｅ ｕｏ ｔ ｄ ｙｇ ｎ ｒｔ ｅ ｄ ｂｅ ｐ ｏ ｆ ｏ ｅ ｅ ａ ｃ ｒ ｐ ｓｔ ｎ ｌ ｇ ｃ ｙ ｔ ｍ Ｒ． ｈ ｓｐ ｐ ｒ ｃ ｎ ｉ ｌ ａ ｏ ｔｄ ｐ ｏ ｅ ｍｅｈ ｄ ａ ｄ ｎ ｔ ｒｌｄ ｄ ｃ ｉｎ ｍｅｈ ｄ， ｈ ｃ ｉ ｌｔ ｄ ｈ ｍａ ｎ ｏ ｗ ｒ ｎ ａ ｋ ａ ｄ ｒ ｓ ｅ ｔ ｅｙ． ｒ ｂ ｄ ｐｅ ｒ ｂ ｔ ｏ ｎ ａｕ ａ ｅ ｕ ｔ ｔ ｏ ｗ ｉｈ ｓｍｕ ａｅ ｕ ｎ ｍｉｄ ｆｒ ａ ｄ ａ ｄ ｂ ｃ ｗ ｒ ｅ ｐ ｃ ｉ ｌ ｐ ｏ ｅ ｏ ｖ ｍｅｈ ｄ ｂ ｃ ｗ ｒ ｅ ｏ ｏ ｅ ｏ ｍｕ ａ ｃ ｏ ｄ ｎ ｅ ｕ ｔ ｎ ｒ ｌ ｓ ａ ｄ ｎ ｔ ｒ ｌ ｅ ｕ ｔ ｎ ｍｅ ｈ ｄ ｆ ｒ ａ ｄ ｇ ｎ ｒ ｔｄ ｎ ｗ ｆ ｒ ． ｔ ｏ ａ ｋ ａ ｄ ｄ ｃ ｍｐ ｓ ｄ ｆ ｒ ｌ ｓａ ｃ ｒ ｉｇ ｄ ｄ ｃｉ ｕ ｅ ． ｎ ａｕ ａ ｄ ｃ ｉ ｔ ｏ ｏ ｒ ｅ ｅ ａｅ ｅ ｍｕ ｏ ｄ ｏ ｗ ｏ １ ｓｆｏ ｈ ｐ ｔ ｅ ｉ ｓ ｔ ｃ ｏ ｄ ｎ ｅ ｕ ｔ ｎ ｒ ｌ ｓ Ｔ ｉ ｐ ｐ ｒ ｂ ａｎ ｄ ｒ ａ ａ ｌ ｒ ｏｓｆｒｒ ｌｖ ｎ ｅ ｐ ｏ ｏ ｉ ｏ ａ ｇｃ ｓ ｓ ｍ ａ ｒｍ ｙ ｏｈ ｓ ｅ ｃ ｒ ｉ ｇｄ ｄ ｃ ｉ ｕ ｅ ． ｈ ｓ ａ ｅ ｔ ｉ ｅ ｅ ｄ ｂ ｅ ｐ ｏ ｆ ｏ ｅｅ ａ ｃ ｒ ｐ ｓｔ ｎ ｌ ｏ ｉ ｙ ｔ Ｒ ｓ ａ ｏ ａ ｉ ｌ ｅ ｂ ｗ ｔ ｏ ｓｒ ｓ ｅ ｔ ｅｙ ａ ｄ ｃ ｍｂ ｎ ｎ ｅ ｙｔ ｏ ｍｅｈ ｄ ｅ ｐ ｃ ｉ ｌ ｎ ｏ ｉ ｉ ｇｔ ｍ．Ｐ ｏ ｅ ｍｅｈ ｄ ａ ｄ ｎ ｔ ｒ ｌ ｅ ｕ ｔ ｎｍｅｈ ｄ ａ ｅ ｅｆｃｉ ｅｆｒｇ ｎ ｒ ｔ ｇｒ ａ — ｖ ｈ ｒ ｂ ｔ ｏ ｎ ａ ｕ ａ ｄ ｃｉ ｔｏ ｒ ｆ ｔ ｏ ｅ ｅ ａｉ ｅ ｄ ｄ ｏ ｅ ｖ ｎ ａ ｌ ｒ ｏ ｓ Ｆ ｒ ａ ｄ ｄ ｄ ｃｉｎ ａ ｄ ｂ ｃ ｗａｄ ｄ ｄ ｃｉｎ ａ ｅ ａｓ ｕｔ ｂｅ ｆ ｒａ ｔｍａｅ ｅ ｓ ｎ ｎ ｎ ｏｈ ｒｌｇｃ ｓ ｓｅ ． ｂ ｅ ｐ ｏ ｆ． ｏ ｒ — ｅ ｕ ｔ ｎ ａ ｋ ｒ — ｅ ｕ ｔ ｒ ｌｏ ｓ ｉ ｌ ｕｏ ｔ ｄ ｒ ａ ｏ ｉｇ ｉ ｔ ｅ ｏ ｉ ｙ ｔ ｍｓ ｗ ｏ ｏ ａ ｏ Ｋｅ ｒ ｓ ｙ ｗｏ ｄ ：ｐ ｏ ｏ ｉ ｏ ａ ｌｇ ｃ ｈ ｕ ｉｔ ｔ ｏ ； ｐ ｏ ｅ ｍｅｈ ｄ ｎ ｔ ｒ ｌ ｅ ｕ ｔ ｎ ｍｅｈ ｄ； ｒ ａ ａ ｌ ｒｏ ｓ ｒｐ ｓ ｉｎ ｌ ｏ ｉ ； ｅ ｒｓ ｃ ｍｅｈ ｄ ｔ ｉ ｒ ｂ ｔｏ ； ａ ｕ ａ ｄ ｃ ｉ ｔ ｏ ｄ ｏ ｅ ｄ ｂｅ ｐ ｏ ｆ
点法 ， 实现 了自动生成 几何定 理 的可读证 明 ， 文献 ［ ］ 述 丫 ７详
其算 法实现。
逻辑 自动证 明的成 果更 加 丰富。２ ０世 纪 ５ ０年代 的代 表 性成果有逻辑理论 机和王浩 算法 。逻辑判定方 法主要有 Ｄ Ｐ
方法 、 归结 方法 、 义表方法 、 语 相继式方法等 ’ 。这 些方法对 “
郭远华
（ 电子科技 大学 自 动化工程学院， 成都 ６ １３ ） １７ １
摘 要 ： 讨 了 自动生 成命题 逻辑 系统 的 可读证 明 。采用试 探 法 和 自然推 理 法分 别从 前推 和 后推 模 拟人 类 探
思维 求证 ， 试探 法根据 推理规 则将 待证 公 式反 向分解 ， 自然推 理 法从 假 设 出发 根 据推 理 规 则 生成新 的公 式。 两 种 方法都 实现 了相 干命题 逻辑 系统 的 可读证 明 ， 结合 实现 了混 合证 明。试探 法和 自然推理 法是 生成可读 证 并
２ 系统 只的后推证明
２ １ 后推试探算法 ． ，
式 ， 以实现算 法不具备完备性和终 止性 。在初始假设数量为 所 ｎ证 明树 的深度 为 ｈ的情况下 ， 法复杂度 为 ｎ 、 算 “。