一、 实验题目 一阶逻辑的归结推理 二、 实验内容
- 算法原理 实验要求是编写函数实现一阶逻辑的归结推理，输入为子句集（元组的集合），输出为整个归结推理的过程，将每个归结步骤存储在一个列表中返回。 实验首先要明确的一点是：在归结推理的过程中，不同阶段应该采取什么样的数据类型存储每一个公式，子句，子句集，和实现归结推理所需的临时数据。根据作业要求，函数的输入子句集的数据类型是元组的集合，我首先将其转化成嵌套列表的数据类型，这样子句的顺序就能确定了，而且调用列表的方法也更加便捷。对应每一个原子公式，实验要求其数据类型是字符串的形式，但是字符串形式在解析公式的结构（如谓词，正负，变量，常量）的时候会非常不方便，这就需要定义一个类来表示每一个原子公式，类中包括对应的正负（0或1），谓词（字符串），参数（字符串的列表），这样能使我更加便捷的解析每一个原子公式从而进行归结，因此我还需要有将输入原子公式的字符串转变成对应类的实例的函数步骤。在返回的步骤列表中，每一个步骤以字符串的形式存储，因此还需要将公式类的实例反过来转化回原子公式的字符串。 明确的所需的数据类型，接下来的关键就是具体的归结算法了。单步归结的步骤就是从两个子句中找到相同谓词，不同正负的原子公式，去掉两个原子公式后将两个子句合并为一个（这一步可能需要用到合一，将变量用常量赋值）并加入到子句集中。反复调用单步归结直到得到空子句或者一直不产生新子句则函数终止。
- 实验分析 可以看到，整个归结步骤十分繁琐，这主要是实验要求的输出太繁琐所致，其实整个逻辑是不复杂的。用文字表达整个逻辑如下：遍历两个子句的所有原子公式，找到符合归结要求的两个原子公式（正负相反，谓词相同），然后分类讨论，如果这两个原子公式的参数也相同，则表明不需要合一，直接归结就可以了，创建一个新列表，赋值为不包括这两个原子公式的子句合并，判断在原子句集中不包含这一个新子句的情况下，将这一步的操作细节用字符串表示，加入到整个归结步骤的字符串当中。如果两个原子公式的参数不相同，说明要进行合一，要将变量赋值为常量才能使参数相同，进而继续归结，并将这一步的操作细节用字符串表示，加入到整个归结步骤的字符串当中。若得到空子句，说明归结完成，函数返回0，不然则返回1。 三个示例都最终归结得到空子句，成功完成了一阶逻辑的归结推理。但是也可以看到相较于老师给出的输出示例，归结步骤有一点多，相较于人的归结操作来看，效率确实比较低，这是因为我的算法中是直接遍历子句进行归结的，而且把所有可能的归结步骤都列出来了，然而有一些归结步骤是不需要的，这就需要对代码的选择字句归结的算法进行优化。 因为我采用的是暴力遍历的方法进行两两归结，所以效率不算高，在最坏的情况下时间复杂度是O(n^3)（n为子句集中子句的个数），因此需要改进选择两个子句的算法来降低时间复杂度。不过我暂时还没有想到有什么更好的算法。