Horn 子句归结

实验概述

实验目的

熟悉和掌握归结原理的基本思想和基本方法，通过实验培养学生利用逻辑方法表示知识，并掌握采用机器推理来进行问题求解的基本方法。

实验内容

对所给问题进行知识的逻辑表示，转换为子句，对子句进行归结求解。

选用一种编程语言，在逻辑框架中实现 Horn 子句的归结求解。

对下列问题用逻辑推理的归结原理进行求解，要求界面显示每一步的求解过程。

破案问题：在一栋房子里发生了一件神秘的谋杀案，现在可以肯定以下几点事实：

1. 在这栋房子里仅住有 A,B,C 三人；
2. 是住在这栋房子里的人杀了 A；
3. 谋杀者非常恨受害者；
4. 所恨的人，C 一定不恨；
5. 除了 B 以外，A 恨所有的人；
6. 恨所有不比 A 富有的人；
7. 所恨的人，B 也恨；
8. 没有一个人恨所有的人；
9. 杀人嫌疑犯一定不会比受害者富有。

为了推理需要，增加如下常识：(j)A 不等于 B。

问：谋杀者是谁？

实验方案设计

• 总体设计思路与总体架构
• 输入事实/过程
• 将一阶逻辑语言化为子句
• 输入目标
• 调用归结法证明
• 利用置换合一，匹配目标和过程的后件，根据前件更新目标
• 目标变成空语句，结论成立
• 输出证明过程
  

核心算法及基本原理：

采用的数据结构：线性结构、数组（Python 代码里面分别用到列表和元组存储 Horn 子句和逻辑语句的函数表示）

算法：本实验并没有涉及到很复杂的算法，其过程是模拟手写推导过程，需要将 Horn 子句，输入执行 main 文件中，最主要的两个函数是 mgu(self, other, limit=None)（实现置换合一）和 resolution(self, exp: Expression)（子句归结），都是通过遍历所有子句（从数组里面取出），尝试所有可能的表达式/单元，进行置换合一和归结，其中，子句归结过程主要通过递归证明置换后的新目标，返回一条证明步骤。

关于 Horn 子句的解释：

网络查找的解释

Horn 子句可以表示出事件之间的逻辑关系，通过结合 Python 高效的处理正则语言的功能，可以简化证明过程。

关于机器推理：

机器推理（Machine Reasoning），是指基于已有知识对未见问题进行理解和推断，并得出问题对应答案的过程。根据该定义，机器推理涉及 4 个主要问题：（1）如何对输入进行理解和表示？（2）如何定义知识？（3）如何抽取和表示与输入相关的知识？（4）基于对输入及其相关知识的理解，如何推断出输入对应的输出？下图给出机器推理的整体框架：

机器推理整体框架

本次子句归结实验，总体上是依照机器推理的思路框架展开，可归类为机器推理里的基于推理的事实检测，具体推理步骤在下面依次进行展开。

模块设计：本实验的具体模块设计

两个 py 文件： main.py 为入口文件，用于输入输出，控制流程_init_.py 包含 3 个类，分别为 Unit(过程体或函数），Expression（事实，过程，目标）, Engine（归结法核心）

其他创新内容或优化算法

创新点：开始在处理非语句的时候考虑在肯定语句前加上“<-”来表示否定，例如：“A 所恨的人，C 一定不恨。”表示为“<-hate(C,*X)<-hate(A,*X)”结果这样实现起来会很麻烦，因为一个 Horn 语句中有两个“<-”，给正则语句分析造成了混淆，最后考虑在原肯定语句的基础上，在前面加上 n 表否定，如“nhate(C,*X)<-hate(A,*X)”，事实上还是一个肯定句，但语义是否定的，通过这种方法，使得证明步骤的实现方便了很多。

实验过程

环境说明：

操作系统：windows10

开发语言：Python 3.7 开发环境：PyCharm Professional 2017

核心使用库：re、copy

主要函数清单

函数名	作用域	功能	功能	功能
def is_variable(cls, arg: str) ；-> bool	Unit 类	判断事实或目标集中是否含有变量	判断事实或目标集中是否含有变量	判断事实或目标集中是否含有变量
def update_args(self, ；mapping: dict)	Unit 类	在置换的过程中替换变量	在置换的过程中替换变量	在置换的过程中替换变量
def mapping_args(self, ；other)	Unit 类	寻找可置换的过程（函数） ；self 和 other，分别需要修改什么变量，以 other 的为主	寻找可置换的过程（函数） ；self 和 other，分别需要修改什么变量，以 other 的为主	寻找可置换的过程（函数） ；self 和 other，分别需要修改什么变量，以 other 的为主
def eq(self, other)	Unit 类	判断当前事实和目标是否相等	判断当前事实和目标是否相等	判断当前事实和目标是否相等
def str(self)	Unit 类和；Expression 类	将事实集转换为字符串	将事实集转换为字符串	将事实集转换为字符串
def update_args(self, ；mapping: dict)	Expression 类	用 mapping 中的置换对，更新表达式	用 mapping 中的置换对，更新表达式	用 mapping 中的置换对，更新表达式
def ；remove_all_from_body(self, unit: Unit)	Expression 类	清除表达式中所有 unit	清除表达式中所有 unit	清除表达式中所有 unit
def clear_same_unit(self)	Expression 类	移除相同的 unit	移除相同的 unit	移除相同的 unit
def mgu(self, other, limit=None)	Expression 类		置换合一，利用过程更新目标
def mgu(self, other, limit=None)	Expression 类		self 和 other 的归结结果
def mgu(self, other, limit=None)	Expression 类		self 是目标（待证明）
def mgu(self, other, limit=None)	Expression 类
def resolution(self, exp: ；Expression)	Engine 类	实现子句归结的过程	实现子句归结的过程	实现子句归结的过程
def proof(self, exp: str)	Engine 类	返回归结过程，存到数组中，如果证明失败，则返回 None	返回归结过程，存到数组中，如果证明失败，则返回 None	返回归结过程，存到数组中，如果证明失败，则返回 None

实验结果展示