實驗二 王浩算法的實現(xiàn)

1、實驗二 王浩算法的實現(xiàn)一 實驗?zāi)康模菏炀氄莆彰}邏輯中的王浩算法。二 實驗內(nèi)容實現(xiàn)命題邏輯框架內(nèi)的王浩算法。 將命題邏輯中的王浩算法推廣至下述命題語言的情形之下: 命題變量符號：， 邏輯連接符：， 間隔符：， 在上述中所定義的命題語言中實現(xiàn)王浩算法。三 程序功能：輸入命題邏輯公式，程序?qū)⒆詣舆M(jìn)行推理，并判斷公式的真假性。四 主要數(shù)據(jù)結(jié)構(gòu)（1）term類：用于存放推理過程中的邏輯連接符和間隔符。（2）wanghao類：用于完成整個推理過程。五 主要函數(shù)功能，參數(shù)說明（1）main():程序的入口函數(shù)，無參數(shù)傳遞。（2）input():功能：從屏幕上讀入命題邏輯公式，并將其存入數(shù)組和term里（3

2、）simple():功能：對輸入的公式進(jìn)行化簡，將, - & | 消去，全部轉(zhuǎn)換成原子，或原子的非。=左部的逗號代表與，右邊的逗號代表或。規(guī)則：p-q p|q（4）reason():功能：對公式進(jìn)行推理，推理規(guī)則為：若p,q=x,r，則p,x,q=r.若p,x=q,r，則p=q,x,r若p,x,q=r且p,y,q=r，則p,(x-y),q=r若p=q,x,y,r且q=q,(x-y),r（5）move():功能：移動等式左右兩邊的原子。=左邊含有原子或公式的否定，則移到右邊并取反。同理，右邊含有原子或公式的否定，則移到左邊并取反。最終使左右兩邊都只含有原子。（6）judge():功能：判斷公式是

3、否恒真，通過判斷最終等式兩邊是否含有相同的元素來判斷是否恒真。（7）output():功能：輸出邏輯公式六編程過程中遇到的問題及解決方案1.符號的存儲：再輸入過程中區(qū)分符號和字母很困難，而且不容易存儲，為此引入了term類，類中有符號和字母兩個變量，分別用于存放符號和字母。當(dāng)遇到，-，&，|，和符號，含有&的公式放在=左部，&用逗號表示，含有|的公式放在=右部，|用逗號表示，按照下列規(guī)則移動=左右兩邊的原子或公式，最終消去，化成只含有原子的公式。若p,q=x,r，則p,x,q=r.若p,x=q,r，則p=q,x,r若p,x,q=r且p,y,q=r，則p,(x-y),q=r若p=q,x,y,r且

