基于谓词逻辑的归结推理系统。

简介：
该项目涉及人工智能实验，旨在根据提供的公式集合和目标子句，生成归结树。经过我近五天的努力，最终得以完成，现分享给大家以供参考。关于代码方面，如果您有需求，可以通过联系我获取。以下提供一个用于测试的示例：假设“所有不贫穷且聪明的人都快乐”。并且已知“那些看书的人都是聪明的”，同时又了解到“李明能够看书且不贫穷”。此外，“快乐的人过着激动人心的生活”。现在，我们需要验证“李明过着激动人心的生活”这一结论。公式如下： $(\x)(~Poor(x)∧Smart(x)→happy(x))$ $(\x)(Read(x)→Smart(x))$ $Read(Li)∧~Poor(Li)$ $(\x)(happy(x)→Exciting(x))$ $Exciting(Li)$ 目标公式直接位于最后一行，无需添加否定符号。