Horn 子句归结

实验概述

实验目的

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

实验内容

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

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

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

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

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

为了推理需要，增加如下常识：(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

实验结果展示

基于Python实现的Horn子句归结相关推荐

Horn子句归结实验设计与实现文档+任务书+答辩PPT+演示视频+项目源码
Horn子句归结实验摘要归结原理是一般逻辑推理算法的基础理论,即智能体可以通过一系列已给定的子句集,通过将两个子句归结合并的方式,判断某个结论是否成立.该原理可以被高效地应用于计算机中,是能在计 ...
国科大高级人工智能8-归结原理和horn子句
只有一条规则的推理 resolution(消解,归结) CNF(conjunction normal form合取范式 (A∨B)∧(B∨C)(A∨B)∧(B∨C)(A∨B)∧(B∨C) 任何逻辑式都 ...
基于Python的SQLite基础知识学习
前言前一段时间偶然的看到了一个名词SQLite3,大概了解到此为一种轻量型的关系型数据库.官网介绍到SQLite是一个进程内库,它实现了一个自包含的.无服务器的.零配置的事务性SQL数据库引擎(官网 ...
基于Python实现的桌面图书管理系统
资源下载地址:https://download.csdn.net/download/sheziqiong/85610891 图书管理系统 PART 1:实验要求设计并实现一个精简的图书管理系统,要求 ...
基于Python的人脸识别方法
摘要:得益于计算机硬件技术的进步以及软件算法的不断改进,近些年来人工智能技术得到了前所未有的发展,基于深.度学习的人脸识别技术也已经得到了广泛的应用,特别是在安保.金融等需要安全系数较高的领域.提出了 ...
【CV】OpenCV（基于Python）学习笔记
以下内容中的页码均来自<OpenCV 4详解 : 基于Python> 目录第2章载入.显示与保存数据 2.2 图像的读取与显示 2.2.1 图像读取函数 cv.imread() 2.2 ...
基于Python的人工智能美颜系统
基于Python的人工智能美颜系统使用PyQt5模块搭建可视化界面,使用Dlib模型(shape_predictor_68_face_landmarks.dat)实现人脸关键点检测和定位,人脸美颜(美 ...
python深度神经网络量化_基于Python建立深度神经网络！你学会了嘛？
原标题:基于Python建立深度神经网络!你学会了嘛? 图1 神经网络构造的例子(符号说明:上标[l]表示与第l层:上标(i)表示第i个例子:下标i表示矢量第i项) 单层神经网络图2 单层神经网络示 ...
python selenium脚本_怎样开始写第一个基于python的selenium脚本
1.下载并安装python(http://www.python.org/geti/). 2.安装selenium(http://pypi.python.org/pypi/selenium)下载并解压缩 ...

基于Python实现的Horn子句归结