實(shí)現(xiàn)基于謂詞邏輯的歸結(jié)原理

1、河南城建學(xué)院人工智能實(shí)驗(yàn)報(bào)告實(shí)驗(yàn)名稱：實(shí)現(xiàn)基于謂詞邏輯的歸結(jié)原理成 績：_ 專業(yè)班級：  學(xué) 號： 姓 名： 實(shí) 驗(yàn) 日 期 ：20 14 年 05 月 13日實(shí)驗(yàn)器材： 一臺裝PC機(jī)。1、 實(shí)驗(yàn)?zāi)康?熟練掌握使用歸結(jié)原理進(jìn)行定理證明的過程，掌握基于謂詞邏輯的歸結(jié)過程中，子句變換過程、替換與合一算法、歸結(jié)過程及簡單歸結(jié)策略等重要環(huán)節(jié)，進(jìn)一步了解機(jī)器自動定理證明的實(shí)現(xiàn)過程。2、 實(shí)驗(yàn)要求對于任意給定的一階謂詞邏輯所描述的定理，要求實(shí)現(xiàn)如下過程：(1) 謂詞公式到子句集變換；(2) 替換與合一算法；(3) 在某簡單歸結(jié)策略下的歸結(jié)。3、 實(shí)驗(yàn)步驟 步1 設(shè)計(jì)

2、謂詞公式及自居的存儲結(jié)構(gòu)，即內(nèi)部表示。注意對全稱量詞"x和存在量詞$x可采用其他符號代替；步2 實(shí)現(xiàn)謂詞公式到子句集變換過程；步3 實(shí)現(xiàn)替換與合一算法；步4 實(shí)現(xiàn)某簡單歸結(jié)策略；步5 設(shè)計(jì)輸出，動態(tài)演示歸結(jié)過程，可以以歸結(jié)樹的形式給出；步6 實(shí)現(xiàn)謂詞邏輯中的歸結(jié)過程，其中要調(diào)用替換與合一算法和歸結(jié)策略。4、 代碼謂詞公式到子句集變換的源代碼：#include<iostream>#include<sstream>#include<stack>#include<queue>using namespace std;/一些函數(shù)的定義void i

3、nitString(string &ini);/初始化string del_inlclue(string temp);/消去蘊(yùn)涵符號string dec_neg_rand(string temp);/減少否定符號的轄域string standard_var(string temp);/對變量標(biāo)準(zhǔn)化string del_exists(string temp);/消去存在量詞string convert_to_front(string temp);/化為前束形string convert_to_and(string temp);/把母式化為合取范式string del_all(string

4、 temp);/消去全稱量詞string del_and(string temp);/消去連接符號合取%string change_name(string temp);/更換變量名稱/輔助函數(shù)定義bool isAlbum(char temp);/是字母string del_null_bracket(string temp);/刪除多余的括號string del_blank(string temp);/刪除多余的空格void checkLegal(string temp);/檢查合法性char numAfectChar(int temp);/數(shù)字顯示為字符/主函數(shù)void main()cout&

5、lt;<"-求子句集九步法演示-"<<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 command,command0,command1

6、,command2,command3,command4,command5,command6,command7,command8,command9,command10;/=cout<<"請輸入(Y/y)初始化謂詞演算公式"<<endl;cin>>command;if(command = 'y' | command = 'Y')initString(orign);elseexit(0);/=cout<<"請輸入(Y/y)消除空格"<<endl;cin>>c

7、ommand0;if(command0 = 'y' | command0 = 'Y')/del_blank(orign);/undonecout<<"消除空格后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)消去蘊(yùn)涵項(xiàng)"<<endl;cin>>command1;if(command1 = 'y' | command1 = 'Y')orign =del_in

8、lclue(orign);cout<<"消去蘊(yùn)涵項(xiàng)后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)減少否定符號的轄域"<<endl;cin>>command2;if(command2 = 'y' | command2 = 'Y')dotemp = orign;orign = dec_neg_rand(orign);while(temp != orign);cout<<&qu

