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

实验三化为子句集的九步法实验一、实验目的理解和掌握消解原理，熟悉谓词公式化为子句集的九个步骤，理解消解推理规则，能把任意谓词公式转换成子句集。二、实验原理消解是可用于一定的子句公式的重要推理规则，任一谓词演算公式可以化成一个子句集。通过九步法消解可以从这两个父辈子句推导出一个新子句。九步法消解包括消去蕴涵符号、减否定符辖域、对变量标准化、消去存在量词、化为前束型、化为合取范式、消去全程量词、消去合取符、更换变量名，依次变换即可得到子句集。具体为：（1）消去连接词“→”和“↔”P→Q⇔﹁P∨QP↔Q⇔(P∧Q)∨(﹁P∧﹁Q)（2）将否定符号“﹁”移到仅靠谓词的位置﹁(﹁P)⇔P﹁(P∧Q)⇔﹁P∨﹁Q﹁(P∨Q)⇔﹁P∧﹁Q﹁(∀x)P(x)⇔(∃x)﹁P(x)﹁(∃x)P(x)⇔(∀x)﹁P(x)(∀x)(﹁(∀y)P(x,y)∨﹁(∀y)(﹁Q(x,y)∨R(x,y)))⇔(∀x)((∃y)﹁P(x,y)∨(∃y)(Q(x,y)∧﹁R(x,y)))（3）对变元标准化(∀x)((∃y)﹁P(x,y)∨(∃z)(Q(x,z)∧﹁R(x,z)))（4）化为前束范式(∀x)(∃y)(∃z)(﹁P(x,y)∨(Q(x,z)∧﹁R(x,z)))（5）消去存在量词(∀x)(﹁P(x,f(x))∨(Q(x,g(x))∧﹁R(x,g(x))))（6）化为Skolem标准形P∨(Q∧R)⇔(P∨Q)∧(P∨R)(∀x)((﹁P(x,f(x))∨Q(x,g(x))∧(﹁P(x,f(x))∨﹁R(x,g(x))))（7）消去全称量词(∀x)((﹁P(x,f(x))∨Q(x,g(x))∧(﹁P(x,f(x))∨﹁R(x,g(x))))（8）消去合取词﹁P(x,f(x))∨Q(x,g(x))﹁P(x,f(x))∨﹁R(x,g(x))（9）更换变量名称﹁P(x,f(x))∨Q(x,g(x))﹁P(y,f(y))∨﹁R(y,g(y))三、实验内容（1）可以采用自己熟悉的C#、C++、JAVA等任一种语言编写出Windows应用程序，演示子句消解推理演示程序。（2）界面中可以通过实例按钮，由程序指定具体的实例，给出原始谓词公式；（3）设计九个步骤的按钮，每按一步按钮，给出这一步消解的结果；（4）该程序主要帮助初学者学习、掌握九步法谓词公式化为子句集的过程。四、实验要求（1）提交实验报告，以word文档形式“学号+姓名”命名；（2）报告中要有程序源代码；（3）有程序运行结果截图；（4）报告提交到：任建平/人工智能五．实验截图六．源代码#includeiostream#includesstream#includestack#includequeue#includestringusingnamespacestd;//一些函数的定义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;//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));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);//=============================================================================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'){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本例程规定输入