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

1、河南城建学院人工智能实验报告实验名称：实现基于谓词逻辑的归结原理成绩：专业班级：学号：姓名：实验日期：2014年05月13日实验器材：一台装PC机。一、实验目的熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。二、实验要求对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程：(1)谓词公式到子句集变换；(2)替换与合一算法；(3)在某简单归结策略下的归结。三、实验步骤步1设计谓词公式及自居的存储结构，即内部表示。注意对全称量词x和存在量词x可采用其他符号代替；步2实现谓

2、词公式到子句集变换过程；步3实现替换与合一算法；步4实现某简单归结策略；步5设计输出，动态演示归结过程，可以以归结树的形式给出；步6实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。.下载可编辑.四、代码谓词公式到子句集变换的源代码#include#include#include#includeusingnamespacestd;/一些函数的定义voidinitString(string&ini);/stringdel_inlclue(stringtemp);/stringdec_neg_rand(stringtemp);/stringstandard_var(stringtemp

3、);/stringdel_exists(stringtemp);/stringconvert_to_front(stringtemp);/stringconvert_to_and(stringtemp);/stringdel_all(stringtemp);/stringdel_and(stringtemp);/stringchange_name(stringtemp);/辅助函数定义初始化消去蕴涵符号减少否定符号的辖域对变量标准化消去存在量词化为前束形把母式化为合取范式消去全称量词消去连接符号合取更换变量名称boolisAlbum(chartemp);/是字母stringdel_null_b

