人工智能实验-王浩算法

2016-2017第1学期《人工智能基础》实验报告

实验名称：王浩算法的实现

专业班级 学号 姓名 1、实验环境 Visual C++ 6.0

2、实验目的和要求 熟练掌握命题逻辑中的王浩算法。 3、解题思路、代码 3.1解题思路 王浩算法实质上是一个反向推理的过程，它把给定的公式化成合取范式，然后通过判断每个字句是否恒真的来判定给定的公式是否是恒真的。

设X1，…，Xm，Y1，…Yn是的公式，则相继式X1，…，Xm → Y1，…，Yn的直观含义可以理解为（X1^…^ Xm）→（Y1ˇ…ˇYn），┌X1ˇ…ˇ┌XmˇY1ˇ…ˇYn。

3.2代码 #include #include #include #define MAX_L 5 int i=0;

int stepcount=1;

enum type{ and,or,detrusion,equal,level,variable };

struct node{ char *s; type kind; int polar; node *next; node *child; int start; };

struct step{ step *child; step *brother; node *lhead; node *rhead;

1 / 18

********* ******** ***** 2016-2017第1学期《人工智能基础》实验报告

int count; char name[30]; };

//初始化，输入表达式

int inite(char *s,node *head){ int len=strlen(s); int j=0,polar=1; node *current=NULL; node *last=NULL; if(s==NULL)return 0; last=head; while(i='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)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{ last->next=current; } last=current; i++; } else 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)return 0;

2 / 18

2016-2017第1学期《人工智能基础》实验报告

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++; } else 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]!='!')return 0; polar=1-polar; i++; } else if(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)return 0; 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;

3 / 18

2016-2017第1学期《人工智能基础》实验报告

} else if(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')return 0; 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; } else if(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++;

4 / 18