王浩算法实验报告资料

《王浩算法的实现》实验报告一．实验目的熟练掌握命题逻辑中的王浩算法。二．实验内容实现命题逻辑框架内的王浩算法。1.将命题逻辑中的王浩算法推广至下述命题语言的情形之下：(1).命题变量符号：p1,p2,p3,……(2).逻辑连接符：﹁，︿，﹀，-，……(3).间隔符：（，）……2.在上述1中所定义的命题语言中实现王浩算法。三．数据结构给定公式，例如：(p1-(q1-r1))-((p1-q1)-(p1-r1))函数inite主要作用是负责将符号初始化成树的结构。函数clone复制一棵完全相同的符号树。函数restruct查找所有&，|，-等符号，并将其拆分成新形式：！，-符号。函数searching王浩算法的主要函数。函数show和output:显示符号串和推理过程。四．实验结果公式正确公式错误六．实验总结公式不是恒真的时候，不一定是恒假的，王浩算法实质上是一个反向推理过程，它把给定的公式化成合取范式，然后通过判断每个子句是否恒真的来判定给定的公式是否是恒真的。所以，王浩算法不能说明公式恒假，只能说明不是恒真的。由于写程序水平低下，只能借由网上程序。写程序对我来说很困难，缺少练习，所以在能看懂实验题的情况下能写出程序是一个急需提高的水平。附：程序源代码#includestdio.h#includestdlib.h#includestring.h#defineMAX_L5inti=0;intstepcount=1;enumtype{and,or,detrusion,equal,level,variable};structnode{char*s;typekind;intpolar;node*next;node*child;intstart;};structstep{step*child;step*brother;node*lhead;node*rhead;intcount;charname[30];};intinite(char*s,node*head){intlen=strlen(s);intj=0,polar=1;node*current=NULL;node*last=NULL;if(s==NULL)return0;last=head;while(ilen){if(s[i]=='|'){if(!(s[i+1]='Z'&&s[i+1]='A'||s[i+1]='z'&&s[i+1]='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='('&&s[i+1]!='!'||i==0)return0;current=(node*)malloc(sizeof(node));current-kind=or;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;i++;}elseif(s[i]=='&'){if(!(s[i+1]='Z'&&s[i+1]='A'||s[i+1]='z'&&s[i+1]='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='('&&s[i+1]!='!'||i==0)return0;current=(node*)malloc(sizeof(node));current-kind=and;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;i++;}elseif(s[i]=='!'){if(!(s[i+1]='Z'&&s[i+1]='A'||s[i+1]='z'&&s[i+1]='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='('&&s[i+1]!='!')return0;polar=1-polar;i++;}elseif(s[i]=='-'){if(s[i+1]!=''||(s[i+2]!='!'&&s[i+2]!='('&&!(s[i+2]='Z'&&s[i+2]='A'||s[i+2]='z'&&s[i+2]='a'))||i==0)return0;current=(node*)malloc(sizeof(node));current-kind=detrusion;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;i=i+2;}elseif(s[i]==''){if((s[i+1]!='-'||s[i+2]!='')||(s[i+3]!='!'&&s[i+3]!='('&&!(s[i+3]='Z'&&s[i+3]='A'||s[i+3]='z'&&s[i+3]='a')||i==0)&&s[i+3]!='1'&&s[i+3]!='0')return0;current=(node*)malloc(sizeof(node));current-kind=equal;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;i=i+3;}elseif(s[i]='Z'&&s[i]='A'||s[i]='z'&&s[i]='a'){current=(node*)malloc(sizeof(node));current-kind=variable;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;current-s=(char*)malloc(MAX_L*sizeof(char));if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;j=0;while((s[i]='Z'&&s[i]='A'||s[i]='z'&&s[i]='a')||(s[i]='9'&&s[i]='0')){(current-s)[j]=s[i];i++;j++;}if(s[i]!='|'&&s[i]!='&'&&s[i]!='-'&&s[i]!=''&&s[i]!='\0'&&s[i]!=')')return0;(current-s)[j]='\0';polar=1;}elseif(s[i]=='1'||s[i]=='0'){if(s[i+1]!=''&&s[i+1]!='-'&&s[i+1]!='&'&&s[i+1]!='|'&&s[i+1]!=')'&&s[i+1]!='\0')return0;current=(node*)malloc(sizeof(node));current-kind=equal;current-s=(char*)malloc(2*sizeof(char));(current-s)[0]=s[i];(current-s)[1]='\0';current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;i++;}elseif(s[i]=='('){if(!(s[i+1]='Z'&&s[i+1]='A'||s[i+1]='z'&&s[i+1]='a')&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='!'&&s[i+1]!='(')return0;current=(node*)malloc(sizeof(node));current-kind=level;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind==level&&last-child==NULL){last-child=current;}else{last-next=current;}last=current;i++;polar=1;if(!inite(s,last))return0;}elseif(s[i]==')'){if(s[i+1]!='P'&&s[i+1]!='1'&&s[i+1]!='0'&&s[i+1]!='-'&&s[i+1]!=''&&s[i+1]!='&'&&s[i+1]!='|'&&s[i+1]!='\0'&&s[i+1]!=')')return0;i++;return1;}elsereturn0;}return1;}node*clone(node*parent){node*son=NULL;if(parent==NULL)returnNULL;son=(node*)malloc(sizeof(node));son-kind=parent-kind;son-polar=parent-polar;son-s=parent-s;son-start=parent-start;if(parent-next!=NULL){son-next=clone(parent-next);}else{son-next=NULL;}if(parent-child!=NULL){son-child=clone(parent-child);}else{son-child=NULL;}returnson;}voidremove(node*head){node*current=NULL;current=head;if(current==NULL)return;if(current-kind==level&¤t-child-kind==variable&¤t-child-next==NULL){current-polar=(current-child-polar==current-polar);current-child-polar=1;}while(current-kind==level&¤t-child-kind==level&¤t-child-next==NULL){current-polar=(