实现基于谓词逻辑的归结原理(共23页).doc

河南城建学院人工智能实验报告实验名称：实现基于谓词逻辑的归结原理成 绩：_ 专业班级： 学 号： 姓 名： 实验日期 ：20 14 年 05 月 13日实验器材： 一台装PC机。1、 实验目的 熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。2、 实验要求对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程：(1) 谓词公式到子句集变换；(2) 替换与合一算法；(3) 在某简单归结策略下的归结。3、 实验步骤 步1 设计谓词公式及自居的存储结构，即内部表示。注意对全称量词x和存在量词$x可采用其他符号代替；步2 实现谓词公式到子句集变换过程；步3 实现替换与合一算法；步4 实现某简单归结策略；步5 设计输出，动态演示归结过程，可以以归结树的形式给出；步6 实现谓词逻辑中的归结过程，其中要调用替换