9、ot;減少否定符號的轄域后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)對變量進(jìn)行標(biāo)準(zhǔn)化"<<endl;cin>>command3;if(command3 = 'y' | command3 = 'Y')orign = standard_var(orign);cout<<"對變量進(jìn)行標(biāo)準(zhǔn)化后是"<<endl<<orign<<endl;else

10、exit(0);/=cout<<"請輸入(Y/y)消去存在量詞"<<endl;cin>>command4;if(command4 = 'y' | command4 = 'Y')orign = del_exists(orign);cout<<"消去存在量詞后是(w = g(x)是一個Skolem函數(shù))"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)化為前束形"

11、<<endl;cin>>command5;if(command5 = 'y' | command5= 'Y')orign = convert_to_front(orign);cout<<"化為前束形后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)把母式化為合取方式"<<endl;cin>>command6;if(command6 = 'y' |

12、command6 = 'Y')orign = convert_to_and(orign);cout<<"把母式化為合取方式后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)消去全稱量詞"<<endl;cin>>command7;if(command7 = 'y' | command7 = 'Y')orign= del_all(orign);cout<<&quo

13、t;消去全稱量詞后是"<<endl<<orign<<endl;elseexit(0);/=cout<<"請輸入(Y/y)消去連接符號"<<endl;cin>>command8;if(command8 = 'y' | command8 = 'Y')orign = del_and(orign);cout<<"消去連接符號后是"<<endl<<orign<<endl;elseexit(0);/=cou

14、t<<"請輸入(Y/y)變量分離標(biāo)準(zhǔn)化"<<endl;cin>>command9;if(command9 = 'y' | command9 = 'Y')orign = change_name(orign);cout<<"變量分離標(biāo)準(zhǔn)化后是(x1,x2,x3代替變量x)"<<endl<<orign<<endl;elseexit(0);/=cout<<"-完畢-"<<endl;cout<<

15、"(請輸入Y/y)結(jié)束"<<endl;dowhile('y' = getchar() | 'Y'=getchar();exit(0); void initString(string &ini)char commanda,commandb;cout<<"請輸入您所需要轉(zhuǎn)換的謂詞公式"<<endl;cout<<"需要查看輸入幫助(Y/N)? "<<endl;cin>>commanda;if(commanda = 'Y&#

16、39; | commanda = 'y')cout<<"本例程規(guī)定輸入時蘊(yùn)涵符號為>,全稱量詞為,存在量詞為#,"<<endl<<"取反為,吸取為!,合取為%,左右括號分別為( 、 )，函數(shù)名請用一個字母"<<endl;cout<<"請輸入(y/n)選擇是否用戶自定義"<<endl;cin>>commandb;if(commandb ='Y'| commandb='y')cin>>ini

17、;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)/消去>蘊(yùn)涵項(xiàng)/a>b變?yōu)閍!bchar ctemp100=""string output;int length = temp.length();int i = 0,right_bracket = 0,falg= 0;stac

18、k<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('

19、!');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.

20、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_bracke

21、t = 0,length = temp.length();stack <char> stack1,stack2;queue <char> queue1;strcpy(ctemp,temp.c_str();/復(fù)制到字符數(shù)組中while(ctempi != '0' && i <= length - 1)stack1.push(ctempi);if(ctempi = '')/如果是否則什么都不做char fo = ctempi+2;if(ctempi+1 = '(')/如果是(，否則什么都不做if(fo =

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

23、;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.empt

24、y()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();w

25、hile(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 -

26、 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(')');

27、/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('')

28、;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

29、 = 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();/復(fù)制到字符數(shù)組中while(ctemp3k != '0' && k <= length3-1)stack13.push(ctemp3k);if(ctemp3k = '

30、9;)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 = &#

31、39;%')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)/對變量標(biāo)準(zhǔn)化,簡化,不考慮多層嵌套char ctemp100,des10=&quo

32、t; "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;

33、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 =

34、 '(' && 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='(')

35、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

36、(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(ct

37、empi = '(')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.

38、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 =

39、'(' && 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)/把母式化為合取范式 ,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