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

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

2、其他符号代替；步2实现谓词公式到子句集变换过程；步3实现替换与合一算法；步4实现某简单归结策略；步5设计输出，动态演示归结过程，可以以归结树的形式给出；步6实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略四、代码谓词公式到子句集变换的源代码：#in clude#in clude#in clude#in cludeusing n amespace std;一些函数的定义void in itStri ng(stri ng &ni);/ 初始化string del_inlclue(string temp);/ 消去蕴涵符号string dec_neg_rand(string temp);

3、/ 减少否定符号的辖域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_and(string temp);/ 消去连接符号合取 %stri ng cha nge_n ame(stri ng temp);/ 更换变量名

4、称/辅助函数定义bool isAlbum(char temp);/ 是字母string del_null_bracket(string temp);/ 删除多余的括号string del_blank(string temp);/ 删除多余的空格void checkLegal(string temp);/ 检查合法性char numAfectChar(int temp);/ 数字显示为字符/主函数void mai n()cout 求子句集九步法演示 P);/orign = (#x)y(x);/orign = (x)x!b(x);/orign = (x!y);/orign = (a(b);stri

5、 ng orig n,temp;char comma nd,comma ndO,comma nd1,comma nd2,comma nd3,comma nd4,comma nd5, comma nd6,comma nd7,comma nd8,comma nd9,comma nd10;/=cout请输入(Y/y)初始化谓词演算公式 comma nd;if(comma nd = y | comma nd = Y)in itStri ng(orig n);elseexit(0);/=cout请输入(Y/y)消除空格 comma ndO;if(comma ndO = y | comma ndO = Y

6、)/del_bla nk(orig n); undonecout消除空格后是endlorig nen dl;elseexit(0);/=cout请输入(Y/y)消去蕴涵项 comma nd1;if(comma nd1 = y | comma nd1 = Y)orig n =del_i nl clue(orig n);cout消去蕴涵项后是endlorig nen dl; elseexit(O);/=cout请输入(Y/y)减少否定符号的辖域 comma nd2;if(comma nd2 = y | comma nd2 = Y)dotemp = orig n;orig n = dec_ neg_

7、ra nd(orig n);while(temp != orig n);cout减少否定符号的辖域后是 e ndlorig nen dl;elseexit(0);/=cout请输入(Y/y)对变量进行标准化 comma nd3;if(comma nd3 = y | comma nd3 = Y)orig n = sta ndard_var(orig n);cout对变量进行标准化后是 e ndlorig n comma nd4;cout请输入(Y/y)消去存在量词endl;if(comma nd4 = y | comma nd4 = Y)orig n = del_exists(orig n);c

8、out消去存在量词后是 (w = g(x)是一个 Skolem函数)endlorig nen dl;elseexit(0);/=cout请输入(Y/y)化为前束形 comma nd5;if(comma nd5 = y | comma nd5= Y)orig n = con vert_to_fro nt(orig n);cout化为前束形后是endlorig nen dl;elseexit(0);/=cout请输入(Y/y)把母式化为合取方式 comma nd6;if(comma nd6 = y | comma nd6 = Y)orig n = con vert_to_a nd(orig n);

9、cout把母式化为合取方式后是 e ndlorig nen dl;elseexit(0);/=cout请输入（Y/y）消去全称量词 comma nd7;if(comma nd7 = y | comma nd7 = Y)orig n= del_all(orig n);cout消去全称量词后是endlorig nen dl;elseexit(O);/=cout请输入(Y/y)消去连接符号 comma nd8;if(comma nd8 = y | comma nd8 = Y)orig n = del_a nd(orig n);cout消去连接符号后是endlorig nen dl;elseexit(

10、0);/=cout请输入(Y/y)变量分离标准化 comma nd9;if(comma nd9 = y | comma nd9 = Y)orig n = cha nge_n ame(orig n);cout变量分离标准化后是 (x1,x2,x3代替变量x)endlorig nen dl;elseexit(0);/:cout”完毕e ndl;cout(请输入 Y/y)结束endl;dowhile(y = getchar() | Y=getchar();exit(O); void in itStri ng(stri ng &ini)char comma nda,comma ndb;cout请输入您

11、所需要转换的谓词公式e ndl;cout需要查看输入帮助 (Y/N)? comma nda;if(comma nda = Y | comma nda = y)cout，全称量词为,存在量词为#,endl取反为,吸取为!,合取为%,左右括号分别为(、)，函数名请用一个字母e ndl;cout请输入(y/n)选择是否用户自定义 comma ndb;if(comma ndb =Y| comma ndb=y)ci nini;elseini = ”(x)(P(x)(y)(P(y)P(f(x, y)%(y)(Q(x,y)P(y)”；cout原始命题是endlinib 变为 a!bchar ctemp100

12、=;stri ng output;int len gth = temp.le ngth();int i = O,right_bracket = O,falg= 0;stack stack1,stack2,stack3;strcpy(ctemp,temp.c_str();while(ctempi != 0 & i = ctempi+1) 如果是 ab 则用 a!b 替代falg = 1;if(isAlbum(ctempi) 如果是字母则把 ctempi弹出stack1.pop();stack1.push();stack1.push(ctempi);stack1.push(!);i = i + 1

13、;else if() = ctempi)right_bracket+;doif( = stack1.top()right_bracket-; stack3.push(stack1.top(); stack1.pop();while(right_bracket != 0);stack3.push(stack1.top();stack1.pop();stack1.push();while(!stack3.empty()stack1.push(stack3.top();stack3.pop();stack1.push(!);i = i + 1;i+；while(!stack1.empty()stac

14、k2.push(stack1.top(); stack1.pop();while(!stack2.empty()output += stack2.top();stack2.pop();if(falg = 1)return output;elsereturn temp;string dec_neg_rand(string temp)/ 减少否定符号的辖域 char ctemp100,tempc;stri ng output;int flag2 = 0;int i = 0,left_bracket = 0,le ngth = temp .len gth(); stack stack1,stack2

15、;queue queue1; strcpy(ctemp,temp.c_str(); 复制到字符数组中 while(ctempi != 0 & i =0);queue1.push();while(!queue1.empty()tempc = queuel.fro nt(); queue1.pop(); stackl.push(tempc);i +；while(!stack1.empty()stack2.push(stack1.top(); stack1.pop();while(!stack2.empty()output += stack2.top(); stack2.pop();if(flag2

16、 = 1)temp = output;/*char ctemp1100;stri ng output1;stack stack11,stack22;int falg1 = 0;int times = 0;int len gth1 = temp .len gth(),i nl eftbackets = 1,j = 0;strcpy(ctemp1,temp.c_str();while(ctemp1j != 0 & j =0 & times = 0)stack11.push(ctemp1j);if(ctemp1j=()ini eftbackets +;else if(ctemp1j=)ini eft

17、backets -;if(i nleftbackets = 1 & ctemp1j+1 = ! & ctemp1j+2 != & ctemp1j+2 != #)falgl =1;stackll.push();/stack11.push(%);stack11.push();stack11.push();/j =j+1;if(i nleftbackets = 1 & ctemp1j+1 = % & ctemp1j+2 != & ctemp1j+2 != #)falgl =1;stackll.push();/stack11.push(!);stack11.push();stack11.push();

18、/j =j+1;j = j +1;if(ctemp3k+1=()if(falg1 = 1)stackll.push(); stack11.pop();stackll.push();/此处有 bug stackll.push();/此处有 bugj +;while(!stack11.empty()stack22.push(stack11.top(); stack11.pop();while(!stack22.empty()output1 += stack22.top();stack22.pop();if(falg1 = 1)temp = output1;/* char ctemp3100;str

19、i ng output3;int k = 0,left_bracket3 = 1,le ngth3 = temp.le ngth(); stack stack13,stack23;int flag = 0,bflag = 0;strcpy(ctemp3,temp.c_str(); 复制到字符数组中 while(ctemp3k != 0 & k =0) stack13.push(ctemp3k+1); if(ctemp3k+1=()left_bracket3 +;if(ctemp3k+1=)left_bracket3 -;if(ctemp3k+1 = ! | ctemp3k+1 = %)bfla

20、g = 1;k +;stack13.pop();k +;while(!stack13.empty()stack23.push(stack13.top();stack13.pop();while(!stack23.empty()output3 += stack23.top();stack23.pop();if(flag = 1 & bflag = 0)temp = output3;return temp;string standard_var(string temp)/对变量标准化，简化，不考虑多层嵌套 char ctemp100,des10= ;strcpy(ctemp,temp.c_str(

21、);stack stack1,stack2;int l_bracket = 1,falg = 0,bracket = 1;int i = 0,j = 0;stri ng output;while(ctempi != 0 & i temp.le ngth() stack1.push(ctempi);if(ctempi = | ctempi = #)stack1.push(ctempi+1);desj = ctempi+1;j+;stack1.push(ctempi+2);i = i + 3;stack1.push(ctempi);i+;if(ctempi-1=()while(ctempi !=

22、0 & l_bracket != 0)if(ctempi=()l_bracket +;if(ctempi=)l_bracket -;if(ctempi = ( & ctempi+1 = ) desj = ctempi+2;j+;if(ctempi+1 = ( & ctempi+2 = #) falg = 1;int kk = 1;stack1.push(ctempi);stack1.push();stack1.push(ctempi+2);i = i+3;if(ctempi = y)ctempi =w;stack1.push(ctempi);stack1.push();stack1.push(

23、);i = i+3;while(kk != 0)if(ctempi=()kk+;if(ctempi =)kk-;if(ctempi = y)ctempi =w;stack1.push(ctempi);i+;stack1.push(ctempi);i +;i +;while(!stack1.empty()stack2.push(stack1.top(); stack1.pop();while(!stack2.empty()output += stack2.top();stack2.pop();if(falg = 1)return output;elsereturn temp;string del

24、_exists(string temp)/ 消去存在量词char ctemp100,u nknow;strcpy(ctemp,temp.c_str();int left_brackets = 0,i = 0,falg = 0;queue queue1;stri ng output;while(ctempi != 0 & i temp.le ngth()if(ctempi =( & ctempi+1 =#) falg = 1;unknow = ctempi+2;i = i+4;doif(ctempi=()left_brackets +;left_brackets -;if(ctempi=)if(

25、ctempi = unknow)queuel.push(g);queue1.push();queuel.push(x); queuel.push();if(ctempi != unknow)queue1.push(ctempi); i+；while(left_brackets != 0);queue1.push(ctempi);i+;while(!queue1.empty()output+= queue1.fr on t(); queue1.pop();if(falg = 1)return output;elsereturn temp;string convert_to_front(strin

26、g temp)/ 化为前束形 char ctemp100; strcpy(ctemp,temp.c_str();int i = 0;stri ng out_var = output =; while(ctempi != 0 & i temp.le ngth() if(ctempi = ( & ctempi+1 = )out_var =out_var+ ctempi ;/()out_var = out_var+ ctempi+1out_var =out_var+ctempi+2;out_var =out_var+ctempi+3;i = i + 4;output = output + ctemp

27、i;i+；output = out_var + output;return output;string convert_to_and(string temp)/ 把母式化为合取范式，Q/A?temp = (x)(y)(P(x)!(P(y)!P(f(x,y)%(P(x)!Q(x,g(x)%(P(x)!(P(g(x); return temp;string del_all(string temp)/ 消去全称量词char ctemp100;strcpy(ctemp,temp.c_str();int i = 0,flag = 0;stri ng output =;while(ctempi != 0

28、& i temp.le ngth()if(ctempi = ( & ctempi+1 = )i = i + 4;flag = 1;elseoutput = output + ctempi;i +；return output;string del_and(string temp)/ 消去连接符号合取 %char ctemp100;strcpy(ctemp,temp.c_str();int i = 0,flag = 0;stri ng output =;while(ctempi != 0 & i temp.le ngth()if(ctempi = %)ctempi = n;output = output +ctempi;i+;return output;stri ng cha nge_n ame(stri ng temp)/ 更换变量名称char ctemp100;strcpy(ctemp,temp.c_str();stri ng output =;int i = 0,j = 0,falg = 0;while(ctempi != 0 & i temp.le ngth()falg+;while(n != ctemp