实现基于谓词逻辑得归结原理.doc

某某城建学院人工智能实验报告实验名称：实现基于谓词逻辑的归结原理成绩：_专业班级： 学 号：某某：实 验 日 期 ：实验器材： 一台装PC机。1、 实验目的熟练掌握使用归结原理进展定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程与简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。2、 实验要求对于任意给定的一阶谓词逻辑所描述的定理，要某某现如下过程：(1) 谓词公式到子句集变换；(2) 替换与合一算法；(3) 在某简单归结策略下的归结。3、 实验步骤步1 设计谓词公式与自居的存储结构，即内部表示。注意对全称量词"x和存在量词$x可采用其他符号代替；步2 实现谓词公式到子句集变换过程；步3 实现替换与合一算法；步4 实现某简单归结策略；步5 设计输出，动态演示归结过程，可以以归结树的形式给出；步6 实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。4、 代码谓词公式到子句集变换的源代码：#include<iostream>#include<sstream>#include<stack>#include<queue>using namespace std;/一些函数的定义void initString(string &ini);/初始化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);/把母式化为合取X式string del_all(string temp);/消去全称量词string del_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<<"-求子句集九步法演示-"<<endl;system("color 0A"); /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)"string orign,temp;char mand,mand0,mand1,mand2,mand3,mand4,mand5,mand6,mand7,mand8,mand9,mand10;/=cout<<"请输入(Y/y)初始化谓词演算公式"<<endl;cin>>mand;if(mand = 'y' | mand = 'Y')initString(orign);elseexit(0);/=cout<<"请输入(Y/y)消除空格"<<endl;cin>>mand0;if(mand0 = 'y' | mand0 = 'Y')/del_blank(orign);/undonecout<<"消除空格后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)消去蕴涵项"<<endl;cin>>mand1;if(mand1 = 'y' | mand1 = 'Y')orign =del_inlclue(orign);cout<<"消去蕴涵项后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)减少否认符号的辖域"<<endl;cin>>mand2;if(mand2 = 'y' | mand2 = 'Y')dotemp = orign;orign = dec_neg_rand(orign);while(temp != orign);cout<<"减少否认符号的辖域后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)对变量进展标准化"<<endl;cin>>mand3;if(mand3 = 'y' | mand3 = 'Y')orign = standard_var(orign);cout<<"对变量进展标准化后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)消去存在量词"<<endl;cin>>mand4;if(mand4 = 'y' | mand4 = 'Y')orign = del_exists(orign);cout<<"消去存在量词后是(w = g(x)是一个Skolem函数)"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)化为前束形"<<endl;cin>>mand5;if(mand5 = 'y' | mand5= 'Y')orign = convert_to_front(orign);cout<<"化为前束形后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)把母式化为合取方式"<<endl;cin>>mand6;if(mand6 = 'y' | mand6 = 'Y')orign = convert_to_and(orign);cout<<"把母式化为合取方式后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)消去全称量词"<<endl;cin>>mand7;if(mand7 = 'y' | mand7 = 'Y')orign= del_all(orign);cout<<"消去全称量词后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)消去连接符号"<<endl;cin>>mand8;if(mand8 = 'y' | mand8 = 'Y')orign = del_and(orign);cout<<"消去连接符号后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"请输入(Y/y)变量别离标准化"<<endl;cin>>mand9;if(mand9 = 'y' | mand9 = 'Y')orign = change_name(orign);cout<<"变量别离标准化后是(x1,x2,x3代替变量x)"<<endl<<orign<<endl;elseexit(0);/=cout<<"-完毕-"<<endl;cout<<"(请输入Y/y)完毕"<<endl;dowhile('y' = getchar() | 'Y'=getchar();exit(0);void initString(string &ini)char manda,mandb;cout<<"请输入您所需要转换的谓词公式"<<endl;cout<<"需要查看输入帮助(Y/N)? "<<endl;cin>>manda;if(manda = 'Y' | manda = 'y')cout<<"本例程规定输入时蕴涵符号为>,全称量词为,存在量词为#,"<<endl<<"取反为,吸取为!,合取为%,左右括号分别为( 、 )，函数名请用一个字母"<<endl;cout<<"请输入(y/n)选择是否用户自定义"<<endl;cin>>mandb;if(mandb ='Y'| mandb='y')cin>>ini;elseini = "(x)(P(x)>(y)(P(y)>P(f(x, y)%(y)(Q(x,y)>P(y)"cout<<"原始命题是"<<endl<<ini<<endl;string del_inlclue(string temp)/消去>蕴涵项/a>b变为a!bchar ctemp100=""string output;int length = temp.length();int i = 0,right_bracket = 0,falg= 0;stack<char> stack1,stack2,stack3;strcpy(ctemp,temp.c_str();while(ctempi != '0' && i <= length-1)stack1.push(ctempi);if('>' = ctempi+1)/如果是a>b如此用a!b替代falg = 1;if(isAlbum(ctempi)/如果是字母如此把ctempi弹出stack1.pop();stack1.push('');stack1.push(ctempi);stack1.push('!');i = i + 1;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()stack2.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;string output;int flag2 = 0;int i = 0,left_bracket = 0,length = temp.length();stack <char> stack1,stack2;queue <char> queue1;strcpy(ctemp,temp.c_str();/复制到字符数组中while(ctempi != '0' && i <= length - 1)stack1.push(ctempi);if(ctempi = '')/如果是否如此都不做char fo = ctempi+2;if(ctempi+1 = '(')/如果是(，否如此都不做if(fo = '' | fo ='#')/如果是全称量词flag2 = 1;i+;stack1.pop();stack1.push(ctempi);if(fo = '')stack1.push('#');elsestack1.push('');stack1.push(ctempi+2);stack1.push(ctempi+3);stack1.push('(');stack1.push('');if(isAlbum(ctempi+4)stack1.push(ctempi+4);i = i + 5;elsei = i + 4;doqueue1.push(tempi);if(tempi = '(')left_bracket +;else if(tempi = ')')left_bracket -;i +;while(left_bracket != 0 && left_bracket >=0);queue1.push(')');while(!queue1.empty()tempc = queue1.front();queue1.pop();stack1.push(tempc);i +;while(!stack1.empty()stack2.push(stack1.top();stack1.pop();while(!stack2.empty()output += stack2.top();stack2.pop();if(flag2 = 1)temp = output;/*/char ctemp1100;string output1;stack<char> stack11,stack22;int falg1 = 0;int times = 0;int length1 = temp.length(),inleftbackets = 1,j = 0;strcpy(ctemp1,temp.c_str();while(ctemp1j != '0' && j <= (length1 -1)stack11.push(ctemp1j);if(ctemp1j = '')if(ctemp1j+1 = '(' /*&& ctemp1j + 2 != ''*/)j = j + 2;stack11.push('(');/while(inleftbackets != 0 && inleftbackets >=0 && times <= (length1 - j) && times >= 0)stack11.push(ctemp1j);if(ctemp1j = '(')inleftbackets +;else if(ctemp1j = ')')inleftbackets -;if(inleftbackets = 1 && ctemp1j+1 = '!' && ctemp1j+2 != '' && ctemp1j+2 != '#')falg1 =1;stack11.push(')');/stack11.push('%');stack11.push('');stack11.push('(');/j = j+1;if(inleftbackets = 1 && ctemp1j+1 = '%' && ctemp1j+2 != '' && ctemp1j+2 != '#')falg1 =1;stack11.push(')');/stack11.push('!');stack11.push('');stack11.push('(');/j = j+1;j = j +1;if(falg1 = 1)stack11.push(')');stack11.pop();stack11.push(')');/此处有bugstack11.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;string output3;int k = 0,left_bracket3 = 1,length3 = temp.length();stack <char> stack13,stack23;int flag = 0,bflag = 0;strcpy(ctemp3,temp.c_str();/复制到字符数组中while(ctemp3k != '0' && k <= length3-1)stack13.push(ctemp3k);if(ctemp3k = '')if(ctemp3k+1 = '(')if(ctemp3k + 2 = '')flag = 1;stack13.pop();k =k + 2;while(left_bracket3 != 0 && left_bracket3 >=0)stack13.push(ctemp3k+1);if(ctemp3k+1 = '(')left_bracket3 +;if(ctemp3k+1 = ')')left_bracket3 -;if(ctemp3k+1 = '!' | ctemp3k+1 = '%')bflag = 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();stack <char> stack1,stack2;int l_bracket = 1,falg = 0,bracket = 1;int i = 0,j = 0;string output;while(ctempi != '0' && i < temp.length()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 != '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('(');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_exists(string temp)/消去存在量词char ctemp100,unknow;strcpy(ctemp,temp.c_str();int left_brackets = 0,i = 0,falg = 0;queue<char> queue1;string output;while(ctempi != '0' && i < temp.length()if(ctempi ='(' && ctempi+1 ='#')falg = 1;unknow = ctempi+2;i = i+4;doif(ctempi = '(')left_brackets +;if(ctempi = ')')left_brackets -;if(ctempi = unknow)queue1.push('g');queue1.push('(');queue1.push('x');queue1.push(')');if(ctempi != unknow)queue1.push(ctempi);i+;while(left_brackets != 0);queue1.push(ctempi);i+;while(!queue1.empty()output+= queue1.front();queue1.pop();if(falg = 1)return output;elsereturn temp;string convert_to_front(string temp)/化为前束形char ctemp100;strcpy(ctemp,temp.c_str();int i = 0;string out_var = "",output = ""while(ctempi != '0' && i < temp.length()if(ctempi = '(' && ctempi+1 = '')out_var = out_var + ctempi ;/()out_var = out_var + ctempi+1 ;out_var = out_var +ctempi+2;out_var = out_var +ctempi+3;i = i + 4;output = output + ctempi;i+;output = out_var + output;return output;string convert_to_and(string temp)/把母式化为合取X式 ,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;string output = ""while(ctempi != '0' && i < temp.length()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;string output = ""while(ctempi != '0' && i < temp.length()if(ctempi = '%' )ctempi = 'n'output = output +ctempi;i+;return output;string change_name(string temp)/更换变量名称char ctemp100;strcpy(ctemp,temp.c_str();string output = ""int i = 0,j = 0,falg = 0;while(ctempi != '0' && i < temp.length()falg+;while('n' != ctempi && i < temp.length()if('x' = ctempi)output = output + ctempi ;output = output + numAfectChar(falg);elseoutput = output + ctempi ;i+;output = output + ctempi ;i +;return output;bool isAlbum(char temp)if(temp <= 'Z' && temp >= 'A' | temp <= 'z' && temp >= 'a')return true;return false;char numAfectChar(int temp)/数字显示为字符int t;switch (temp)case 1:t = 1;break;case 2:t = 2;break;case 3:t = 3;break;case 4:t = 4;break;default:t = 89;break;return t;5、 结果分析（1） 非用户自定义时：6、 心得体会通过这次实验，熟悉了谓词公式转换成子句集的步骤，理解消解谓词公式化为子句集规如此，能把任意谓词公式转换成子句集。对子句集进展消解推理，得到相应的结论。为了对含有变量的字句使用消解规如此，必须找到一个置换，作用于父辈字句使其含有互补文字。消解两个字句时可能有一个以上的消解式，不过，在任何情况下最多有有限个消解式。