实验二 王浩算法的实现.doc

实验二 王浩算法的实现一 实验目的：熟练掌握命题逻辑中的王浩算法。二 实验内容实现命题逻辑框架内的王浩算法。 将命题逻辑中的王浩算法推广至下述命题语言的情形之下: 命题变量符号：， 逻辑连接符：， 间隔符：， 在上述中所定义的命题语言中实现王浩算法。三 程序功能：输入命题逻辑公式，程序将自动进行推理，并判断公式的真假性。四 主要数据结构（1）term类：用于存放推理过程中的逻辑连接符和间隔符。（2）wanghao类：用于完成整个推理过程。五 主要函数功能，参数说明（1）main():程序的入口函数，无参数传递。（2）input():功能：从屏幕上读入命题逻辑公式，并将其存入数组和term里（3）simple():功能：对输入的公式进行化简，将, - & | 消去，全部转换成原子，或原子的非。=左部的逗号代表与，右边的逗号代表或。规则：p-q p|q（4）reason():功能：对公式进行推理，推理规则为：若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():功能：判断公式是否恒真，通过判断最终等式两边是否含有相同的元素来判断是否恒真。（7）output():功能：输出逻辑公式六编程过程中遇到的问题及解决方案1.符号的存储：再输入过程中区分符号和字母很困难，而且不容易存储，为此引入了term类，类中有符号和字母两个变量，分别用于存放符号和字母。当遇到，-，&，|，和符号，含有&的公式放在=左部，&用逗号表示，含有|的公式放在=右部，|用逗号表示，按照下列规则移动=左右两边的原子或公式，最终消去，化成只含有原子的公式。若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),r3.判别：=左右含有相同的原子，则公式恒真。七测试输入公式(a-(b-c)-(a-b)-(a-c),运行结果为：程序代码：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 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类的数组中public void input() bufferedreader br = new bufferedreader(new inputstreamreader(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 = 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);/输出公式的函数public void output() for(int i=0;ileft.size();i+)system.out.print(left.elementat(i).tostring();if(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 != & & 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.elementat(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(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 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.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.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.elementat(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;for(le=0;le= a) & (left.elementat(le).zimu = a) & (left.elementat(le).zimu = 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 = 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.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($,);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.elementat(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).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($,);left.removeelementat(l);if(!lef