王浩算法c语言实现

大连海事大学人工智能基础课程实验报告（2011-2012学年第一学期）王浩算法班级：学号：姓名：指导老师：2011年12月7日王浩算法的实现一．实验内容实现命题逻辑框架内的王浩算法。1.将命题逻辑中的王浩算法推广至下述命题语言的情形之下：(1).命题变量符号：p1,p2,p3,……(2).逻辑连接符：﹁，︿，﹀，-，……(3).间隔符：（，）……2.在上述1中所定义的命题语言中实现王浩算法。二．实验目的熟练掌握命题逻辑中的王浩算法。三．实验要求1.实验题目必须由个人独立完成，允许自行参考相关文献资料，但严禁同学间相互拷贝和抄袭程序以及文档资料。实验结束后一周内上交实验报告和实验文档资料。2.提交的文档资料包括设计文档和程序源代码。设计文档和程序源代码以书面文档方式提供（用A4纸打印），并提交电子文档备查。四．数据结构给定公式，例如：(p1-(q1-r1))-((p1-q1)-(p1-r1))函数inite主要作用是负责将符号初始化成树的结构。函数clone复制一棵完全相同的符号树。函数restruct查找所有&，|，-等符号，并将其拆分成新形式：！，-符号。函数searching王浩算法的主要函数。函数show和output:显示符号串和推理过程。五．实验结果公式正确公式错误六．实验总结公式不是恒真的时候，不一定是恒假的，王浩算法实质上是一个反向推理过程，它把给定的公式化成合取范式，然后通过判断每个子句是否恒真的来判定给定的公式是否是恒真的。所以，王浩算法不能说明公式恒假，只能说明不是恒真的。程序中的move函数十分重要，有的时候可能出现程序不能运行的情况所以，写这个函数时候是非常谨慎小心的。附：程序源代码#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