#include <iostream> #include <string> #include <vector> #include<stack> using namespace std; /*struct类的定义*/ struct transform { string t_f1; string t_f2; }; /*函数声明*/ bool same(const string f1,const string f2) ; transform dif(const string f1,const string f2); string change(string f,transform q); string change2(string f,transform q); bool syncretism(const string f1,const string f2, vector<transform> & ); int legal(transform &); bool var(const string s); string varData(string s); int panduan(string a); int count(string f); /*主函数*/ int main() { system("color F0"); /*adjust the blackground color*/ cout<<"-------欢迎来到合一算法--------"<<endl; cout<<"-------请按照下面格式输入------"<<endl; cout<<"-------命题：A，B，C，D，E，F--"<<endl; cout<<"-------谓词：P，Q，R，S，T-----"<<endl; cout<<"-------常量：a,b,c,d,e---------"<<endl; cout<<"-------函数：f,g,h-------------"<<endl; cout<<"-------变元：u,v,w,x,y,z-------"<<endl; cout<<"请以字符串形式输入两个合法名词."<<endl; /*以字符串形式输入两个谓词公式*/ string f1,f2; cout<<"-------intput F1---------------"<<endl; cin>>f1; cout<<"-------intput F2---------------"<<endl; cin>>f2; cout<<"--------------------------------"<<endl; cout<<"--------------------------------"<<endl; int u=panduan(f1); int v=panduan(f2); if(u==2||v==2) { cout<<"输入命题不合法"<<endl; return 0; } if(u==1||v==1) { cout<<"输入命题含有普通命题，无法合一"; return 0; } cout<<f1<<"的参数个数为："<<count(f1)<<endl; cout<<f1<<"的参数个数为："<<count(f1)<<endl; vector <transform> mgu; if(syncretism(f1,f2,mgu))//存在最一般合一，并输出结果 { cout<<"mgu={ "; int i=0; for(i=0;i<mgu.size()-1;i++) cout<<mgu[i].t_f1<<"/"<<mgu[i].t_f2<<", "; cout<<mgu[i].t_f1<<"/"<<mgu[i].t_f2<<" }"<<endl; } else //不存在最一般合一 { cout<<"不存在最一般合一"<<endl; } return 0; } /*合一方法，判断是否可进行合一*/ bool syncretism (const string tf1,const string tf2,vector<transform> &mgu) { string f1=tf1, f2=tf2; while(!same(f1,f2))//f1与f2中的符号不完全相同时才进入while循环 { transform t=dif(f1,f2);//得到f1和f2的一个差异集，并把它赋给t int flag=legal(t); if(flag==0) return false; else { mgu.push_back(t); f1=change(f1,mgu.back()); f2=change(f2,mgu.back()); cout<<"合一过程："<<endl; cout<<"f1:"<<f1<<endl; cout<<"f2:"<<f2<<endl; if(same(f1,f2)) break;//f1和f2相同时就停止循环 } } return true; } /*判断两个谓词f1和f2是否相同*/ bool same(const string f1, const string f2) { if(f1.length()==f2.length()) { int i=0; while(i<f1.length()&&f1.at(i)==f2.at(i)) i++; if(i==f1.length()) return true; else return false; } else return false; } /*求解f1和f2的差异集 */ transform dif(const string f1,const string f2) { int i=0; transform t; while(f1.at(i)==f2.at(i))//第i个相等时就转向比较i+1，直到遇到不相等时就跳出while循环 i++; int j1=i; while(j1<f1.length()-1&&f1.at(j1)!=',')//从不相等的部分开始，直到遇到‘，’或到达结尾时跳出while循环 j1++; if(j1-i==0) return t;//说明无差集 t.t_f1=f1.substr(i,j1-i);//将f1中的不相同的项截取出来放入变量t.t_f1中 int j2=i; while(j2<f2.length()-1&&f2.at(j2)!=',') j2++; if(j2-i==0) return t;//无差集 t.t_f2=f2.substr(i,j2-i);//将f2中的不相同的项截取出来放入变量t.t_f2中 while(t.t_f1[j1-i-1]==t.t_f2[j2-i-1])//去除相同的部分 { t.t_f1.erase(j1-1-i); t.t_f2.erase(j2-i-1); j1--; j2--; } return t; } /*判断置换t是否合法*/ int legal(transform &t) { if(t.t_f1.length()==0||t.t_f2.length()==0) return 0; if(var(t.t_f2)) { if(var(t.t_f1)&&(varData(t.t_f1)==varData(t.t_f2)))//不能代换合一 return 0; else return 2; } if(!var(t.t_f1))//若t_f1和t_f2都不是变量，也不能合一 return 0; string temp; temp=t.t_f1; t.t_f1=t.t_f2; t.t_f2=temp;//在t_f1是变量而t_f2不是变量的情况下，交换t_f1和t_f2 return 1; } /*剥去外层括号*/ string varData(string s) { if(s.length()==1||s.length()==0) return s; if(s.length()>1) { int i=0; while(i<s.length()&&s.at(i)!='(') i++; int j=i; while(j<s.length()&&s.at(j)!=')') j++; string ss=s.substr(i+1,j-i-1); return varData(ss); } else return false; } bool var(const string s) { if(s.length()==0) return false; if(s.length()==1&&s[0]>='A'&&s[0]<='Z') return false; if(s.length()>1) { int i=0; while(i<s.length()&&s.at(i)!='(')//略过不是'('的字符 i++; int j=i; while(j<s.length()&&s.at(j)!=')')//略过')'前的字符 j++; string ss=s.substr(i+1,j-i-1);//取出'('和')'之间的串 return var(ss);//递归调用var } else { return true; } } /*该函数查找t_f2在f中的位置并用t_f1替代f中相应的t_f2*/ string change(string f,transform q) { int i=f.find(q.t_f2); while(i<f.length()) { i=f.find(q.t_f2); if(i<f.length()) f=f.replace(i,q.t_f2.length(),q.t_f1); } return f; } /*判断输入字符串是否合法*/ int panduan(string a) { stack<char> s; stack<int> b; int flag=0; if(a[0]=='P'||a[0]=='Q'||a[0]=='R'||a[0]=='S'||a[0]=='T') cout<<a<<"命题为谓词命题"<<endl; else { if(a[0]=='A'||a[0]=='B'||a[0]=='C'||a[0]=='D'||a[0]=='E'||a[0]=='F') { cout<<a<<"命题为普通命题。"<<endl; return 1; } else { cout<<a<<"命题为不合法命题"<<endl; return 2; } } for(int i=1;i<a.length();i++) { if(a[i]!='('&&a[i]!=')') continue; if(a[i]=='(') { s.push('('); b.push(i); } if(a[i]==')') { if(s.empty()) { flag=1; break; } else { s.pop(); int w=b.top(); if(w==1) { b.pop(); } else { if(a[w-1]!='f'&&a[w-1]!='g'&&a[w-1]!='h') flag=1; b.pop(); } } } } if(!s.empty()) flag=1; for(int i=0;i<a.length();i++) { if(a[i]=='('||a[i]==')'||a[i]==','||a[i]=='P'||a[i]!='Q'||a[i]!='R'||a[i]=='S'||a[i]=='T'||a[i]=='f'||a[i]=='g'||a[i]=='h'||a[i]=='a'||a[i]=='b'||a[i]=='c'||a[i]=='d'||a[i]=='e') continue; else { if(a[i]=='x'||a[i]=='y'||a[i]=='z'||a[i]=='u'||a[i]=='v'||a[i]=='w') { } else { flag=1; break; } } } if(flag==0) { cout<<"并且"<<a<<"命题合法。"<<endl; return 0; } else { cout<<"但是"<<a<<"谓词命题为不合法命题。"<<endl; return 2; } } /*计算参数个数*/ int count(string f) { int count=1;; for(int i=0;i<f.length();i++) { if(f[i]==',') count++; } return count; }