谓词逻辑归结原理源代码
#include<iostream.h>#include<string.h>#include<stdio.h>#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;i<strlen(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;i<count;i+) if(!(u+i)->s) 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;i<j&&k>0;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=null; k-; cout<<"gjvjkhllknkln"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:unifier()count=0;unit0.s=null;void unifier:input() cout <<endl<< "请输入原子谓词公式的个数(输入0退出) " cin>>num; string=new charnum*50; cout<<"请注意:公式的输入不能出错!"<<endl; for(int j=1;j<=num;j+) cout << "请输入第" << j << "个原子谓词公式(字符个数不超过50个)" <<endl; cin>>(string+(j-1)*50); int unifier:change(int i,int j,int n)char temp210;temp00=stringi+;temp10=stringj+; if(stringi!='(') temp01='0' else int k=1,flag=1; temp0k+=stringi+; while(flag!=0)&&k<10) 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=temp10; 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 if(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;i<j;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); delete uniti.s; uniti.s=p; sort(unit,count); return 0;void unifier:print() cout <<"The MGU is " for(int i=1;i<count+1;i+) cout <<(uniti).s<<"/"<<uniti.var; if(i<count) cout<<"," int once() unifier form; form.input(); if(form.num<2) cout<<"The MGU is empty!"<<endl; return form.num; int k=form.differ(0); if(k=1&&form.num=2) cout<<"The MGU is empty!"<<endl; return form.num; if(k=2) cout<<"The 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) cout<<"The MGU is not exist!"<<endl; return form.num; form.print(); return form.num; for(k=0;k<form.num-1;k+) if(form.differ(k)=2) cout<<"The MGU do not exist!"<<endl; return form.num; form.print();int main() int i=once(); while(i!=0) i=once();return 0;
