化为子句集九步法.doc

化为子句集的九步法
一、实验目的:
熟悉谓词公式化为子句集的九个步骤，理解消解(谓词公式化为子句集)规则，能把任意谓词公式转换成子句集，掌握基于规则推理的基本方法。
二、实验原理
产生式系统用来描述若干个不同的以一个基本概念为基础的系统，这个基本概念就是产生式规则或产生式条件和操作对。在产生式系统中，论域的知识分为两部分:用事实表示静态知识;用产生式规则表示推理过程和行为。任一谓词公式通过九步法可以化成一个子句集。九步法消解包括消去蕴含和等价符号、把否定符号移到紧靠谓词的位置上、变量标准化、消去存在量词、化为前束型、化为Skolem标准形、略去全称量词、消去合取词，把母式用子句集表示、子句换变量标准化，依次变换即可得到子句集。
三、实验内容代码:
void main()
{
cout<<"------------------求子句集九步法演示-----------------------"<<endl;
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))";
string orign,temp;
char command,command0,command1,command2,command3,command4,command5,
command6,command7,command8,command9,command10;
//=================================================================
============
cout<<"请输入(Y/y)初始化谓词演算公式"<<endl;
cin>>command;
if(command == 'y' || command == 'Y')
initString(orign);
else
exit(0);
//=================================================================
1
============
cout<<"请输入(Y/y)消除空格"<<endl;
cin>>command0;
if(command0 == 'y' || command0 == 'Y')
{
//del_blank(orign);//undone
cout<<"消除空格后是"<<endl
<<orign<<endl;
}
else
exit(0);
//=================================================================
============
cout<<"请输入(Y/y)消去蕴涵项"<<endl;
cin>>command1;
if(command1 == 'y' || command1 == 'Y')
{
orign =del_inlclue(orign);
cout<<"消去蕴涵项后是"<<endl
<<orign<<endl;
}
else
exit(0);
//=================================================================
============
cout<<"请输入(Y/y)减少否定符号的辖域"<<endl;
cin>>command2;
if(command2 == 'y' || command2 == 'Y')
{
do
{
temp = orign;
orign = dec_neg_rand(orign);
}while(temp != orign);
cout<<"减少否定符号的辖域后是"<<endl
<<orign<<endl;
}
else
exit(0);
//=================================================================
============
cout<<"请输入(Y/y)对变量进行标准化"<<endl;
cin>>command3;
if(command3 == 'y' || command3 =