下载文档原格式
离散数学谓词逻辑python离散数学是计算机科学中的一门重要学科，它研究离散对象及其相互关系的数学理论和方法。
谓词逻辑是离散数学中的一个重要概念，它用于描述和推理关于对象之间的关系和性质。
在本文中，我们将介绍谓词逻辑在Python编程语言中的应用。
谓词逻辑是一种用于描述和推理关于对象之间关系的形式系统。
它由一组谓词、变量和逻辑连接词组成。
在谓词逻辑中，谓词用于描述对象的性质或关系，变量用于表示未知对象，逻辑连接词用于构建复杂的命题。
在Python中，我们可以使用谓词逻辑来表示和处理关于对象之间的关系和性质。
Python的谓词逻辑库提供了一些函数和方法，可以实现谓词逻辑的基本操作，如命题的合取、析取、否定、存在量化和全称量化等。
在Python中，我们可以使用符号或者关键字来表示谓词逻辑中的各种操作。
例如，我们可以使用符号"∧"表示合取操作，使用符号"∨"表示析取操作，使用关键字"not"表示否定操作，使用关键字"exists"表示存在量化，使用关键字"forall"表示全称量化等。
下面是一个简单的例子，演示了如何使用Python的谓词逻辑库来表示和处理关于人和年龄的关系：```pythonfrom sympy import symbols, Predicate, And, Or, Not, Exists, ForAll# 定义谓词和变量Person = symbols('Person')Age = symbols('Age')Young = Predicate('Young', Age)Old = Predicate('Old', Age)# 定义谓词逻辑公式formula = And(Exists(Person, Young), ForAll(Person, Old))# 打印谓词逻辑公式print(formula)```上述代码中，我们首先引入了Python的谓词逻辑库，并定义了谓词"Young"和"Old"以及变量"Person"和"Age"。
人工智能第3章谓词逻辑与归结原理
1、谓词逻辑是什么？
谓词逻辑（Predicate Logic）是一种通用的符号化语言，用来表达
和分析各种谓词命题（Propositional Statements）的逻辑关系。
它可以
用来表达抽象概念和客观真理，并以精确的形式描述这些概念和真理。
谓
词逻辑最重要的功能是，它能够发现和解决各种类型的逻辑问题，这在人
工智能中显得尤为重要。
2、归结原理是什么？
归结原理是一种认识论。
它提出的基本原则是，如果要获得B给定A，应当给出一个充分陈述，即必须提供一系列真实可信的参数，以及由此产
生B的能力证明，在这种情况下A必须是正确的。
因此，归结原理会被用
来推理。
例如，通过归结原理，如果一个具体的概念被认为是正确的，那
么人们可以得出结论，即所有概念的结果也是正确的。
z3 solver 是微软研究院开发的一款高性能定理证明器，它主要用于解决布尔约束，线性算术约束和非线性约束等问题，被广泛应用于软硬件验证、形式化验证、符号执行、模型检验等领域。
本文将介绍 z3 solver 在谓词编程中的应用示例，并详细阐述其在谓词编程中的重要性和价值。
一、z3 solver 谓词编程的基本概念谓词编程是一种基于谓词逻辑的编程范式，它将程序的状态和行为抽象为谓词，通过对谓词进行推理和求解，来验证程序的正确性和性质。
而 z3 solver 作为一种高效的定理证明器，能够提供强大的谓词求解能力，为谓词编程的实践提供了有力的支持。
二、z3 solver 谓词编程示例接下来，我们将通过一个具体的示例来演示 z3 solver 在谓词编程中的应用。
假设有一个简单的程序，其功能为判断一个整数数组中是否存在重复元素。
此时，我们可以借助 z3 solver 来进行谓词编程，具体步骤如下：1. 定义状态和谓词：我们首先需要定义程序的状态和谓词，其中程序的状态包括输入数组和重复元素的存在性，谓词则是用来描述重复元素的性质。
2. 构造约束条件：接下来，我们需要根据程序的逻辑和性质，构造相应的约束条件，以限定谓词的取值范围。
在本例中，我们可以构造一个关于数组元素不等的约束条件。
3. 运行 z3 solver：将约束条件输入 z3 solver 中，通过调用 z3 solver 的求解接口，来求解谓词的取值。
如果 z3 solver 能够找到符合约束条件的解，即说明程序存在重复元素；如果 z3 solver 无法找到解，即说明程序不存在重复元素。
通过以上步骤，我们可以很方便地利用 z3 solver 来验证程序的正确性和性质，从而提高程序的可靠性和安全性。
三、z3 solver 在谓词编程中的重要性和价值z3 solver 作为一种高性能的定理证明器，具有以下几点重要性和价值：1. 提供强大的谓词求解能力：z3 solver 可以高效地求解包括布尔约束、线性算术约束和非线性约束在内的各种谓词，为谓词编程提供了强大的支持。
#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 unit[50];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;unit[0].s=null;}void unifier::input(){cout <<endl<< "请输入原子谓词公式的个数(输入0退出) "; cin>>num;string=new char[num*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 temp[2][10];temp[0][0]=string[i++];temp[1][0]=string[j++];if(string[i]!='(')temp[0][1]='\0';else{int k=1,flag=1;temp[0][k++]=string[i++];while((flag!=0)&&k<10){if(string[i]=='(')flag++;else if(string[i]==')')flag--;temp[0][k++]=string[i++];}temp[0][k]='\0';}temp[1][1]='\0';if(strlen(temp[1])==1){if(strstr(temp[0],temp[1]))return 2;strreplace(string+n*50,temp[1],temp[0]);strreplace(string+(n+1)*50,temp[1],temp[0]);count++;int m=count;unit[m].var=temp[1][0];char *p=new char[strlen(temp[0])+1];unit[m].s=p;strcpy(p,temp[0]);}return 1;}int unifier::differ(int n){int i=n*50,j=(n+1)*50;while((string[i]!='\0')&&(string[j]!='\0')&&(string[i]==string[j])) {i++;j++;}if(string[i]=='\0'||string[j]=='\0')return 1;int k;if(string[i+1]=='(')k=change(i,j,n);else if(string[j+1]=='(')k=change(j,i,n);else if(string[j]=='x'||string[j]=='y'||string[j]=='z'||string[j]=='u'|| string[j]=='v'||string[j]=='w')k=change(i,j,n);elsek=change(j,i,n);if(k==2)return k;j=count;char c[2],*p;for(i=1;i<j;i++){c[0]=unit[j].var;c[1]='\0';if(!strstr(unit[i].s,c))continue;p=new char[strlen(unit[j].s)+strlen(unit[i].s)+1];strcpy(p,unit[i].s);strreplace(p,c,unit[j].s);delete unit[i].s;unit[i].s=p;}sort(unit,count);return 0;}void unifier::print(){cout <<"The MGU is ";for(int i=1;i<count+1;i++){cout <<(unit[i]).s<<"/"<<unit[i].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;}。
例3.1(永真性判断)给定一阶语言 , 其中 是两个常元,是 元谓词符号, 是不同的变元. 假设 是以下公式:考察公式 :即它的前束范式是:它的 Skolem 范式 是:根据以下语义推出关系:可知:若将 看成是命题变元 , 对于子句集合它具有一个反驳, 这表明它能够语义推出一个恒假式, 所以, 能够语义推出一个恒假式, 因而 是永假的.所以 是永假的.所以 是永真的.□定义3.1(文字,相反文字,子句,子句集合,空子句,基文字,基子句,子句代换,子句集合代换 )对于谓词逻辑, 可以定义类似于命题逻辑的一些概念:z原子公式或者原子公式的非称为文字.谓词逻辑归结法,,,,.L={c1,c2,P,Q}c1,c2P,Q1x,y,zA(^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x))\A\((^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x))),(^xP(x)Z^xQ(x))[]x(\P(x)[\Q(x)).^x^y]z((P(x)Z Q(y))[\P(z)[\Q(z)).C]z((P(c1)Z Q(c2))[\P(z)[\Q(z)).C(P(c1)Z Q(c2))[\P(c1)[\Q(c1)C(P(c1)Z Q(c2))[\P(c2)[\Q(c2)C X P(c1)Z Q(c2)C X\P(c1)C X\Q(c2)P(c1),Q(c2)p,q{p Z q,\p,\q},CC\AA X Xz 若 是原子公式,则 是 的 相反文字,是 的相反文字. z 文字的有限集合称为子句.z 不出现变元的文字称为基文字. z 不出现变元的子句称为基子句. z 空的子句称为空子句.z 子句的有限集合称为子句集合.z称 为一个代换. 若 是文字, 则 表示z若子句 是 , 则 表示□事实3.1(子句集合与 Skolem 范式)子句 也写为 表示的闭包. 子句集合表示以下合取范式的闭包:因而表示一个 Skolem 范式.□例3.2(基本概念)z 与 是相反文字, 但是 与 不是相反文字.z假设代换 , 则 等于 .z基子句 表示 .z子句 表示语句L \L L L \L 5:{x 1/t 1,l ,x m /t m }L 5(L)L x 1,l ,xm t 1,l ,t m.C {L 1,l ,L n }5(C){5(L 1),l ,5(L n )}.{L 1,l ,L n }L 1ZlZ L n L 1ZlZ L n {{L 1,1,l ,L 1,n 1},{L 2,1,l ,L 2,n 2},l ,{L m,1,l ,L m,n m}}(L 1,1ZlZ L 1,n 1)[(L 2,1ZlZ L 2,n 2)[l[(L m,1ZlZ L m,nm).P(c 1)\P(c 1)P(c 1)\P(z)5={z/c 1}5(\P(z))\P(c 1){P(c)}P(c){P(x),Q(y)}]x ]y(P(x)Z Q(y)).z子句集合 表示 Skolem 范式□定义3.2(可满足)给定一阶语言 , 假设 是子句,是字句集合. z的一个解释 满足 , 是指 满足 所表示的语句.记为z若以下条件成立:则称 是 和 的逻辑推论. 记为 .z若存在 的解释满足 , 则称 是可满足的; 否则称 是不可满足的.z解释 满足 是指 满足 所表示的 Skolem 范式.z若存在 的解释满足 , 则称 是可满足的; 否则称 是不可满足的.□例3.3(可满足)给定一阶语言 , 假设 是 元谓词符号,是常元, 是变元. z子句 是可满足的.z□定义3.3(归结子句)给定一阶语言 , 假设 是 的两个子句. 形如的子句称为 与 的归结子句. 其中 是两个代换,而 与 是两个相反的文字.若三个子句 具有上述关系, 则记为 .□例3.4(归结子句)对任意的赋值 , 当 及 时, 有 . {P(x)Z Q(y),P(c)Z\Q(z)}]x ]y ]z ((P(x)Z Q(y))[(P(c)Z\Q(z))).L C,C 1,C 2,C 3S L I C I C I X C I I X C 1I X C 2I X C 3C 3C 1C 2C 1,C 2X C 3L C C C I S I S L S S S L P,Q 1c x,y P(c)Z Q(x)P(c)Z Q(x),\Q(y)P(c).L C 1,C 2L (51(C 1)-{L 1})P (52(C 2)-{L 2})C 1C 251,52L 1J 51(C 1),L 2J 52(C 2),L 1L 2C 1,C 2,C 3C 1,C 2U res C 3X给定一阶语言 , 其中 是常元,是变元, 是 元函数符号, 是 元谓词符号. 有以下归结推出关系:z .z .z .z .z. z假设{ 是 . {是 . 则:□定义3.4(反驳)子句集合 的一个反驳是指子句的有限序列 , 它满足以下条件:z 是 .z对于每个 :{或者 ,{或者存在 使得 . □例3.5(反驳)给定一阶语言 , 其中 是常元,是变元, 是 元谓词符号. 子句集合有一个反驳 , 其中:L ={c,f,g,P,Q}c x,y f,g 11P(c),\P(x)U res P(c)Z Q(x),\Q(y)U res P(c)P(x)Z Q(x),\Q(y)U res P(x)P(x)Z Q(x),\Q(y)U res P(f (x))P(x)Z Q(x),\Q(y)res P(f 2(x))A P(x)Z P(f(y))Z R(g(y))B \P(y)Z\R(y)A,B res P(f(y))Z R(g(y))Z\R(y),A,B res R(g(y))Z\R(f(y)).S {C i |15i 5n}C n `i C i J S j,k<i (15j,k< n )C j ,C k U res C i L ={c 1,c 2,P,Q}c 1,c 2x P,Q 1{P(c 1)Z Q(c 2),\P(x),\Q(x)}{C 1,C 2,C 3,C 4,C 5}C 1:P(c 1)Z Q(c 2)C 2:\P(x)C 3:\Q(x)C 4:Q(c 2)C 1,C 2U res C 4C 5:`C 3,C 4U res C 5`U U U□定理3.1(归结推出与语义推出)给定一阶语言 , 假设 是 的两个子句.证明:从 可知存在代换 及两个相反的文字 与 , 使得 , , 而假设子句 分别表示公式 . 则可知 . 因为 , 所以即:□定理3.2(归结方法的可靠性)给定一阶语言 , 假设 是 的子句集合. 若 有一个反驳, 则 是不可满足的. 证明根据归结一步可以传递可满性, 若 是可满足的, 则它的反驳序列中每个子句都是可满足的, 但最後一个空子句是不可满足的. 所以 是不可满足的.□定理3.3(归结方法的完全性)给定一阶语言 , 假设 是 的子句集合. 若 是不可满足的, 则 有一个反驳.□例3.6(简单证明)给定一阶语言 , 其中 是常元,是变元, 是 元谓词符号. 语句的 Skolem 范式是:所对应的子句集合是:若 则 .L C 1,C 2L C 1,C 2U res C 3C 1,C 2X C 3C 1,C 2U res C 351,52L 1L 2L 1J 51(C 1)L 2J 52(C 2)C 3=(51(C 1)-{L 1})P (52(C 2)-{L 2}).C i 9i 9i X 5i (C i )(i=1,2)(51(C 1)-{L 1})P (52(C 2)-{L 2})C 391,92C 3,91,9293.C 1,C 2X C 3.L S L S S S S L S L S S L ={c 1,c 2,P,Q}c 1,c 2x P,Q 1\((^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x))),]z((P(c 1)Z Q(c 2))[\P(z)[\Q(z)).=X X它有一个反驳:因而是永假的, 即是永真的. 子句集合对应的基实例集合是若将 分别看成是命题变元 , 则上述基实例集合对应于命题逻辑语句集合:它有一个反驳:对应于谓词逻辑的反驳:可以直接转换为最初子句集合的反驳:□例3.7(多种证明)给定一阶语言 , 假设 是 元谓词符号, 是 元谓词符号,是三个不同的变元, 是两个不同的常元. 定义以下公式: {P(c 1)Z Q(c 2),\P(z),\Q(z)},< P (c 1)Z Q(c 2),\P(z),\Q(z),Q(c 2),`> .\((^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x)))(^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x)){P(c 1)Z Q(c 2),\P(z),\Q(z)},{P(c 1)Z Q(c 2),\P(c 1),\P(c 2),\Q(c 1),\Q(c 2),},P(c 1),P(c 2),Q(c 1),Q(c 2)p 1,p 2,q 1,q 2{p 1Z q 2,\p 1,\p 2,\q 1,\q 2},<p 1Z q 2,\p 1,\q 2,q 2,`> .<P (c 1)Z Q(c 2),\P(c 1),\Q(c 2),Q(c 2),`> .< P (c 1)Z Q(c 2),\P(z),\Q(z),Q(c 2),`> .L ={c 1,c 2,P,Q,R,S}P,Q,R 1S 2x,y,z c 1,c 2A :^x(P(x)[]y(R(y)> S (x,y))),B :]x(P(x)>]y(Q(y)> \S(x,y))),C :]x(R(x)>\Q(x)).则 .□证明(解释赋值方法).若 是一个解释. 假设 , 以下证明:z从 , 可知存在 , 使得 , 且对任意的 , 都有当 时z因为 且 , 所以因而 . z所以 .证毕.□证明(归结方法).的转化为:的转化为:的转化为:前提与结论的反面可以转化为以下子句:有以下的归结推出:对任意的 , 当 时 .若 则 , , , ,., , ,,A,B X C I I X A [B a J D I R I (a )=1Q I (a )=0I X A b J D I P I (b )=1a J D I R I (a )=1S I (b ,a )=1.I X B I X P I (b )Q I (a )=1S I (b ,a )=0.Q I (a )=0I X C A ^x(P(x)[]y(R(y)>S (x,y))),^x ]y(P(x)[(R(y)>S (x,y)))^x ]y(P(x)[(\R(y)Z S(x,y)))]y(P(c 1)[(\R(y)Z S(c 1,y)))]x(P(c 1)[(\R(x)Z S(c 1,x))){P(c 1),\R(x)Z S(c 1,x)}B ]x(P(x)> ]y(Q(y)> \S(x,y))),]x ]y(P(x)>(Q(y)> \S(x,y))),]x ]y(\P(x)Z\Q(y)Z\S(x,y)),]]x(\P(y)Z\Q(z)Z\S(y,z)),{\P(y)Z\Q(z)Z\S(y,z)}.\C \]x(R(x)> \Q(x)).^x \(R(x)> \Q(x))^x(R(x)[Q(x))R()[Q(c 2){R(c 2),Q(c 2)}C 1:P(c 1)C 2:\R(x)Z S(c 1,x),C 3:\P(y)Z\Q(z)Z\S(y,z),C 4:R(c 2)C 5:Q(c 2)y c 2所以证毕.□例3.8(语义推出)给定一阶语言 , 为 元谓词符号, 为 元谓词符号, 为元谓词符号,是三个不同的常元.是四个不同的变元.是以下公式:则 .证明的转化为:的转化为:的转化为:的转化为:可得以下子句:有以下的归结关系:,,..,.,.,,.C1,C3Ures\Q(z)Z\S(c1,z),C2,C4UresS(c1,c2),\Q(z)Z\S(c1,z),S(c1,c2)Ures\Q(c2),C5,\Q(c2)Ures`.A,B X C.L={a,b,c,P,Q,R,S}P,S1R2Q 3a,b,c x,y,z,w A,B,C,D ]x]y((Q(x,x,y)[\P(y))> S(x)),^x^y(R(y,x)[\P(x))^x]yQ(x,x,y)^xS(x)A,B,C X DA]x]y((Q(x,x,y)[\P(y))> S(x)),]x]y(\Q(x,x,y)Z P(y)Z S(x)),\Q(x,x,y)Z P(y)Z S(x)B^x^y(R(y,x)[\P(x)){R(b,a),\P(a)}C^x]yQ(x,x,y)Q(c,c,z)\D\^xS(x)]x\S(x)\S(w)\Q(x,x,y)Z P(y)Z S(x)R(b,a),\P(a)Q(c,c,z)\S(w)证毕.□例3.9(不可推出)给定一阶语言 , 为 元谓词符号,是两个不同的常元. 是三个不同的变元. 则证明可以化为:可能的归结推出只有:因而上述子句集合没有反驳. 即□例3.10(符号化与证明)某些学生喜欢每门课程, 没有学生喜欢文学. 因此, 没有课程是文学. 假设学生与课程的集合为论域, 定义以下谓词:则有以下的符号化:z“某些学生喜欢每门课程”的符号化为 :\Q(x,x,y)Z P(y)Z S(x),Q(c,c,z)U res P(y)Z S(c),P(y)Z S(c),\P(a)U res S(c),S(c),\S(w)U res `.L ={c 1,c 2,P,Q}P,Q 1c 1,c 2x,y,z ^xP(x),^xQ(x)X^x(P(x)[Q(x))./^xP(x)[^xQ(x)[\^x(P(x)[Q(x))^xP(x)[^xQ(x)[]x(\P(x)Z\Q(x))^x ^y(P(x)[Q(y))[]x(\P(x)Z\Q(x))^x ^y ]z(P(x)[Q(y)[(\P(z)Z\Q(z)){P(c 1),Q(c 2),\P(z)Z\Q(z)}P(c 1),\P(z)Z\Q(z)U res \Q(c 1),Q(c 2),\P(z)Z\Q(z)U res \P(c 2).^xP(x),^xQ(x)X^x(P(x)[Q(x))./P(x)x D(x)x S(x)x L(x,y)x yA ^x(P(x)[]y(D(y)>L (x,y))).z“没有学生喜欢文学”的符号化为 :z“没有课程是文学”的符号化为 :需要证明假设 是两个不同的常元,是三个不同的变元.的转化为:的转化为:的转化为:有以下归结推出关系:因而□作业全部B\^xy(P(x)[S(y)[L(x,y)).C\^x(D(x)[S(x)).A,B X C.c1,c2x,y,zA^x(P(x)[]y(D(y)> L(x,y))).P(c1),\D(y)Z L(c1,y).P(c1),\D()Z L(c1,z).B\^xy(P(x)[S(y)[L(x,y)).\P(x)Z\S(y)Z\L(x,y).\C\\^x(D(x)[S(x)).^x(D(x)[S(x)).D(c2),S(c2).P(c1),\P(x)Z\S(y)Z\L(x,y)Ures\S(y)Z\L(c1,y),S(c2),\S(y)Z\L(c1,y)Ures\L(c1,c2),\D(z)Z L(c1,z),\L(c1,c2)Ures\D(c2),D(c2),\D(c2)Ures`.A,B X C.z。
#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 unit[50];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;unit[0].s=null;}void unifier::input(){cout <<endl<< "请输入原子谓词公式的个数(输入0退出) "; cin>>num;string=new char[num*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 temp[2][10];temp[0][0]=string[i++];temp[1][0]=string[j++];if(string[i]!='(')temp[0][1]='\0';else{int k=1,flag=1;temp[0][k++]=string[i++];while((flag!=0)&&k<10){if(string[i]=='(')flag++;else if(string[i]==')')flag--;temp[0][k++]=string[i++];}temp[0][k]='\0';}temp[1][1]='\0';if(strlen(temp[1])==1){if(strstr(temp[0],temp[1]))return 2;strreplace(string+n*50,temp[1],temp[0]);strreplace(string+(n+1)*50,temp[1],temp[0]);count++;int m=count;unit[m].var=temp[1][0];char *p=new char[strlen(temp[0])+1];unit[m].s=p;strcpy(p,temp[0]);}return 1;}int unifier::differ(int n){int i=n*50,j=(n+1)*50;while((string[i]!='\0')&&(string[j]!='\0')&&(string[i]==string[j])) {i++;j++;}if(string[i]=='\0'||string[j]=='\0')return 1;int k;if(string[i+1]=='(')k=change(i,j,n);else if(string[j+1]=='(')k=change(j,i,n);else if(string[j]=='x'||string[j]=='y'||string[j]=='z'||string[j]=='u'|| string[j]=='v'||string[j]=='w')k=change(i,j,n);elsek=change(j,i,n);if(k==2)return k;j=count;char c[2],*p;for(i=1;i<j;i++){c[0]=unit[j].var;c[1]='\0';if(!strstr(unit[i].s,c))continue;p=new char[strlen(unit[j].s)+strlen(unit[i].s)+1];strcpy(p,unit[i].s);strreplace(p,c,unit[j].s);delete unit[i].s;unit[i].s=p;}sort(unit,count);return 0;}void unifier::print(){cout <<"The MGU is ";for(int i=1;i<count+1;i++){cout <<(unit[i]).s<<"/"<<unit[i].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;}。
