人工智能化為子句集的九步法實(shí)驗(yàn)

1、化為子句集的九步法實(shí)驗(yàn)報(bào)告實(shí)驗(yàn)?zāi)康?. 熟悉謂詞公式化為子句集的九個(gè)步驟2. 理解消解（謂詞公式化為子句集）規(guī)則，能把任意謂詞公式轉(zhuǎn)換成子句集。3. 學(xué)會謂詞公式化為子句集實(shí)驗(yàn)原理任一謂詞公式通過九步法可以化成一個(gè)子句集。九步法消解包括消去蘊(yùn)含和等價(jià)符號、把否定符號移到緊靠謂詞的位置上、變量標(biāo)準(zhǔn)化、消去存在量詞、化為前束型、化為Skolem標(biāo)準(zhǔn)形、略去全稱量詞、消去合取詞，把母式用子句集表示、子句換變量標(biāo)準(zhǔn)化，依次變換即可得到子句集。實(shí)驗(yàn)條件1. Window NT/xp/7及以上的操作系統(tǒng)2. 內(nèi)存在512M以上3. CPU在奔騰II以上實(shí)驗(yàn)內(nèi)容熟悉謂詞公式轉(zhuǎn)換成子句集的步驟，子句集轉(zhuǎn)換演示

2、程序參考界面如下圖1所示。圖1 子句集轉(zhuǎn)換演示程序參考界面實(shí)驗(yàn)分析1. 對默認(rèn)謂詞公式進(jìn)行轉(zhuǎn)換。進(jìn)入程序，點(diǎn)擊“語法檢查”，再依次點(diǎn)擊消解過程的九個(gè)步驟按鈕，得到轉(zhuǎn)換結(jié)果。2. 自定義轉(zhuǎn)換目標(biāo)。點(diǎn)擊“清除”刪除默認(rèn)公式，利用界面鍵盤輸入新的轉(zhuǎn)換目標(biāo)，用“大寫字母”、“小寫字母”按鍵進(jìn)行輸入中的字母變換。3. 語法檢查。點(diǎn)擊“語法檢查”檢查輸入謂詞公式的語法錯(cuò)誤。如無錯(cuò)誤，則依次點(diǎn)擊步驟按鈕進(jìn)行轉(zhuǎn)換。4. 重復(fù)運(yùn)行2、3步，熟悉消解原理和轉(zhuǎn)換過程。程序代碼/化為子句集的九步法演示/作者:RanchoChan/時(shí)間/有bug#include#include#include#includeusing

3、 namespace std;/一些函數(shù)的定義void initString(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);/把母式化為

4、合取范式string del_all(string 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ù)字

5、顯示為字符/主函數(shù)void main()cout-求子句集九步法演示-P);/orign = (#x)y(x);/orign = (x)x!b(x);/orign = (x!y);/orign = (a(b);string orign,temp;char command,command0,command1,command2,command3,command4,command5,command6,command7,command8,command9,command10;/=cout請輸入(Y/y)初始化謂詞演算公式command;if(command = y | command = Y)init

6、String(orign);elseexit(0);/=cout請輸入(Y/y)消除空格command0;if(command0 = y | command0 = Y)/del_blank(orign);/undonecout消除空格后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)消去蘊(yùn)涵項(xiàng)command1;if(command1 = y | command1 = Y)orign =del_inlclue(orign);cout消去蘊(yùn)涵項(xiàng)后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)減少否定符號的轄域command2;i

7、f(command2 = y | command2 = Y)dotemp = orign;orign = dec_neg_rand(orign);while(temp != orign);cout減少否定符號的轄域后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)對變量進(jìn)行標(biāo)準(zhǔn)化command3;if(command3 = y | command3 = Y)orign = standard_var(orign);cout對變量進(jìn)行標(biāo)準(zhǔn)化后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)消去存在量詞command4;if(com

8、mand4 = y | command4 = Y)orign = del_exists(orign);cout消去存在量詞后是(w = g(x)是一個(gè)Skolem函數(shù))endlorignendl;elseexit(0);/=cout請輸入(Y/y)化為前束形command5;if(command5 = y | command5= Y)orign = convert_to_front(orign);cout化為前束形后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)把母式化為合取方式command6;if(command6 = y | command6 = Y)

9、orign = convert_to_and(orign);cout把母式化為合取方式后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)消去全稱量詞command7;if(command7 = y | command7 = Y)orign= del_all(orign);cout消去全稱量詞后是endlorignendl;elseexit(0);/=cout請輸入(Y/y)消去連接符號command8;if(command8 = y | command8 = Y)orign = del_and(orign);cout消去連接符號后是endlorignendl;

10、elseexit(0);/=cout請輸入(Y/y)變量分離標(biāo)準(zhǔn)化command9;if(command9 = y | command9 = Y)orign = change_name(orign);cout變量分離標(biāo)準(zhǔn)化后是(x1,x2,x3代替變量x)endlorignendl;elseexit(0);/=cout-完畢-endl;cout(請輸入Y/y)結(jié)束endl;dowhile(y = getchar() | Y=getchar();exit(0);void initString(string &ini)char commanda,commandb;cout請輸入您所需要轉(zhuǎn)換的謂詞公

11、式endl;cout需要查看輸入幫助(Y/N)? commanda;if(commanda = Y | commanda = y)cout,全稱量詞為,存在量詞為#,endl取反為,吸取為!,合取為%,左右括號分別為( 、 )，函數(shù)名請用一個(gè)字母endl;cout請輸入(y/n)選擇是否用戶自定義commandb;if(commandb =Y| commandb=y)cinini;elseini = (x)(P(x)(y)(P(y)P(f(x, y)%(y)(Q(x,y)P(y);cout原始命題是endlini蘊(yùn)涵項(xiàng)/ab變?yōu)閍!bchar ctemp100=;string output;i

12、nt length = temp.length();int i = 0,right_bracket = 0,falg= 0;stack stack1,stack2,stack3;strcpy_s(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;else if() = ctempi)rig

13、ht_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();stac

14、k1.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 stack1,stack2;queue queue1;strcpy_s(ctemp,temp

15、.c_str();/復(fù)制到字符數(shù)組中while(ctempi != 0 & i =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;s

16、tring output1;stack stack11,stack22;int falg1 = 0;int times = 0;int length1 = temp.length(),inleftbackets = 1,j = 0;strcpy_s(ctemp1,temp.c_str();while(ctemp1j != 0 & j =0 & times = 0)stack11.push(ctemp1j);if(ctemp1j = ()inleftbackets +;else if(ctemp1j = )inleftbackets -;if(inleftbackets = 1 & ctemp1

17、j+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.p

18、ush();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.leng

19、th();stack stack13,stack23;int flag = 0,bflag = 0;strcpy_s(ctemp3,temp.c_str();/復(fù)制到字符數(shù)組中while(ctemp3k != 0 & k =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.pu

20、sh(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= ;strcpy_s(ctemp,temp.c_str();stack stack1,stack2;int l_bracket = 1,falg = 0,bracket =

21、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_

22、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-;i

23、f(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_s(c

24、temp,temp.c_str();int left_brackets = 0,i = 0,falg = 0;queue 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(

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

26、;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 conver

27、t_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(ctempi = ( & ctempi+1 = )i = i + 4;flag = 1;elseoutput = output + ctempi;i +;return output;string del_and(string temp)/消去