化为子句集的九步法
一、实验目的：
熟悉谓词公式化为子句集的九个步骤，理解消解（谓词公式化为子句集）规则，能把任意谓词公式转换成子句集，掌握基于规则推理的基本方法。
二、实验原理
产生式系统用来描述若干个不同的以一个基本概念为基础的系统，这个基本概念就是产生式规则或产生式条件和操作对。在产生式系统中，论域的知识分为两部分：用事实表示静态知识；用产生式规则表示推理过程和行为。任一谓词公式通过九步法可以化成一个子句集。九步法消解包括消去蕴含和等价符号、把否定符号移到紧靠谓词的位置上、变量标准化、消去存在量词、化为前束型、化为Skolem标准形、略去全称量词、消去合取词，把母式用子句集表示、子句换变量标准化，依次变换即可得到子句集。 三、实验内容代码：
void main() { cout<<\求子句集九步法演示-----------------------\ system(\ //orign = \ //orign = \ //orign = \ //orign = \ //orign = \ //orign = \ string orign,temp; char command,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); //=================================================================
1
============ cout<<\请输入(Y/y)消除空格\ cin>>command0; if(command0 == 'y' || command0 == 'Y') { //del_blank(orign);//undone cout<<\消除空格后是\ <
2
{ orign = standard_var(orign); cout<<\对变量进行标准化后是\ < 3 ============ cout<<\请输入(Y/y)消去全称量词\ cin>>command7; if(command7 == 'y' || command7 == 'Y') { orign= del_all(orign); cout<<\消去全称量词后是\ < 4 } string change_name(string temp)//更换变量名称 { char ctemp[100]; strcpy(ctemp,temp.c_str()); string output = \ int i = 0,j = 0,falg = 0; while(ctemp[i] != '\\0' && i < temp.length()) { falg++; while('\\n' != ctemp[i] && i < temp.length()) { if('x' == ctemp[i]) { output = output + ctemp[i] ; output = output + numAfectChar(falg); } else output = output + ctemp[i] ; i++; } output = output + ctemp[i] ; i ++; } return output; } bool isAlbum(char temp) { if(temp <= 'Z' && temp >= 'A' || temp <= 'z' && temp >= 'a') return true; return false; } char numAfectChar(int temp)//数字显示为字符 { char t; switch (temp) { case 1: t = '1'; break; case 2: t = '2'; break; case 3: 5