王浩算法c语言实现.doc

大连海事大学
人工智能基础课程实验报告
(2011-2012学年第一学期)
王浩算法
班级:
学号:
姓名:
指导老师:
2011年 12月 7日
王浩算法的实现

实现命题逻辑框架内的王浩算法。
:
(1).命题变量符号:p1,p2,p3,……
(2).逻辑连接符:﹁,︿,﹀,->,……
(3).间隔符:(,)……
。

熟练掌握命题逻辑中的王浩算法。

,允许自行参考相关文献资料,但严禁同学间相互拷贝和抄袭程序以及文档资料。实验结束后一周内上交实验报告和实验文档资料。
。设计文档和程序源代码以书面文档方式提供(用A4纸打印),并提交电子文档备查。

给定公式,例如:(p1->(q1->r1))->((p1->q1)->(p1->r1))
函数inite主要作用是负责将符号初始化成树的结构。
函数clone复制一棵完全相同的符号树。
函数restruct查找所有&,|, <->等符号,并将其拆分成新形式:!,->符号。
函数searching王浩算法的主要函数。
函数show和output:显示符号串和推理过程。

公式正确

公式错误

公式不是恒真的时候,不一定是恒假的,王浩算法实质上是一个反向推理过程,它把给定的公式化成合取范式,然后通过判断每个子句是否恒真的来判定给定的公式是否是恒真的。所以,王浩算法不能说明公式恒假,只能说明不是恒真的。程序中的move函数十分重要,有的时候可能出现程序不能运行的情况所以,写这个函数时候是非常谨慎小心的。
附:程序源代码
#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;
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<len){
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;
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;
current=(node*)malloc(sizeof(node));
current->kind=and;