人工智能 化为子句集的九步法实验.docx
《人工智能 化为子句集的九步法实验.docx》由会员分享，可在线阅读，更多相关《人工智能 化为子句集的九步法实验.docx（27页珍藏版）》请在冰点文库上搜索。
人工智能化为子句集的九步法实验
化为子句集的九步法实验报告
实验目的
1.熟悉谓词公式化为子句集的九个步骤
2.理解消解（谓词公式化为子句集）规则，能把任意谓词公式转换成子句集。
3.学会谓词公式化为子句集
实验原理
任一谓词公式通过九步法可以化成一个子句集。
九步法消解包括消去蕴含和等价符号、把否定符号移到紧靠谓词的位置上、变量标准化、消去存在量词、化为前束型、化为Skolem标准形、略去全称量词、消去合取词，把母式用子句集表示、子句换变量标准化，依次变换即可得到子句集。
实验条件
1.WindowNT/xp/7及以上的操作系统
2.内存在512M以上
3.CPU在奔腾II以上
实验内容
熟悉谓词公式转换成子句集的步骤，子句集转换演示程序参考界面如下图1所示。
图1子句集转换演示程序参考界面
实验分析
1.对默认谓词公式进行转换。
进入程序，点击“语法检查”，再依次点击消解过程的九个步骤按钮，得到转换结果。
2.自定义转换目标。
点击“清除”删除默认公式，利用界面键盘输入新的转换目标，用“大写字母”、“小写字母”按键进行输入中的字母变换。
3.语法检查。
点击“语法检查”检查输入谓词公式的语法错误。
如无错误，则依次点击步骤按钮进行转换。
4.重复运行2、3步，熟悉消解原理和转换过程。
程序代码
//化为子句集的九步法演示
//作者:
RanchoChan
//时间:
2010.12.15
//有bug
#include
#include
#include
#include
usingnamespacestd;
//一些函数的定义
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<<"------------------求子句集九步法演示-----------------------"<system（"color0A"）;
//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）初始化谓词演算公式"<cin>>command;
if（command=='y'||command=='Y'）
initString（orign）;
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）消除空格"<cin>>command0;
if（command0=='y'||command0=='Y'）
{
//del_blank（orign）;//undone
cout<<"消除空格后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）消去蕴涵项"<cin>>command1;
if（command1=='y'||command1=='Y'）
{
orign=del_inlclue（orign）;
cout<<"消去蕴涵项后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）减少否定符号的辖域"<cin>>command2;
if（command2=='y'||command2=='Y'）
{
do
{
temp=orign;
orign=dec_neg_rand（orign）;
}while（temp!
=orign）;
cout<<"减少否定符号的辖域后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）对变量进行标准化"<cin>>command3;
if（command3=='y'||command3=='Y'）
{
orign=standard_var（orign）;
cout<<"对变量进行标准化后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）消去存在量词"<cin>>command4;
if（command4=='y'||command4=='Y'）
{
orign=del_exists（orign）;
cout<<"消去存在量词后是（w=g（x）是一个Skolem函数）"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）化为前束形"<cin>>command5;
if（command5=='y'||command5=='Y'）
{
orign=convert_to_front（orign）;
cout<<"化为前束形后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）把母式化为合取方式"<cin>>command6;
if（command6=='y'||command6=='Y'）
{
orign=convert_to_and（orign）;
cout<<"把母式化为合取方式后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）消去全称量词"<cin>>command7;
if（command7=='y'||command7=='Y'）
{
orign=del_all（orign）;
cout<<"消去全称量词后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）消去连接符号"<cin>>command8;
if（command8=='y'||command8=='Y'）
{
orign=del_and（orign）;
cout<<"消去连接符号后是"<<}
else
exit（0）;
//=============================================================================
cout<<"请输入（Y/y）变量分离标准化"<cin>>command9;
if（command9=='y'||command9=='Y'）
{
orign=change_name（orign）;
cout<<"变量分离标准化后是（x1,x2,x3代替变量x）"<<}
else
exit（0）;
//============================================================================
cout<<"-------------------------完毕-----------------------------------"<cout<<"（请输入Y/y）结束"<do
{
}while（'y'==getchar（）||'Y'==getchar（））;
exit（0）;
}
voidinitString（string&ini）
{
charcommanda,commandb;
cout<<"请输入您所需要转换的谓词公式"<cout<<"需要查看输入帮助（Y/N）?
"<cin>>commanda;
if（commanda=='Y'||commanda=='y'）
cout<<"本例程规定输入时蕴涵符号为>,全称量词为@,存在量词为#,"<<<"取反为~,吸取为!
合取为%,左右括号分别为（、），函数名请用一个字母"<cout<<"请输入（y/n）选择是否用户自定义"<cin>>commandb;
if（commandb=='Y'||commandb=='y'）
cin>>ini;
else
ini="（@x）（P（x）>（（@y）（P（y）>P（f（x,y）））%~（@y）（Q（x,y）>P（y））））";
cout<<"原始命题是"<<}
stringdel_inlclue（stringtemp）//消去>蕴涵项
{
//a>b变为~a!
b
charctemp[100]={""};
stringoutput;
intlength=temp.length（）;
inti=0,right_bracket=0,falg=0;
stackstack1,stack2,stack3;
strcpy_s（ctemp,temp.c_str（））;
while（ctemp[i]!
='\0'&&i<=length-1）
{
stack1.push（ctemp[i]）;
if（'>'==ctemp[i+1]）//如果是a>b则用~a!
b替代
{
falg=1;
if（isAlbum（ctemp[i]））//如果是字母则把ctemp[i]弹出
{
stack1.pop（）;
stack1.push（'~'）;
stack1.push（ctemp[i]）;
stack1.push（'!
'）;
i=i+1;
}
elseif（'）'==ctemp[i]）
{
right_bracket++;
do
{
if（'（'==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（stack1.top（））;
stack1.pop（）;
}
while（!
stack2.empty（））
{
output+=stack2.top（）;
stack2.pop（）;
}
if（falg==1）
returnoutput;
else
returntemp;
}
stringdec_neg_rand（stringtemp）//减少否定符号的辖域
{
charctemp[100],tempc;
stringoutput;
intflag2=0;
inti=0,left_bracket=0,length=temp.length（）;
stackstack1,stack2;
queuequeue1;
strcpy_s（ctemp,temp.c_str（））;//复制到字符数组中
while（ctemp[i]!
='\0'&&i<=length-1）
{
stack1.push（ctemp[i]）;
if（ctemp[i]=='~'）//如果是~否则什么都不做
{
charfo=ctemp[i+2];
if（ctemp[i+1]=='（'）//如果是（，否则什么都不做
{
if（fo=='@'||fo=='#'）//如果是全称量词
{
flag2=1;
i++;
stack1.pop（）;
stack1.push（ctemp[i]）;
if（fo=='@'）
stack1.push（'#'）;
else
stack1.push（'@'）;
stack1.push（ctemp[i+2]）;
stack1.push（ctemp[i+3]）;
stack1.push（'（'）;
stack1.push（'~'）;
if（isAlbum（ctemp[i+4]））
{
stack1.push（ctemp[i+4]）;
i=i+5;
}
else
i=i+4;
do
{
queue1.push（temp[i]）;
if（temp[i]=='（'）
left_bracket++;
elseif（temp[i]=='）'）
left_bracket--;
i++;
}while（left_bracket!
=0&&left_bracket>=0）;
queue1.push（'）'）;
while（!
queue1.empty（））
{
tempc=queue1.front（）;
queue1.pop（）;
stack1.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;
/************************************************************/
charctemp1[100];
stringoutput1;
stackstack11,stack22;
intfalg1=0;
inttimes=0;
intlength1=temp.length（）,inleftbackets=1,j=0;
strcpy_s（ctemp1,temp.c_str（））;
while（ctemp1[j]!
='\0'&&j<=（length1-1））
{
stack11.push（ctemp1[j]）;
if（ctemp1[j]=='~'）
{
if（ctemp1[j+1]=='（'/*&&ctemp1[j+2]!
='~'*/）
{
j=j+2;
stack11.push（'（'）;////////////////
while（inleftbackets!
=0&&inleftbackets>=0&×<=（length1-j）&×>=0）
{
stack11.push（ctemp1[j]）;
if（ctemp1[j]=='（'）
inleftbackets++;
elseif（ctemp1[j]=='）'）
inleftbackets--;
if（inleftbackets==1&&ctemp1[j+1]=='!
'&&ctemp1[j+2]!
='@'&&ctemp1[j+2]!
='#'）
{
falg1=1;
stack11.push（'）'）;//////////
stack11.push（'%'）;
stack11.push（'~'）;
stack11.push（'（'）;//////////
j=j+1;
}
if（inleftbackets==1&&ctemp1[j+1]=='%'&&ctemp1[j+2]!
='@'&&ctemp1[j+2]!
='#'）
{
falg1=1;
stack11.push（'）'）;//////////
stack11.push（'!
'）;
stack11.push（'~'）;
stack11.push（'（'）;//////////
j=j+1;
}
j=j+1;
}
if（falg1==1）
stack11.push（'）'）;
stack11.pop（）;
stack11.push（'）'）;//此处有bug
stack11.push（'）'）;//此处有bug
}
}
j++;
}
while（!
stack11.empty（））
{
stack22.push（stack11.top（））;
stack11.pop（）;
}
while（!
stack22.empty（））
{
output1+=stack22.top（）;
stack22.pop（）;
}
if（falg1==1）
temp=output1;
/************************************************************/
charctemp
升级会员 