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

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

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

3、_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_and(string temp);/ 消去连接符号合取 % stri ng cha n

4、ge_n ame(stri ng 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 mai n() cout 求子句集九步法演示 P); /orign = (#x)y(x); /orign = (x)

5、x!b(x); /orign = (x!y); /orign = (a(b); stri 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); else exit(0); /= cout请输

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

7、; if(comma nd2 = y | comma nd2 = Y) do temp = orig n; orig n = dec_ neg_ra nd(orig n); while(temp != orig n); cout减少否定符号的辖域后是 e ndl orig nen dl; else exit(0); /= cout请输入(Y/y)对变量进行标准化 comma nd3; if(comma nd3 = y | comma nd3 = Y) orig n = sta ndard_var(orig n); cout对变量进行标准化后是 e ndl orig n comma nd4; c

8、out请输入(Y/y)消去存在量词endl; if(comma nd4 = y | comma nd4 = Y) orig n = del_exists(orig n); cout消去存在量词后是 (w = g(x)是一个 Skolem函数)endl orig nen dl; else exit(0); /= cout请输入(Y/y)化为前束形 comma nd5; if(comma nd5 = y | comma nd5= Y) orig n = con vert_to_fro nt(orig n); cout化为前束形后是endl orig nen dl; else exit(0); /=

9、 cout请输入(Y/y)把母式化为合取方式 comma nd6; if(comma nd6 = y | comma nd6 = Y) orig n = con vert_to_a nd(orig n); cout把母式化为合取方式后是 e ndl orig nen dl; else exit(0); /= cout请输入（Y/y）消去全称量词 comma nd7; if(comma nd7 = y | comma nd7 = Y) orig n= del_all(orig n); cout消去全称量词后是endl orig nen dl; else exit(O); /= cout请输入(Y

10、/y)消去连接符号 comma nd8; if(comma nd8 = y | comma nd8 = Y) orig n = del_a nd(orig n); cout消去连接符号后是endl orig nen dl; else exit(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)endl orig nen dl; else exit(0); /: cout”完毕e n

11、dl; cout(请输入 Y/y)结束endl; do while(y = getchar() | Y=getchar(); exit(O); void in itStri ng(stri ng cout请输入您所需要转换的谓词公式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 =

12、Y| comma ndb=y) ci nini; else ini = ”(x)(P(x)(y)(P(y)P(f(x, y)%(y)(Q(x,y)P(y)”； cout原始命题是endl inib 变为 a!b char ctemp100=; 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 if(isAlbum(ctempi) 如果是

13、字母则把 ctempi弹出 stack1.pop(); stack1.push(); stack1.push(ctempi); stack1.push(!); i = i + 1; else if() = ctempi) right_bracket+; do if( = stack1.top() right_bracket-; stack3.push(stack1.top(); stack1.pop(); while(right_bracket != 0); stack3.push(stack1.top(); stack1.pop(); stack1.push(); while(!stack3

14、.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; else return temp; string dec_neg_rand(string temp)/ 减少否定符号的辖域 char cte

15、mp100,tempc; stri ng output; int flag2 = 0; int i = 0,left_bracket = 0,le ngth = temp .len gth(); stack stack1,stack2; queue queue1; strcpy(ctemp,temp.c_str(); 复制到字符数组中 while(ctempi != 0 queue1.push(); while(!queue1.empty() tempc = queuel.fro nt(); queue1.pop(); stackl.push(tempc); i +； while(!stack

16、1.empty() stack2.push(stack1.top(); stack1.pop(); while(!stack2.empty() output += stack2.top(); stack2.pop(); if(flag2 = 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,

17、temp.c_str(); while(ctemp1j != 0 if(ctemp1j=() ini eftbackets +; else if(ctemp1j=) ini eftbackets -; if(i nleftbackets = 1 stackll.push();/ stack11.push(%); stack11.push(); stack11.push();/ j =j+1; if(i nleftbackets = 1 stackll.push();/ stack11.push(!); stack11.push(); stack11.push();/ j =j+1; j = j

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

19、nt 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 if(ctemp3k+1=() left_bracket3 +; if(ctemp3k+1=) left_bracket3 -; if(ctemp3k+1 = ! | ctemp3k+1 = %) bflag = 1; k +; stack13.pop(); k +; while(!s

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

21、ket = 1; int i = 0,j = 0; stri ng output; while(ctempi != 0 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 if(ctempi=) l_bracket -; if(ctempi = ( j+; if(ctempi+1 = ( int kk = 1; stack1.

22、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(

23、) stack2.push(stack1.top(); stack1.pop(); while(!stack2.empty() output += stack2.top(); stack2.pop(); if(falg = 1) return output; else return temp; string del_exists(string temp)/ 消去存在量词 char ctemp100,u nknow; strcpy(ctemp,temp.c_str(); int left_brackets = 0,i = 0,falg = 0; queue queue1; stri ng out

24、put; while(ctempi != 0 unknow = ctempi+2; i = i+4; do if(ctempi=() left_brackets +; left_brackets -; if(ctempi=) if(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(!

25、queue1.empty() output+= queue1.fr on t(); queue1.pop(); if(falg = 1) return output; else return temp; string convert_to_front(string temp)/ 化为前束形 char ctemp100; strcpy(ctemp,temp.c_str(); int i = 0; stri ng out_var = output =; while(ctempi != 0 /() out_var = = out_var + ctempi+1 out_var = =out_var +

26、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)/ 把母式化为合取范式，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

27、; strcpy(ctemp,temp.c_str(); int i = 0,flag = 0; stri ng output =; while(ctempi != 0 flag = 1; else output = 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 output = output

28、+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 while(n != ctempi output = output + nu mAfectChar(falg); else output = output + ctempi; i+； output = output + ctempi; i +； return output; bool isAlbum(char temp) if(temp = A | temp = a) return true; return false; char numAfectChar(int temp)/