4、racket(stringtemp);/删除多余的括号stringdel_blank(stringtemp);/voidcheckLegal(stringtemp);/charnumAfectChar(inttemp);/主函数voidmain()coutP)”;/orign=(#x)y(x)”;/orign=(x)x!b(x)”;/orign=(x!y)”;删除多余的空格检查合法性数字显示为字符求子句集九步法演示endl;一下载可编辑/orign=(a(b);stringorign,temp;charcommand,command0,command1,command2,command3,co

5、mmand4,command5,command6,command7,command8,command9,command10;=cout请输入(Y/y)初始化谓词演算公式command;if(command=y|command=Y)initString(orign);elseexit(0);=cout”请输入(Y/y)消除空格command0;if(command0=y|command0=Y)/del_blank(orign);/undonecout消除空格后是endlorignendl;elseexit(0);=cout请输入(Y/y)消去蕴涵项command1;if(command1=y|c

6、ommand1=Y)orign=del_inlclue(orign);cout消去蕴涵项后是endlorignendl;else一下载可编辑exit(0);:cout请输入(Y/y)减少否定符号的辖域command2;if(command2=y|command2=Y)dotemp=orign;orign=dec_neg_rand(orign);while(temp!=orign);cout减少否定符号的辖域后是endlorignendl;elseexit(0);=cout请输入(Y/y)对变量进彳T标准化command3;if(command3=y|command3=Y)orign=stand

7、ard_var(orign);cout对变量进行标准化后是endlorignendl;elseexit(0);=cout请输入(Y/y)消去存在量词command4;if(command4=y|command4=Y)一下载可编辑orign=del_exists(orign);cout消去存在量词后是(w=g(x)是一个Skolem函数)endlorignendl;elseexit(0);=cout请输入(Y/y)化为前束形command5;if(command5=y|command5=Y)orign=convert_to_front(orign);cout化为前束形后是endlorignend

8、l;elseexit(0);=cout请输入(Y/y)把母式化为合取方式command6;if(command6=y|command6=Y)orign=convert_to_and(orign);cout把母式化为合取方式后是endlorignendl;elseexit(0);=cout请输入(Y/y)消去全称量词command7;if(command7=y|command7=Y)一下载可编辑orign=del_all(orign);cout消去全称量词后是endlorignendl;)elseexit(0);=cout请输入(Y/y)消去连接符号command8;if(command8=y|

9、command8=Y)(orign=del_and(orign);cout消去连接符号后是endlorignendl;)elseexit(0);=cout请输入(Y/y)变量分离标准化command9;if(command9=y|command9=Y)(orign=change_name(orign);cout变量分离标准化后是(x1,x2,x3代替变量x)endlorignendl;)elseexit(0);/：一下载可编辑cout完毕endl;cout(请输入Y/y)结束endl;do(while(y=getchar()|Y=getchar();exit(0);voidinitString

10、(string&ini)(charcommanda,commandb;cout请输入您所需要转换的谓词公式endl;cout需要查看输入帮助(Y/N)?commanda;if(commanda=Y|commanda=y)cout,全称量词为,存在量词为#,endl取反为，吸取为！，合取为，左右括号分别为(、)，函数名请用一个字母endl;cout请输入(y/n)选择是否用户自定义commandb;if(commandb=Y|commandb=y)cinini;elseini=(x)(P(x)(y)(P(y)P(f(x,y)%(y)(Q(x,y)P(y);cout原始命题是endlini蕴涵项(

11、/ab变为a!bcharctemp100=;stringoutput;intlength=temp.length();inti=0,right_bracket=0,falg=0;.下载可编辑stackstack1,stack2,stack3;strcpy(ctemp,temp.c_str();while(ctempi!=0&i=ctempi+1)/如果是ab则用a!b替代falg=1;if(isAlbum(ctempi)/如果是字母则把ctempi弹出stack1.pop();stack1.push();stack1.push(ctempi);stack1.push(!);i=i+1;else

12、if()=ctempi)right_bracket+;doif(=stack1.top()right_bracket-;stack3.push(stack1.top();stack1.pop();while(right_bracket!=0);stack3.push(stack1.top();stack1.pop();stack1.push();while(!stack3.empty()stack1.push(stack3.top();stack3.pop();.下载可编辑stack1.push(!);i=i+1;)i+；)while(!stack1.empty()(stack2.push(s

13、tack1.top();stack1.pop();)while(!stack2.empty()(output+=stack2.top();stack2.pop();)if(falg=1)returnoutput;elsereturntemp;)stringdec_neg_rand(stringtemp)/减少否定符号的辖域(charctemp100,tempc;stringoutput;intflag2=0;inti=0,left_bracket=0,length=temp.length();stackstack1,stack2;queuequeue1;strcpy(ctemp,temp.c_

14、str();/复制到字符数组中while(ctempi!=0&i=0);queue1.push();while(!queue1.empty().下载可编辑tempc=queue1.front();queue1.pop();stackl.push(tempc);)i+；)while(!stack1.empty()(stack2.push(stack1.top();stack1.pop();)while(!stack2.empty()(output+=stack2.top();stack2.pop();)if(flag2=1)temp=output;/*/charctemp1100;stringo

15、utput1;stackstack11,stack22;intfalg1=0;inttimes=0;intlength1=temp.length(),inleftbackets=1,j=0;strcpy(ctemp1,temp.c_str();while(ctemp1j!=0&j=0×=0)(stack11.push(ctemp1j);if(ctemp1j=()inleftbackets+;elseif(ctemp1j=)inleftbackets-;if(inleftbackets=1&ctemp1j+1=!&ctemp1j+2!=&ctemp1j+2!=#)(falg1=1;st

16、ack11.push();/stack11.push(%);stack11.push();stack11.push();/j=j+1;if(inleftbackets=1&ctemp1j+1=%&ctemp1j+2!=&ctemp1j+2!=#)(falg1=1;stack11.push();/stack11.push(!);stack11.push();stack11.push();/j=j+1;j=j+1;.下载可编辑if(falg1=1)stackll.push();stack11.pop();stackll.push();/此处有bugstack11.push();/此处有bug)j+

17、;)while(!stack11.empty()stack22.push(stack11.top();stack11.pop();)while(!stack22.empty()output1+=stack22.top();stack22.pop();)if(falg1=1)temp=output1;/*/charctemp3100;stringoutput3;intk=0,left_bracket3=1,length3=temp.length();stackstack13,stack23;intflag=0,bflag=0;strcpy(ctemp3,temp.c_str();/复制到字符数组

18、中while(ctemp3k!=0&k=0)(stack13.push(ctemp3k+1);if(ctemp3k+1=()left_bracket3+;if(ctemp3k+1=)left_bracket3-;if(ctemp3k+1=!|ctemp3k+1=%)bflag=1;k+;stack13.pop();k+;while(!stack13.empty()(stack23.push(stack13.top();stack13.pop();while(!stack23.empty()(output3+=stack23.top();stack23.pop();if(flag=1&bflag

19、=0)temp=output3;returntemp;.下载可编辑对变量标准化，简化，不考虑多层嵌套)stringstandard_var(stringtemp)/(charctemp100,des10=;strcpy(ctemp,temp.c_str();stackstack1,stack2;intl_bracket=1,falg=0,bracket=1;inti=0,j=0;stringoutput;while(ctempi!=0&itemp.length()stack1.push(ctempi);if(ctempi=|ctempi=#)stack1.push(ctempi+1);desj=ctempi+1;j+;stack1.push(ctempi+2);i=i+3;stack1.push(ctempi);i+;if(ctempi-1=()while(ctempi!=0&l_bracket!=0)if(ctempi=()l_bracket+;if(ctempi=)l_bracket-;if(ctempi=(&ctempi+1=)desj=ctempi+2;j+;if(ctempi+1=(&ctempi+2=#).下载可编辑falg=1;intkk=1;stack1.push(ctempi);stack1.push();stack1.push(c