《谓词逻辑归结原理源代码》由会员分享，可在线阅读，更多相关《谓词逻辑归结原理源代码（6页珍藏版）》请在金锄头文库上搜索。
1、#include#include#include#define null 0typedef struct char var; char *s;mgu;void strreplace(char *string,char *str1,char *str2) char *p; while(p=strstr(string,str1) int i=strlen(string); int j=strlen(str2); *(string+i+j-1)=0; for(int k=i-1;(string+k)!=p;k-) *(string+k+j-1)=*(string+k); for(i=0;istrle
2、n(str2);i+) *(p+)=*(str2+i); void sort(mgu *u,int count) int j=count; int k=j; if(count=1)return; for(int i=1;is) continue; if(u+i)-var=(u+j)-var) delete (u+j)-s; (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(int i=1;i0;i
3、+) 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=null; k-; coutgjvjkhllknkln;class unifier char *string; mgu unit50; int count;public:int num;unifier();void input();int differ(int n);int change(int i,int j,int n);void print();unifier()delete string;unifier:
4、unifier()count=0;unit0.s=null;void unifier:input() cout endlnum; string=new charnum*50; cout请注意:公式的输入不能出错!endl; for(int j=1;j=num;j+) cout 请输入第 j 个原子谓词公式(字符个数不超过50个) (string+(j-1)*50); int unifier:change(int i,int j,int n)char temp210;temp00=stringi+;temp10=stringj+; if(stringi!=() temp01=0; else in
5、t k=1,flag=1; temp0k+=stringi+; while(flag!=0)&k10) if(stringi=() flag+; else if(stringi=) flag-; temp0k+=stringi+; temp0k=0; temp11=0; if(strlen(temp1)=1) if(strstr(temp0,temp1) return 2; strreplace(string+n*50,temp1,temp0); strreplace(string+(n+1)*50,temp1,temp0); count+; int m=count; unitm.var=te
6、mp10; char *p=new charstrlen(temp0)+1; unitm.s=p; strcpy(p,temp0); return 1; int unifier:differ(int n) int i=n*50,j=(n+1)*50; while(stringi!=0)&(stringj!=0)&(stringi=stringj) i+;j+; if(stringi=0|stringj=0) return 1; int k; if(stringi+1=() k=change(i,j,n); else if(stringj+1=() k=change(j,i,n); else i
7、f(stringj=x|stringj=y|stringj=z|stringj=u| stringj=v|stringj=w) k=change(i,j,n); else k=change(j,i,n); if(k=2) return k; j=count; char c2,*p; for(i=1;ij;i+) c0=unitj.var; c1=0; if(!strstr(uniti.s,c) continue; p=new charstrlen(unitj.s)+strlen(uniti.s)+1; strcpy(p,uniti.s); strreplace(p,c,unitj.s); de
8、lete uniti.s; uniti.s=p; sort(unit,count); return 0;void unifier:print() cout The MGU is ; for(int i=1;icount+1;i+) cout (uniti).s/uniti.var; if(icount) cout,; int once() unifier form; form.input(); if(form.num2) coutThe MGU is empty!endl; return form.num; int k=form.differ(0); if(k=1&form.num=2) co
9、utThe MGU is empty!endl; return form.num; if(k=2) coutThe MGU is not exist!endl; return form.num; else if(k=0&form.num=2) while(k!=1) k=form.differ(0); if(k=2) coutThe MGU is not exist!endl; return form.num; form.print(); return form.num; for(k=0;kform.num-1;k+) if(form.differ(k)=2) coutThe MGU do not exist!endl; return form.num; form.print();int main() int i=once(); while(i!=0) i=once();return 0;
