实现基于谓词逻辑的归结原理

河南城建学院

《人工智能》实验报告

实验名称：实现基于谓词逻辑的归结原理

成绩：________ 专业班级:

学号:

姓名: 实验日期：20 14年05月13日

实验器材：一台装PC机。

、实验目的

熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。

、实验要求对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程:

(1)谓词公式到子句集变换；

(2)替换与合一算法；

(3)在某简单归结策略下的归结三、实验步骤

步1设计谓词公式及自居的存储结构，即内部表示。注意对全称量词x和存在量词x可采用其他符号代替；

步2实现谓词公式到子句集变换过程；

步3实现替换与合一算法；

步4实现某简单归结策略；

步5设计输出，动态演示归结过程，可以以归结树的形式给出；

步6实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略

四、代码

谓词公式到子句集变换的源代码：

#in clude

#in clude

#in clude

using n amespace std;

〃一些函数的定义

void in itStri ng(stri ng &ni);// 初始化

string del_inlclue(string temp);// 消去蕴涵符号

string dec_neg_rand(string temp);// 减少否定符号的辖域

string standard_var(string temp);// 对变量标准化

string del_exists(string temp);// 消去存在量词

string convert_to_front(string temp);// 化为前束形

string convert_to_and(string temp);// 把母式化为合取范式

string del_all(string temp);// 消去全称量词

string del_and(string temp);// 消去连接符号合取%

stri ng cha nge_n ame(stri ng temp);// 更换变量名称

//辅助函数定义

bool isAlbum(char temp);// 是字母

string del_null_bracket(string temp);// 删除多余的括号

string del_blank(string temp);// 删除多余的空格

void checkLegal(string temp);// 检查合法性

char numAfectChar(int temp);// 数字显示为字符

//主函数

void mai n()

{

cout<<" ---------------- 求子句集九步法演示-----------------"<

system("color 0A");

//orign = "Q(x,y)%~(P(y)";

//orign = "(@x)(P(y)>P)";

//orign = "~(#x)y(x)";

//orign = "~((@x)x!b(x))";

//orign = "~(x!y)";

//orign = "~(~a(b))";

stri ng orig n,temp;

char comma nd,comma ndO,comma nd1,comma nd2,comma nd3,comma nd4,comma nd5, comma nd6,comma nd7,comma nd8,comma nd9,comma nd10;

//=================================================================

cout<<"请输入(Y/y)初始化谓词演算公式"<

cin> >comma nd;

if(comma nd == 'y' || comma nd == 'Y')

in itStri ng(orig n);

else

exit(0);

//=================================================================

cout<<"请输入(Y/y)消除空格"<

cin> >comma ndO;

if(comma ndO == 'y' || comma ndO == 'Y')

{

//del_bla nk(orig n);〃undone

cout<<"消除空格后是"<

<

}

else

exit(0);

//=================================================================

cout<<"请输入(Y/y)消去蕴涵项"<

cin> >comma nd1;

if(comma nd1 == 'y' || comma nd1 == 'Y')

{

orig n =del_i nl clue(orig n);

cout<<"消去蕴涵项后是"<

<

} else

exit(O);

//=================================================================

cout<<"请输入(Y/y)减少否定符号的辖域"<

cin> >comma nd2;

if(comma nd2 == 'y' || comma nd2 == 'Y')

{

do

{

temp = orig n;

orig n = dec_ neg_ra nd(orig n);

}while(temp != orig n);

cout<<"减少否定符号的辖域后是"<

<

}

else

exit(0);

//=================================================================

cout<<"请输入(Y/y)对变量进行标准化"<

cin> >comma nd3;

if(comma nd3 == 'y' || comma nd3 == 'Y')

{

orig n = sta ndard_var(orig n);

cout<<"对变量进行标准化后是"<

<

}

else

exit(0);

//================================================================= cin> >comma nd4;

cout<<"请输入(Y/y)消去存在量词"<

{

orig n = del_exists(orig n);

cout<<"消去存在量词后是(w = g(x)是一个Skolem函数)"<

<

}

else

exit(0);

//=================================================================

cout<<"请输入(Y/y)化为前束形"<

cin> >comma nd5;

if(comma nd5 == 'y' || comma nd5== 'Y')

{

orig n = con vert_to_fro nt(orig n);

cout<<"化为前束形后是"<

<

}

else

exit(0);

//=================================================================

cout<<"请输入(Y/y)把母式化为合取方式"<

cin> >comma nd6;

if(comma nd6 == 'y' || comma nd6 == 'Y')

{

orig n = con vert_to_a nd(orig n);

cout<<"把母式化为合取方式后是"<

<

}

else

exit(0);

//=================================================================

cout<<"请输入（Y/y）消去全称量词"<

cin> >comma nd7;

{

orig n= del_all(orig n);

cout<<"消去全称量词后是"<

<

}

else

exit(O);

//=================================================================

cout<<"请输入(Y/y)消去连接符号"<

cin> >comma nd8;

if(comma nd8 == 'y' || comma nd8 == 'Y')

{

orig n = del_a nd(orig n);

cout<<"消去连接符号后是"<

<

}

else

exit(0);

//=================================================================

cout<<"请输入(Y/y)变量分离标准化"<

cin> >comma nd9;

if(comma nd9 == 'y' || comma nd9 == 'Y')

{

orig n = cha nge_n ame(orig n);

cout<<"变量分离标准化后是(x1,x2,x3代替变量x)"<

<

}

else

exit(0);

//:

cout<<” ----------------------- 完毕------------------------- "<

cout<<"(请输入Y/y)结束"<

do

{

}while('y' == getchar() || 'Y'==getchar());

exit(O);

} void in itStri ng(stri ng &ini)

{

char comma nda,comma ndb;

cout<<"请输入您所需要转换的谓词公式"<

cout<<"需要查看输入帮助(Y/N)? "<

cin> >comma nda;

if(comma nda == 'Y' || comma nda == 'y')

cout<<"本例程规定输入时蕴涵符号为>，全称量词为@,存在量词为#,"<

cout<<"请输入(y/n)选择是否用户自定义"<

cin> >comma ndb;

if(comma ndb =='Y'|| comma ndb=='y')

ci n?ini;

else

ini = ”(@x)(P(x)>((@y)(P(y)>P(f(x, y)))%~(@y)(Q(x,y)>P(y))))”；

cout<<"原始命题是"<

<

}

string del_inlclue(string temp)// 消去〉蕴涵项

{

//a>b 变为~a!b

char ctemp[100]={""};

stri ng output;

int len gth = temp.le ngth();

int i = O,right_bracket = O,falg= 0;

stack stack1,stack2,stack3;

strcpy(ctemp,temp.c_str());

while(ctemp[i] != '\0' && i <= len gth-1)