Horn子句归结实验
摘 要
归结原理是一般逻辑推理算法的基础理论，即智能体可以通过一系列已给定的子句集，通过将两个子句归结合并的方式，判断某个结论是否成立。该原理可以被高效地应用于计算机中，是能在计算机中较好实现的一种推理技术，使得定理自动证明获得了长足进步。
在本次试验中，采用了将目标取反并入子句集，然后查看子句集能否推出空子句的证明方式，实现了一个子句集自动推出内核。该内核遵循上述二元归结规则，整体采用遍历搜索的方式推出子树，同时为了优化搜索时长，采用了包容归结策略与删除部分子句的策略。
本次实验的UI部分使用了Qt框架来实现与用户的交互，用户可以通过界面指示较为方便地进行子句集、目标语句的输入与归结过程的查看。
关键词：归结原理，包容归结，自动推理，Qt框架
Horn clause resolution experiment
ABSTRACT
Resolution principle is the basic theory of general logic reasoning algorithm, that is, agents can judge whether a conclusion is true or not by a series of given clause sets and combining two clauses. This principle can be used in computer efficiently, and it is a better reasoning technology that can be realized in computer. It makes great progress in automatic theorem proving.
In this experiment, we use the method of combining the target inversion into the clause set, and then check whether the clause set can push out the empty clause, and realize the automatic push out kernel of the clause set. The kernel follows the above binary resolution rules and adopts the way of traversal search to push out the subtree. In order to optimize the search time, the kernel adopts the strategy of containing resolution and deleting some clauses.
In the UI part of this experiment, QT framework is used to realize the interaction with users. Users can easily view the input and resolution process of clause set and target statement through the interface instructions.
Key words：Resolution principle, Inclusive resolution, Automatic reasoning, QT framework
目 录
1 实验概述 1
1.1 实验目的 1
1.2 实验内容 1
1.3 归结原理简介 1
2 实验方案设计 2
2.1 总体设计思路与总体架构 2
2.1.1 内核部分思路说明 2
2.1.2 内核部分总体架构 2
2.1.3 UI部分思路说明 3
2.1.4 UI部分总体架构 3
2.2 核心算法及基本原理 3
2.2.1 归结推理说明 3
2.2.2 反演完备性说明 4
2.3 模块设计 5
2.3.1 各模块设计说明 5
2.3.2 各模块图示说明 6
2.4 其他创新内容或优化算法 7
2.4.1 包容归结策略 7
2.4.2 “长度限制”优化策略 8
2.4.3 对E函数关键字的处理 9
3 实验过程 10
3.1 环境说明 10
3.1.1 内核部分开发环境说明 10
3.1.2 展示部分开发环境说明 10
3.2 源代码文件与主要函数清单 10
3.3 实验结果展示 12
4 总结 17
4.1 实验中存在的问题及解决方案 17
4.1.1 初次归结总是归结不出结果 17
4.1.2出现“undefined reference to 'vtable for 方法名 '的错误 17
4.2 心得体会 17
4.3 后续改进方向 18
4.4 总结 18
参考文献 19
小组分工 19
附录： 20
