谓词逻辑归结原理源代码

《谓词逻辑归结原理源代码》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、#include#include#include#definenull0typedefstruct{charvar;char*s;}mgu;voidstrreplace(char*string,char*str1,char*str2){char*p;while(p=strstr(string,str1)){inti=strlen(string);intj=strlen(str2);*(string+i+j-1)='';for(in

2、tk=i-1;(string+k)!=p;k--)*(string+k+j-1)=*(string+k);for(i=0;is))continue;if((u+i)->var==(u+j)->var){delete(u+j)->s

3、;(u+j)->s=null;k--;j=i;}if(((u+i)->s)&&((u+i)->var==*((u+i)->s))){delete(u+i)->s;(u+i)->s=null;k--;}}j=count;if(k==j)return;count=k;for(inti=1;i0;i++){if((u+i)->s)continue;while(!((u+j)->s))j--;(u+i)->var=(u+j)->var;(u+i)->s=(u+j)->s;(u+j)->s=n

4、ull;k--;}cout<<"gjvjkhllknkln";}classunifier{char*string;mguunit[50];intcount;public:intnum;unifier();voidinput();intdiffer(intn);intchange(inti,intj,intn);voidprint();~unifier(){deletestring;}};unifier::unifier(){count=0;unit[0].s=null;}voidunifier:

5、:input(){cout<>num;string=newchar[num*50];cout<<"请注意:公式的输入不能出错!"<>(string+(j-1)*50);}}intunifier::change(inti,intj,intn){chartemp[2][10];te

6、mp[0][0]=string[i++];temp[1][0]=string[j++];if(string[i]!='(')temp[0][1]='';else{intk=1,flag=1;temp[0][k++]=string[i++];while((flag!=0)&&k<10){if(string[i]=='(')flag++;elseif(string[i]==')')flag--;temp[0][k++]=string[i++];}temp[0][k]='';}temp[1][

7、1]='';if(strlen(temp[1])==1){if(strstr(temp[0],temp[1]))return2;strreplace(string+n*50,temp[1],temp[0]);strreplace(string+(n+1)*50,temp[1],temp[0]);count++;intm=count;unit[m].var=temp[1][0];char*p=newchar[strlen(temp[0])+1];unit[m].s=p;strcpy(p,tem

8、p[0]);}return1;}intunifier::differ(intn){inti=n*50,j=(n+1)*50;while((string[i]!='')&&(string[j]!='')&&(string[i]==string[j])){i++;j++;}if(string[i]==''

9、

10、string[j]=='')return1;intk;if(string[i+1]=='(')k=change(i,j,n);elseif(string[j+1]=='(')k=