实验二王浩算法的实现.docx
- 文档编号:6617603
- 上传时间:2023-05-10
- 格式:DOCX
- 页数:27
- 大小:24.35KB
实验二王浩算法的实现.docx
《实验二王浩算法的实现.docx》由会员分享,可在线阅读,更多相关《实验二王浩算法的实现.docx(27页珍藏版)》请在冰点文库上搜索。
实验二王浩算法的实现
实验二王浩算法的实现
学号:
**********
班级:
计科二班
姓名:
***
一、实验内容:
实现命题逻辑框架内的王浩算法。
⑴将命题逻辑中的王浩算法推广至下述命题语言的情形之下:
ⅰ命题变量符号:
,
,
,
ⅱ逻辑连接符:
,
,
,
,
ⅲ间隔符:
,
⑵在上述⑴中所定义的命题语言中实现王浩算法。
二、实验目的
熟练掌握命题逻辑中的王浩算法。
三、实验原理
王浩算法实质上是一个反向推理的过程,它吧给定的公式化成合取范式,然后通过判断每个字句是否恒真的来判定给定的公式是否是恒真的。
设X1,…,Xm,Y1,…Yn是的公式,则相继式X1,…,Xm→Y1,…,Yn的直观含义可以理解为
(X1^…^Xm)→(Y1ˇ…ˇYn),
┌X1ˇ…ˇ┌XmˇY1ˇ…ˇYn。
四、实验源代码
#include
#include
#include
#defineMAX_L5
inti=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(i 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=(current->polar==current->child->polar); current->child=current->child->child; } if(current->next! =NULL)remove(current->next); if(current->child! =NULL)remove(current->child); } voidrestruct(node*head){ node*current=NULL; node*last=NULL; node*newone=NULL,*newtwo=NULL,*newthree=NULL,*newfour=NULL,*newcurrent=NULL; intorder=1; while(order<=4){ last=head; current=last->child; while(current! =NULL){ if((current->kind==variable||current->kind==level)&&order==1){ if(current->next! =NULL&¤t->next->kind==and){ newone=(node*)malloc(sizeof(node)); newone->child=NULL; newone->kind=level; newone->next=NULL; newone->polar=0; newone->s=NULL; newone->start=0; if(last->kind==level){ last->child=newone; } else{ last->next=newone; } newone->next=current->next->next->next; newone->child=current; current->next->next->polar=1-current->next->next->polar; current->next->kind=detrusion; current->next->next->next=NULL; current=newone; } else{ last=current; current=current->next; } } elseif((current->kind==variable||current->kind==level)&&order==2){ if(current->next! =NULL&¤t->next->kind==or){ newone=(node*)malloc(sizeof(node)); newone->child=NULL; newone->kind=level; newone->next=NULL; newone->polar=1; newone->s=NULL; newone->start=0; if(last->kind==level){ last->child=newone; } else{ last->next=newone; } newone->next=current->next->next->next; newone->child=current; current->polar=1-current->polar; current->next->kind=detrusion; current->next->next->next=NULL; current=newone; } else{ last=current; current=current->next; } } elseif((current->kind==variable||current->kind==level)&&order==3){ if(current->next! =NULL&¤t->next->kind==equal){ newone=(node*)malloc(sizeof(node)); newone->child=NULL; newone->kind=level; newone->next=NULL; newone->polar=0; newone->s=NULL; newone->start=0; newtwo=(node*)malloc(sizeof(node)); newtwo->child=NULL; newtwo->kind=level; newtwo->next=NULL; newtwo->polar=1; newtwo->s=NULL; newtwo->start=0; newthree=(node*)malloc(sizeof(node)); newthree->child=NULL; newthree->kind=detrusion; newthree->next=NULL; newthree->polar=1; newthree->s=NULL; newthree->start=0; newfour=(node*)malloc(sizeof(node)); newfour->child=NULL; newfour->kind=level; newfour->next=NULL; newfour->polar=0; newfour->s=NULL; newfour->start=0; if(last->kind==level){ last->child=newone; } else{ last->next=newone; } newone->next=current->next->next->next; newone->child=newtwo; current->next->kind=detrusion; newtwo->child=current; current->next->next->next=NULL; newtwo->next=newthree; newthree->next=newfour; newfour->next=NULL; newcurrent=clone(current); newcurrent->next->kind=detrusion; newfour->child=newcurrent->next->next; newcurrent->next->next->next=newcurrent->next; newcurrent->next->next=newcurrent; newcurrent->next=NULL; current=newone; } else{ last=current; current=current->next; } } elseif(current->kind==level&&order==4){ restruct(current); last=current; current=current->next; } else{ last=current; current=current->next; } } order++; } } voidshow(node*head){ node*current=NULL; current=head; while(current! =NULL){ if(current->kind==level){ if(current->polar==0)printf("! "); if(current->start! =1||(current->polar==0&¤t->child->next! =NULL))printf("("); show(current->child); if(current->start! =1||(current->p
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 实验二 王浩算法的实现 实验 算法 实现