北京航空航天大学离散数学课件4.第四章 归结法.pdf

离散数学(1): 数理逻辑 Discrete Mathematics (1): Mathematical Logic 第四章 归结法 赵永望 zhaoyw@buaa.edu.cn 北京航空航天大学计算机学院 内容 • 3.0. 归结法简介 • 3.1. 命题逻辑的归结法 • 3.2. 前束范式和斯科伦范式 • 3.3. 谓词逻辑的归结法 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 2 简介 • 自动推理早期的工作主要集中在机器定理证明。 • 机械定理证明的中心问题是寻找判定公式是否是有 效的通用程序。 • 对命题逻辑公式，由于解释的个数是有限的，总可 以建立一个通用判定程序，使得在有限时间内判定 出一个公式是有效的或是无效的。 • 对一阶逻辑公式，其解释的个数通常是任意多个， 丘奇（A.Church ）和图灵（A.M.Turing ）在1936 年证明了不存在判定公式是否有效的通用程序。 – 如果一阶逻辑公式是有效的，则存在通用程序可以验 证它是有效的 – 对于无效的公式这种通用程序一般不能终止。 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 3 简介 • 1930年希尔伯特为定理证明建立了一种重要方 法，他的方法奠定了机械定理证明的基础。 • 开创性的工作是赫伯特·西蒙 （Herbert A. Simon）和艾伦·纽威尔 （Allen Newell ）的Logic Theorist 。 • 机械定理证明的主要突破是1965年由鲁宾逊 （John Alan Robinson ）做出的，他建立了所 谓归结原理，使机械定理证明达到了应用阶段。 • 归结法推理规则简单, 而且在逻辑上是完备的, 因而成为逻辑式程序设计语言Prolog的计算模 型。 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 4 简介 • 判断一个公式是否为永真式 • 命题逻辑 – 可判定, 用真值表即可计算, 但当命题变元较多 时, 效率低 – 更实用得到方法——归结法 • 谓词逻辑 – 归结法是一个部分终止的算法 – 当输入语句是永真式时, 判断算法终止并给出 正确答案 – 当输入语句不是永真式时, 判断算法可能不终 止, 因而得不出结论 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 5 内容 • 3.0. 归结法简介 • 3.1. 命题逻辑的归结法 • 3.2. 前束范式和斯科伦范式 • 3.3. 谓词逻辑的归结法 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 6 基本原理 • Q ,…,Q ╞R，当且仅当Q …Q R不可满足 1 n 1 n • 证明Q ,…,Q ╞R 1 n – (1) Q …Q R化为合取范式； 1 n – (