实现基于谓词逻辑的归结原理

河南城建学院《人工智能》实验报告实验名称：实现基于谓词逻辑的归结原理成绩：____专业班级：学号：姓名：实验日期：2014年05月13日实验器材：一台装PC机。一、实验目的熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。二、实验要求对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程：(1)谓词公式到子句集变换；(2)替换与合一算法；(3)在某简单归结策略下的归结。三、实验步骤步1设计谓词公式及自居的存储结构，即内部表示。注意对全称量词x和存在量词x可采用其他符号代替；步2实现谓词公式到子句集变换过程；步3实现替换与合一算法；步4实现某简单归结策略；步5设计输出，动态演示归结过程，可以以归结树的形式给出；步6实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。四、代码谓词公式到子句集变换的源代码：#includeiostream#includesstream#includestack#includequeueusingnamespacestd;//一些函数的定义voidinitString(string&ini);//初始化stringdel_inlclue(stringtemp);//消去蕴涵符号stringdec_neg_rand(stringtemp);//减少否定符号的辖域stringstandard_var(stringtemp);//对变量标准化stringdel_exists(stringtemp);//消去存在量词stringconvert_to_front(stringtemp);//化为前束形stringconvert_to_and(stringtemp);//把母式化为合取范式stringdel_all(stringtemp);//消去全称量词stringdel_and(stringtemp);//消去连接符号合取%stringchange_name(stringtemp);//更换变量名称//辅助函数定义boolisAlbum(chartemp);//是字母stringdel_null_bracket(stringtemp);//删除多余的括号stringdel_blank(stringtemp);//删除多余的空格voidcheckLegal(stringtemp);//检查合法性charnumAfectChar(inttemp);//数字显示为字符//主函数voidmain(){cout------------------求子句集九步法演示-----------------------endl;system(color0A);//orign=Q(x,y)%~(P(y);//orign=(@x)(P(y)P);//orign=~(#x)y(x);//orign=~((@x)x!b(x));//orign=~(x!y);//orign=~(~a(b));stringorign,temp;charcommand,command0,command1,command2,command3,command4,command5,command6,command7,command8,command9,command10;//=============================================================================cout请输入(Y/y)初始化谓词演算公式endl;cincommand;if(command=='y'||command=='Y')initString(orign);elseexit(0);//=============================================================================cout请输入(Y/y)消除空格endl;cincommand0;if(command0=='y'||command0=='Y'){//del_blank(orign);//undonecout消除空格后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去蕴涵项endl;cincommand1;if(command1=='y'||command1=='Y'){orign=del_inlclue(orign);cout消去蕴涵项后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)减少否定符号的辖域endl;cincommand2;if(command2=='y'||command2=='Y'){do{temp=orign;orign=dec_neg_rand(orign);}while(temp!=orign);cout减少否定符号的辖域后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)对变量进行标准化endl;cincommand3;if(command3=='y'||command3=='Y'){orign=standard_var(orign);cout对变量进行标准化后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去存在量词endl;cincommand4;if(command4=='y'||command4=='Y'){orign=del_exists(orign);cout消去存在量词后是(w=g(x)是一个Skolem函数)endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)化为前束形endl;cincommand5;if(command5=='y'||command5=='Y'){orign=convert_to_front(orign);cout化为前束形后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)把母式化为合取方式endl;cincommand6;if(command6=='y'||command6=='Y'){orign=convert_to_and(orign);cout把母式化为合取方式后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去全称量词endl;cincommand7;if(command7=='y'||command7=='Y'){orign=del_all(orign);cout消去全称量词后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去连接符号endl;cincommand8;if(command8=='y'||command8=='Y'){orign=del_and(orign);cout消去连接符号后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)变量分离标准化endl;cincommand9;if(command9=='y'||command9=='Y'){orign=change_name(orign);cout变量分离标准化后是(x1,x2,x3代替变量x)endlorignendl;}elseexit(0);//============================================================================cout-------------------------完毕-----------------------------------endl;cout(请输入Y/y)结束endl;do{}while('y'==getchar()||'Y'==getchar());exit(0);}voidinitString(string&ini){charcommanda,commandb;cout请输入您所需要转换的谓词公式endl;cout需要查看输入帮助(Y/N)?endl;cincommanda;if(commanda=='Y'||commanda=='y')cout本例程规定输入时蕴涵符号为,全称量词为@,存在量词为#,endl取反为~,吸取为!,合取为%,左右括号分别为(、)，函数名请用一个字母endl;cout请输入(y/n)选择是否用户自定义endl;cincommandb;if(commandb=='Y'||commandb=='y')cinini;elseini=(@x)(P(x)((@y)(P(y)P(f(x,y)))%~(@y)(Q(x,y)P(y))));cout原始命题是endliniendl;}stringdel_inlclue(stringtemp)//消去蕴涵项{//ab变为~a!bcharctemp[100]={};stringoutput;intlength=temp.length();inti=0,right_bracket=0,falg=0;stackcharstack1,stack2,stack3;strcpy(ctemp,temp.c_str());while(ctemp[i]!='\0'&&i=length-1){stack1.push(ctemp[i]);if(''==ctemp[i+1])//如果是ab则用~a!b替代{falg=1;if(isAlbum(ctemp[i]))//如果是字母则把ctemp[i]弹出{stack1.pop();stack1.push('~');stack1.push(ctemp[i]);stack1.push('!');i=i+1;}elseif(')'==ctemp