人工智能(-化为子句集的九步法实验)

人工智能1化为子句集的九步法实验报告实验目的1.熟悉谓词公式化为子句集的九个步骤2.理解消解（谓词公式化为子句集）规则，能把任意谓词公式转换成子句集。3.学会谓词公式化为子句集实验原理任一谓词公式通过九步法可以化成一个子句集。九步法消解包括消去蕴含和等价符号、把否定符号移到紧靠谓词的位置上、变量标准化、消去存在量词、化为前束型、化为Skolem标准形、略去全称量词、消去合取词，把母式用子句集表示、子句换变量标准化，依次变换即可得到子句集。实验条件1.WindowNT/xp/7及以上的操作系统2.内存在512M以上3.CPU在奔腾II以上实验内容熟悉谓词公式转换成子句集的步骤，子句集转换演示程序参考界面如下图1所示。人工智能2图1子句集转换演示程序参考界面实验分析1.对默认谓词公式进行转换。进入程序，点击“语法检查”，再依次点击消解过程的九个步骤按钮，得到转换结果。2.自定义转换目标。点击“清除”删除默认公式，利用界面键盘输入新的转换目标，用“大写字母”、“小写字母”按键进行输入中的字母变换。3.语法检查。点击“语法检查”检查输入谓词公式的语法错误。如无错误，则依次点击步骤按钮进行转换。4.重复运行2、3步，熟悉消解原理和转换过程。程序代码//化为子句集的九步法演示//作者:RanchoChan//时间:2010.12.15//有bug#includeiostream#includesstream#includestack#includequeueusingnamespacestd;//一些函数的定义voidinitString(string&ini);//初始化stringdel_inlclue(stringtemp);//消去蕴涵符号stringdec_neg_rand(stringtemp);//减少否定符号的辖域stringstandard_var(stringtemp);//对变量标准化stringdel_exists(stringtemp);//消去存在量词stringconvert_to_front(stringtemp);//化为前束形stringconvert_to_and(stringtemp);//把母式化为合取范式stringdel_all(stringtemp);//消去全称量词stringdel_and(stringtemp);//消去连接符号合取%stringchange_name(stringtemp);//更换变量名称//辅助函数定义boolisAlbum(chartemp);//是字母stringdel_null_bracket(stringtemp);//删除多余的括号stringdel_blank(stringtemp);//删除多余的空格voidcheckLegal(stringtemp);//检查合法性charnumAfectChar(inttemp);//数字显示为字符//主函数voidmain(){cout------------------求子句集九步法演示-----------------------endl;system(color0A);//orign=Q(x,y)%~(P(y);//orign=(@x)(P(y)P);//orign=~(#x)y(x);//orign=~((@x)x!b(x));人工智能3//orign=~(x!y);//orign=~(~a(b));stringorign,temp;charcommand,command0,command1,command2,command3,command4,command5,command6,command7,command8,command9,command10;//=============================================================================cout请输入(Y/y)初始化谓词演算公式endl;cincommand;if(command=='y'||command=='Y')initString(orign);elseexit(0);//=============================================================================cout请输入(Y/y)消除空格endl;cincommand0;if(command0=='y'||command0=='Y'){//del_blank(orign);//undonecout消除空格后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去蕴涵项endl;cincommand1;if(command1=='y'||command1=='Y'){orign=del_inlclue(orign);cout消去蕴涵项后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)减少否定符号的辖域endl;cincommand2;if(command2=='y'||command2=='Y'){do{temp=orign;orign=dec_neg_rand(orign);}while(temp!=orign);cout减少否定符号的辖域后是endlorignendl;}elseexit(0);人工智能4//=============================================================================cout请输入(Y/y)对变量进行标准化endl;cincommand3;if(command3=='y'||command3=='Y'){orign=standard_var(orign);cout对变量进行标准化后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去存在量词endl;cincommand4;if(command4=='y'||command4=='Y'){orign=del_exists(orign);cout消去存在量词后是(w=g(x)是一个Skolem函数)endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)化为前束形endl;cincommand5;if(command5=='y'||command5=='Y'){orign=convert_to_front(orign);cout化为前束形后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)把母式化为合取方式endl;cincommand6;if(command6=='y'||command6=='Y'){orign=convert_to_and(orign);cout把母式化为合取方式后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去全称量词endl;cincommand7;if(command7=='y'||command7=='Y')人工智能5{orign=del_all(orign);cout消去全称量词后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)消去连接符号endl;cincommand8;if(command8=='y'||command8=='Y'){orign=del_and(orign);cout消去连接符号后是endlorignendl;}elseexit(0);//=============================================================================cout请输入(Y/y)变量分离标准化endl;cincommand9;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(string&ini){charcommanda,commandb;cout请输入您所需要转换的谓词公式endl;cout需要查看输入帮助(Y/N)?endl;cincommanda;if(commanda=='Y'||commanda=='y')cout本例程规定输入时蕴涵符号为,全称量词为@,存在量词为#,endl取反为~,吸取为!,合取为%,左右括号分别为(、)，函数名请用一个字母endl;cout请输入(y/n)选择是否用户自定义endl;人工智能6cincommandb;if(commandb=='Y'||commandb=='y')cinini;elseini=(@x)(P(x)((@y)(P(y)P(f(x,y)))%~(@y)(Q(x,y)P(y))));cout原始命题是endliniendl;}stringdel_inlclue(stringtemp)//消去蕴涵项{//ab变为~a!bcharctemp[100]={};stringoutput;intlength=temp.length();inti=0,right_bracket=0,falg=0;stackcharstack1,stack2,stack3;strcpy_s(ctemp,temp.c_str());while(ctemp[i]!='\0'&&i=length-1){stack1.push(ctemp[i]);if(