实验二王浩算法的实现

1、实验二 王浩算法的实现一. 实验目的：熟练掌握命题逻辑中的王浩算法。二. 实验内容实现命题逻辑框架内的王浩算法。将命题逻辑中的王浩算法推广至下述命题语言的情形之下：i 命题变量符号： pl , p2 , p3 , ii逻辑连接符： ，iii间隔符：(，) 在上述中所定义的命题语言中实现王浩算法。三. 程序功能：输入命题逻辑公式，程序将自动进行推理，并判断公式的真假性。四. 主要数据结构(1) term类：用于存放推理过程中的逻辑连接符和间隔符。(2) wanghao类：用于完成整个推理过程。五. 主要函数功能，参数说明(1) ma in ():程序的入口函数，无参数传递。(2) input()

2、:功能：从屏幕上读入命题逻辑公式，并将其存入数组和term里(3) simple。：功能：对输入的公式进行化简，将,- & |消去，全部转换成原子，或原子的非。= 左部的逗号代表与，右边的逗号代表或。规则：p-qp|q(4) reason。：功能：对公式进行推理，推理规则为：若 p,q=x,r，贝卩 p,x,q=r.若 p,x=q,r，贝U 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():功能：移动等式左右两边的原子。= 左边含有原子或公式的否定，则移到右边并取反。同理，右边含有原子或公式的

3、否定，则移到左边并取反。最终使左右 两边都只含有原子。(6) judge():功能：判断公式是否恒真， 通过判断最终等式两边是否含有相同的元素来判断是否 恒真。(7) output。：功能：输出逻辑公式六. 编程过程中遇到的问题及解决方案1符号的存储：再输入过程中区分符号和字母很困难，而且不容易存储，为此引入了term类，类中有符号和字母两个变量，分别用于存放符号和字母。当遇到，-, & ,和 符号，含有&的公式放在=左部，&用逗号表示，含有|的公式放在= 右部，|用逗号表示，按照下列规则移动= 左右两边的原子或公式，最终消去，化成只含有原子的公式。若 p,q=x,r，贝卩 p,x,q=r.若

4、 p,x=q,r，贝U 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),r3.判别：= 左右含有相同的原子，则公式恒真。七. 测试输入公式(A-(B-C)-(A-B)-(A-C),运行结果为： Jev削dgj 呈 Consol 盘Wutgh&o Ja.va rflppli cati on C:AFTogr am Fil电八Gdimil电讥匚onraombini量丁谙输入公武存;(例如:| |AB)I_ ( (A_B - |= (Ar (-E,C) ), (AfC) “匕0从釦叫八强疋)C,(-A, C匚Cf A

5、J f Z , A / P Si r J 二公式恒真！程序代码：import java.io.BufferedReader; import java.io.InputStreamReader;import java.io.IOException; import java.util.Vector;/设置 term 类，用于存储输入的公式和推倒过程中的公式 class term char fuhao;char zimu;term (char fuhao,char zimu) this.fuhao = fuhao; this.zimu = zimu;term()public String toStr

6、ing() 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 类的数组中 public void input() BufferedReader br = new BufferedReader(new InputStreamReader(System.in); Stri

7、ng 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 = new term();t.fuhao

8、 = 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);/输出公式的函数 public void output() for(int i=0;ileft.size();i+) System.out.print(left.elementAt(i).toString(); if(left.elementA

9、t(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 != & & right

10、.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.elementAt

11、(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.ele

12、mentAt(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

13、= 0)if(j+1 right.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

14、.elementAt(j); right.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

15、.add(i+, new term($,();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.eleme

16、ntAt(j).zimu = ()count-;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;= z) | Z) |= z) | Z) |for(le=0;le= a) & (left.elemen

17、tAt(le).zimu (left.elementAt(le).zimu = A) & (left.elementAt(le).zimu = left.elementAt(le).zimu = ,)continue; else break;for(ri=0;ri= a) & (right.elementAt(ri).zimu (right.elementAt(ri).zimu = A) & (right.elementAt(ri).zimu = right.elementAt(ri).zimu = ,)continue; else break;if(le = left.size() & (r

18、i = right.size()return;if(r right.size() & right.elementAt(r).fuhao = ) int count = 0,loc = 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.elemen

19、tAt(r);right.removeElementAt(r);if(!right.isEmpty() right.removeElementAt(r);else right.removeElementAt(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($

20、,);right.removeElementAt(r); if(!right.isEmpty()right.removeElementAt(r);break;if(r = 0)left.add(loc+, 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.element

21、At(r).zimu = ()count+; else if(right.elementAt(r).zimu = )count-; if(count = 0) right.removeElementAt(r);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

22、).fuhao = $; if(left.elementAt(l).zimu != ()if(l = 0) right.add(loc+, left.elementAt(l); right.add(loc+, new 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($,); lef