4、q=q,(x-y),r3.判別：=左右含有相同的原子，則公式恒真。七測試輸入公式(a-(b-c)-(a-b)-(a-c),運行結(jié)果為：程序代碼：import java.io.bufferedreader;import java.io.inputstreamreader;import java.io.ioexception;import java.util.vector;/設(shè)置term類，用于存儲輸入的公式和推倒過程中的公式class term char fuhao;char zimu;term (char fuhao,char zimu) this.fuhao = fuhao;this.zim

5、u = zimu;term()public string tostring() if(fuhao = $)return string.valueof(zimu);else return string.valueof(fuhao)+string.valueof(zimu);public class wanghao vector left = new vector();vector right = new vector();/輸入公式，并將其存入term類的數(shù)組中public void input() bufferedreader br = new bufferedreader(new input

6、streamreader(system.in);string words = new string();system.out.println(請輸入公式行: (例如： a-(b&c)|ab );trywords = br.readline();catch(ioexception e)system.out.println(input error);system.exit(0);char ch = words.tochararray();for(int i = 0 ; i ch.length ; i +) if(chi = | chi = - | chi = & | chi = |) term t

7、 = new term();t.fuhao = chi+;t.zimu = chi;right.add(t);else if(chi = ) term t = new term();t.fuhao = chi+;t.zimu = chi+;right.add(t);else term t = new term();t.fuhao = $;t.zimu = chi;right.add(t);/輸出公式的函數(shù)public void output() for(int i=0;ileft.size();i+)system.out.print(left.elementat(i).tostring();i

8、f(left.elementat(i).fuhao = );system.out.print(=);for(int i=0;iright.size();i+)system.out.print(right.elementat(i).tostring();if(right.elementat(i).fuhao = );system.out.println();/化簡公式，將-,消去 ，并把&,|用逗號表示，=左邊為&，右邊為|public void simple() for(int i = 0;i right.size();i+) if(right.elementat(i).fuhao != &

9、& right.elementat(i).fuhao != | & right.elementat(i).fuhao != = 0;j-)if(right.elementat(j).zimu = )count+;else if(right.elementat(j).zimu = ()count-;if(count = 0)right.add(j, new term(,();break;i+;right.elementat(i).fuhao = -;right.elementat(i).zimu = ;if(right.elementat(i+1).fuhao = )right.elementa

10、t(i+1).fuhao=$;else right.elementat(i+1).fuhao=;for(int j = i+1;j right.size();j+)if(right.elementat(j).zimu = ()count+;else if(right.elementat(j).zimu = )count-;if(count = 0)if(j+1 = 0;j-)if(right.elementat(j).zimu = )count+;else if(right.elementat(j).zimu = ()count-;if(count = 0)if(right.elementat

11、(j).fuhao = )right.elementat(j).fuhao=$;else right.elementat(j).fuhao=;right.add(j, new term($,();break;i+;right.elementat(i).fuhao = -;right.elementat(i).zimu = ;for(int j = i+1;j right.size();j+)if(right.elementat(j).zimu = ()count+;else if(right.elementat(j).zimu = )count-;if(count = 0)if(j+1 rig

12、ht.size()right.add(j+1, new term($,);else right.add(new term($,);break;else if(right.elementat(i).fuhao = ) vector l = new vector();vector r = new vector();int j=i-1;int count =0;while(j=0)if(right.elementat(j).zimu = )count+;else if(right.elementat(j).zimu = ()count-;l.add(0,right.elementat(j);righ

13、t.removeelementat(j);j-;i-;if(count = 0)break;j=i+1;while(jright.size()if(right.elementat(j).zimu = ()count+;else if(right.elementat(j).zimu = )count-;r.add(right.elementat(j);right.removeelementat(j);if(count = 0)break;right.removeelementat(i);right.add(i+, new term(,();right.add(i+, new term($,();

14、j=0;while(j);j=0;while(j);right.add(i+, new term(,();j=0;while(j);j=0;while(jl.size()right.add(i+,l.elementat(j+);right.add(i+,new term($,);right.add(i+,new term($,);i-;output();public void reason()for(int i = 0;i = 0;j-)if(right.elementat(j).zimu = )count+;else if(right.elementat(j).zimu = ()count-

15、;if(count = 0)if(right.elementat(j).fuhao = )right.elementat(j).fuhao = $;else if(right.elementat(j).fuhao = $)right.elementat(j).fuhao = ;break;output();move(0,0);/左右兩邊移動原子或公式，移動過程中取反public void move(int l,int r) int le,ri;for(le=0;le= a) & (left.elementat(le).zimu = a) & (left.elementat(le).zimu =

16、 z) | left.elementat(le).zimu = ,)continue;else break;for(ri=0;ri= a) & (right.elementat(ri).zimu = a) & (right.elementat(ri).zimu = z) | right.elementat(ri).zimu = ,)continue;else break;if(le = left.size() & (ri = right.size()return;if(r right.size() & right.elementat(r).fuhao = ) int count = 0,loc

17、 = 0;right.elementat(r).fuhao = $;if(right.elementat(r).zimu != ()if(r = 0) left.add(loc+, right.elementat(r);left.add(loc+, new term($,);else if(left.size() != 0)left.add(new term($,);left.add(right.elementat(r);right.removeelementat(r);if(!right.isempty()right.removeelementat(r);else right.removee

18、lementat(r);count+;if(left.size() != 0)left.add(new term($,);while(true) if(right.elementat(r).zimu = ()count+;else if(right.elementat(r).zimu = )count-;if(count = 0) if(r = 0)left.add(loc+, new term($,);right.removeelementat(r);if(!right.isempty()right.removeelementat(r);break;if(r = 0)left.add(loc

19、+, right.elementat(r);else left.add(right.elementat(r);right.removeelementat(r);else if(r right.size() & right.elementat(r).zimu = () int count=1;right.removeelementat(r);while(true) if(right.elementat(r).zimu = ()count+;else if(right.elementat(r).zimu = )count-;if(count = 0) right.removeelementat(r

20、);break;r+;while(left.size() != 0 & left.elementat(left.size()-1).zimu = ,)left.removeelementat(left.size()-1);if(l left.size() & left.elementat(l).fuhao = ) int count = 0,loc = 0;left.elementat(l).fuhao = $;if(left.elementat(l).zimu != ()if(l = 0) right.add(loc+, left.elementat(l);right.add(loc+, n

21、ew term($,);else if(right.size() != 0)right.add(new term($,);right.add(left.elementat(l);left.removeelementat(l);if(!left.isempty()left.removeelementat(l);else left.removeelementat(l);count+;if(right.size() != 0)right.add(new term($,);while(true) if(left.elementat(l).zimu = ()count+;else if(left.elementat(l).zimu = )count-;if(count = 0) if(l = 0)right.add(loc+, new term($,);left.removeelementat(l);if(!lef