《实现基于谓词逻辑的归结原理》由会员分享，可在线阅读，更多相关《实现基于谓词逻辑的归结原理（25页珍藏版）》请在金锄头文库上搜索。
1、For personal use only in study and research; not for commercial use河南城建学院人工智能实验报告实验名称：实现基于谓词逻辑的归结原理成 绩：_ 专业班级： 学 号： 姓 名： 实验日期 ：20 14 年 05 月 13日实验器材： 一台装PC机。一、 实验目的 熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。二、 实验要求对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程：(1) 谓词公式到子句集变换
2、；(2) 替换与合一算法；(3) 在某简单归结策略下的归结。三、 实验步骤 步1 设计谓词公式及自居的存储结构，即内部表示。注意对全称量词x和存在量词$x可采用其他符号代替；步2 实现谓词公式到子句集变换过程；步3 实现替换与合一算法；步4 实现某简单归结策略；步5 设计输出，动态演示归结过程，可以以归结树的形式给出；步6 实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。四、 代码谓词公式到子句集变换的源代码：#include#include#include#includeusing namespace std;/一些函数的定义void initString(string &in
3、i);/初始化string del_inlclue(string temp);/消去蕴涵符号string dec_neg_rand(string temp);/减少否定符号的辖域string standard_var(string temp);/对变量标准化string del_exists(string temp);/消去存在量词string convert_to_front(string temp);/化为前束形string convert_to_and(string temp);/把母式化为合取范式string del_all(string temp);/消去全称量词string del
4、_and(string temp);/消去连接符号合取%string change_name(string temp);/更换变量名称/辅助函数定义bool isAlbum(char temp);/是字母string del_null_bracket(string temp);/删除多余的括号string del_blank(string temp);/删除多余的空格void checkLegal(string temp);/检查合法性char numAfectChar(int temp);/数字显示为字符/主函数void main()cout-求子句集九步法演示-P);/orign = (#
5、x)y(x);/orign = (x)x!b(x);/orign = (x!y);/orign = (a(b);string orign,temp;char command,command0,command1,command2,command3,command4,command5,command6,command7,command8,command9,command10;/=cout请输入(Y/y)初始化谓词演算公式command;if(command = y | command = Y)initString(orign);elseexit(0);/=cout请输入(Y/y)消除空格comma
6、nd0;if(command0 = y | command0 = Y)/del_blank(orign);/undonecout消除空格后是endlorignendl;elseexit(0);/=cout请输入(Y/y)消去蕴涵项command1;if(command1 = y | command1 = Y)orign =del_inlclue(orign);cout消去蕴涵项后是endlorignendl;elseexit(0);/=cout请输入(Y/y)减少否定符号的辖域command2;if(command2 = y | command2 = Y)dotemp = orign;orig
7、n = dec_neg_rand(orign);while(temp != orign);cout减少否定符号的辖域后是endlorignendl;elseexit(0);/=cout请输入(Y/y)对变量进行标准化command3;if(command3 = y | command3 = Y)orign = standard_var(orign);cout对变量进行标准化后是endlorignendl;elseexit(0);/=cout请输入(Y/y)消去存在量词command4;if(command4 = y | command4 = Y)orign = del_exists(orign
8、);cout消去存在量词后是(w = g(x)是一个Skolem函数)endlorignendl;elseexit(0);/=cout请输入(Y/y)化为前束形command5;if(command5 = y | command5= Y)orign = convert_to_front(orign);cout化为前束形后是endlorignendl;elseexit(0);/=cout请输入(Y/y)把母式化为合取方式command6;if(command6 = y | command6 = Y)orign = convert_to_and(orign);cout把母式化为合取方式后是endl
9、orignendl;elseexit(0);/=cout请输入(Y/y)消去全称量词command7;if(command7 = y | command7 = Y)orign= del_all(orign);cout消去全称量词后是endlorignendl;elseexit(0);/=cout请输入(Y/y)消去连接符号command8;if(command8 = y | command8 = Y)orign = del_and(orign);cout消去连接符号后是endlorignendl;elseexit(0);/=cout请输入(Y/y)变量分离标准化command9;if(command9 = y | command9 = Y)orign = change_name(orign);cout变量分离标准化后是(x1,x2,x3代替变量x)endlorignendl;elseexit(0);/=cout-完毕-endl;cout(请
