1、王浩算法的實現實驗報告一實驗目的熟練掌握命題邏輯中的王浩算法。二實驗內容實現命題邏輯框架內的王浩算法。1.將命題邏輯中的王浩算法推廣至下述命題語言的情形之下：(1).命題變量符號：p1,p2,p3,(2).邏輯連接符：，->，(3).間隔符：（，）2.在上述1中所定義的命題語言中實現王浩算法。三數據結構給定公式，例如：(p1->(q1->r1)->(p1->q1)->(p1->r1)函數inite主要作用是負責將符號初始化成樹的結構。函數clone復制一棵完全相同的符號樹。函數restruct查找所有&，|， <->等符號，并將其拆

2、分成新形式：！，->符號。函數searching王浩算法的主要函數。函數show和output:顯示符號串和推理過程。四實驗結果公式正確 公式錯誤六實驗總結公式不是恒真的時候，不一定是恒假的，王浩算法實質上是一個反向推理過程，它把給定的公式化成合取范式，然后通過判斷每個子句是否恒真的來判定給定的公式是否是恒真的。所以，王浩算法不能說明公式恒假，只能說明不是恒真的。由于寫程序水平低下，只能借由網上程序。寫程序對我來說很困難，缺少練習，所以在能看懂實驗題的情況下能寫出程序是一個急需提高的水平。附：程序源代碼#include<stdio.h>#include<stdlib.h

3、>#include<string.h>#define MAX_L 5int i=0;int stepcount=1;enum typeand,or,detrusion,equal,level,variable;struct nodechar *s;type kind;int polar;node *next;node *child;int start;struct stepstep *child;step *brother;node *lhead;node *rhead;int count;char name30;int inite(char *s,node *head)in

4、t len=strlen(s);int j=0,polar=1;node *current=NULL;node *last=NULL;if(s=NULL)return 0;last=head;while(i<len)if(si='|')if(!(si+1<='Z'&&si+1>='A'|si+1<='z'&&si+1>='a')&&si+1!='1'&&si+1!='0'&&

5、si+1!='('&&si+1!='!'|i=0)return 0;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

6、last->next=current;last=current;i+;else if(si='&')if(!(si+1<='Z'&&si+1>='A'|si+1<='z'&&si+1>='a')&&si+1!='1'&&si+1!='0'&&si+1!='('&&si+1!='!'|i=0)return 0;curren

7、t=(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;elselast->next=current;last=current;i+;else if(si='!')if

8、(!(si+1<='Z'&&si+1>='A'|si+1<='z'&&si+1>='a')&&si+1!='1'&&si+1!='0'&&si+1!='('&&si+1!='!')return 0;polar=1-polar;i+;else if(si='-')if(si+1!='>'|(si+2!='!

9、'&&si+2!='('&&!(si+2<='Z'&&si+2>='A'|si+2<='z'&&si+2>='a')|i=0)return 0;current=(node*)malloc(sizeof(node);current->kind=detrusion;current->s=NULL;current->next=NULL;current->child=NULL;current->po

10、lar=polar;current->start=0;if(last->kind=level&&last->child=NULL)last->child=current;elselast->next=current;last=current;i=i+2;else if(si='<')if(si+1!='-'|si+2!='>')|(si+3!='!'&&si+3!='('&&!(si+3<='Z'&

11、;&si+3>='A'|si+3<='z'&&si+3>='a')|i=0)&&si+3!='1'&&si+3!='0')return 0;current=(node*)malloc(sizeof(node);current->kind=equal;current->s=NULL;current->next=NULL;current->child=NULL;current->polar=polar;current

12、->start=0;if(last->kind=level&&last->child=NULL)last->child=current;elselast->next=current;last=current;i=i+3;else if(si<='Z'&&si>='A'|si<='z'&&si>='a')current=(node*)malloc(sizeof(node);current->kind=variable;curr

13、ent->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;elselast->next=current;last=current;j=0;while(si<='Z'&&si>='A

14、9;|si<='z'&&si>='a')|(si<='9'&&si>='0')(current->s)j=si;i+;j+;if(si!='|'&&si!='&'&&si!='-'&&si!='<'&&si!='0'&&si!=')')return 0;(current->s)

15、j='0'polar=1;else if(si='1'|si='0')if(si+1!='<'&&si+1!='-'&&si+1!='&'&&si+1!='|'&&si+1!=')'&&si+1!='0')return 0;current=(node*)malloc(sizeof(node);current->kind=equal;current->

16、;s=(char*)malloc(2*sizeof(char);(current->s)0=si;(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;elselast->next=current;last=current;i+;else if(si=

17、9;(')if(!(si+1<='Z'&&si+1>='A'|si+1<='z'&&si+1>='a')&&si+1!='1'&&si+1!='0'&&si+1!='!'&&si+1!='(')return 0;current=(node*)malloc(sizeof(node);current->kind=level;current-

18、>s=NULL;current->next=NULL;current->child=NULL;current->polar=polar;current->start=0;if(last->kind=level&&last->child=NULL)last->child=current;elselast->next=current;last=current;i+;polar=1;if(!inite(s,last)return 0;else if(si=')')if(si+1!='P'&&

19、amp;si+1!='1'&&si+1!='0'&&si+1!='-'&&si+1!='<'&&si+1!='&'&&si+1!='|'&&si+1!='0'&&si+1!=')')return 0;i+;return 1;else return 0;return 1;node* clone(node *parent)node *son=NUL

20、L;if(parent=NULL)return NULL;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);elseson->next=NULL;if(parent->child!=NULL)son->child=clo

21、ne(parent->child);elseson->child=NULL;return son;void remove(node *head)node *current=NULL;current=head;if(current=NULL)return;if(current->kind=level&&current->child->kind=variable&&current->child->next=NULL)current->polar=(current->child->polar=current-

22、>polar);current->child->polar=1;while(current->kind=level&&current->child->kind=level&&current->child->next=NULL)current->polar=(current->polar=current->child->polar);current->child=current->child->child;if(current->next!=NULL)remove(cu

23、rrent->next);if(current->child!=NULL)remove(current->child);void restruct(node* head)node *current=NULL;node *last=NULL;node *newone=NULL,*newtwo=NULL,*newthree=NULL,*newfour=NULL,*newcurrent=NULL;int order=1;while(order<=4)last=head;current=last->child;while(current!=NULL)if(current-

24、>kind=variable|current->kind=level)&&order=1)if(current->next!=NULL&&current->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=leve

25、l)last->child=newone;elselast->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;elselast=c

26、urrent;current=current->next;else if(current->kind=variable|current->kind=level)&&order=2)if(current->next!=NULL&&current->next->kind=or) newone=(node*)malloc(sizeof(node);newone->child=NULL;newone->kind=level;newone->next=NULL;newone->polar=1;newone->

27、;s=NULL;newone->start=0;if(last->kind=level)last->child=newone;elselast->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=newon

28、e;elselast=current;current=current->next;else if(current->kind=variable|current->kind=level)&&order=3)if(current->next!=NULL&&current->next->kind=equal)newone=(node*)malloc(sizeof(node);newone->child=NULL;newone->kind=level;newone->next=NULL;newone->pola

29、r=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->nex

30、t=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;elselast->next=newone

31、;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->

32、kind=detrusion;newfour->child=newcurrent->next->next;newcurrent->next->next->next=newcurrent->next;newcurrent->next->next=newcurrent;newcurrent->next=NULL;current=newone;elselast=current;current=current->next;else if(current->kind=level&&order=4)restruct(c

33、urrent);last=current;current=current->next;elselast=current;current=current->next;order+;void show(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&&current

34、->child->next!=NULL)printf("(");show(current->child);if(current->start!=1|(current->polar=0&&current->child->next!=NULL)printf(")");current=current->next;if(current!=NULL&&current->start=1)putchar(',');else if(current->kind=an

35、d)printf("&");current=current->next;else if(current->kind=or)printf("|");current=current->next;else if(current->kind=detrusion)printf("->");current=current->next;else if(current->kind=equal)printf("<->");current=current->next;

36、else if(current->kind=variable)if(current->polar=0)printf("!");printf("%s",current->s);current=current->next;return;int searching(step *one)node *current=NULL;node *last=NULL;node *newlev=NULL;node *ncurrent=NULL;node *nlast=NULL;step *nextone=NULL;step *nexttwo=NULL;

37、int key=0;int mark=0;int re1=1;int re2=1;nextone=(step*)malloc(sizeof(step);nextone->brother=NULL;nextone->child=NULL;nextone->lhead=NULL;nextone->rhead=clone(one->rhead);nextone->lhead=clone(one->lhead);strcpy(nextone->name,"");one->child=nextone; current=nexton

38、e->rhead;last=current;while(current!=NULL)if(current->polar=0)if(current=nextone->rhead)nextone->rhead=current->next;else last->next=current->next;current->next=NULL;remove(current);current->next=nextone->lhead;nextone->lhead=current;current->polar=1-current->p

39、olar;current->start=1;current=last->next;strcpy(one->name,"根據規(guī)則1");mark=1;key=1;break;else if(current->child->next!=NULL&&current->child->next->kind=detrusion)nlast=current->child;ncurrent=current->child->next;while(ncurrent->next->next!=NULL&

40、amp;&ncurrent->next->next->kind=detrusion)nlast=ncurrent->next;ncurrent=ncurrent->next->next;current->polar=1-current->polar;newlev=(node*)malloc(sizeof(node);newlev->child=ncurrent->next;newlev->kind=level;newlev->polar=1;newlev->next=NULL;newlev->start

41、=1;nlast->next=NULL;remove(newlev);newlev->next=current->next;current->next=NULL;remove(current);current->next=newlev;strcpy(one->name,"根據規(guī)則4");mark=1;key=1;break;elselast=current;current=current->next;current=nextone->lhead;last=current;while(current!=NULL&&

42、;key!=1)if(current->polar=0)if(current=nextone->lhead)nextone->lhead=current->next;else last->next=current->next;current->next=NULL;remove(current);current->next=nextone->rhead;nextone->rhead=current;current->polar=1-current->polar;current->start=1;current=last

43、->next;strcpy(one->name,"根據規(guī)則2");mark=1;key=1;break;else if(current->child->next!=NULL&&current->child->next->kind=detrusion)nexttwo=(step*)malloc(sizeof(step);nexttwo->brother=NULL;nexttwo->child=NULL;nexttwo->lhead=NULL;nexttwo->rhead=clone(nexton

44、e->rhead);nexttwo->lhead=clone(nextone->lhead);strcpy(nexttwo->name,"");nlast=current->child;ncurrent=current->child->next;while(ncurrent->next->next!=NULL&&ncurrent->next->next->kind=detrusion)nlast=ncurrent->next;ncurrent=ncurrent->next-&

45、gt;next;current->polar=1-current->polar;current->start=1;nlast->next=NULL;remove(current);current=nexttwo->lhead;last=current;while(current->child->next=NULL|current->child->next->kind!=detrusion)last=current;current=current->next;nlast=current->child;ncurrent=cur

46、rent->child->next;while(ncurrent->next->next!=NULL&&ncurrent->next->next->kind=detrusion)nlast=ncurrent->next;ncurrent=ncurrent->next->next;newlev=(node*)malloc(sizeof(node);newlev->child=ncurrent->next;newlev->kind=level;newlev->polar=1;newlev->n

47、ext=NULL;newlev->start=1;nlast->next=NULL;if(current=nexttwo->lhead)newlev->next=current->next;nexttwo->lhead=newlev;elsenewlev->next=current->next;last->next=newlev;remove(newlev);nextone->brother=nexttwo;strcpy(one->name,"根據規(guī)則3");mark=1;key=1;break;elselast=current;current=current->next;if(mark=0)one->child=NULL;current=one->lhead;ncurrent=one->rhead;while(current!=NULL)ncurrent=one->rhead;while(ncurrent!=NULL)if(!strcmp(current->