化为子句集的九步法 - 图文

化为子句集的九步法

一、实验目的：

熟悉谓词公式化为子句集的九个步骤，理解消解（谓词公式化为子句集）规则，能把任意谓词公式转换成子句集，掌握基于规则推理的基本方法。

二、实验原理

产生式系统用来描述若干个不同的以一个基本概念为基础的系统，这个基本概念就是产生式规则或产生式条件和操作对。在产生式系统中，论域的知识分为两部分：用事实表示静态知识；用产生式规则表示推理过程和行为。任一谓词公式通过九步法可以化成一个子句集。九步法消解包括消去蕴含和等价符号、把否定符号移到紧靠谓词的位置上、变量标准化、消去存在量词、化为前束型、化为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<<\消除空格后是\ <>command1; if(command1 == 'y' || command1 == 'Y') { orign =del_inlclue(orign); cout<<\消去蕴涵项后是\ <>command2; if(command2 == 'y' || command2 == 'Y') { do { temp = orign; orign = dec_neg_rand(orign); }while(temp != orign); cout<<\减少否定符号的辖域后是\ <>command3; if(command3 == 'y' || command3 == 'Y')

2

{ orign = standard_var(orign); cout<<\对变量进行标准化后是\ <>command4; if(command4 == 'y' || command4 == 'Y') { orign = del_exists(orign); cout<<\消去存在量词后是(w = g(x)是一个Skolem函数)\ <>command5; if(command5 == 'y' || command5== 'Y') { orign = convert_to_front(orign); cout<<\化为前束形后是\ <>command6; if(command6 == 'y' || command6 == 'Y') { orign = convert_to_and(orign); cout<<\把母式化为合取方式后是\ <

3

============ cout<<\请输入(Y/y)消去全称量词\ cin>>command7; if(command7 == 'y' || command7 == 'Y') { orign= del_all(orign); cout<<\消去全称量词后是\ <>command8; if(command8 == 'y' || command8 == 'Y') { orign = del_and(orign); cout<<\消去连接符号后是\ <>command9; if(command9 == 'y' || command9 == 'Y') { orign = change_name(orign); cout<<\变量分离标准化后是(x1,x2,x3代替变量x)\ <

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

}

t = '3'; break; case 4: t = '4'; break; default: t = '89'; break; }

return t;

四、实验步骤：

6

1 对默认谓词公式进行转换。进入程序，点击“语法检查”，再依次点击消解过程的九个步骤按钮，得到转换结果。

2 自定义转换目标。点击“清除”删除默认公式，利用界面键盘输入新的转换目标，用“大写字母”、“小写字母”按键进行输入中的字母变换。 3 语法检查。点击“语法检查”检查输入谓词公式的语法错误。如无错误，则依次点击步骤按钮进行转换。

4 重复运行2、3步，熟悉消解原理和转换过程。 五、实验报告要求：

1 了解每一步消解的规则和原则。

2 给出一个谓词公式转换为子句的详细过程和结果。 3 分析消解原理的特点和原理。 六、心得体会：

在本次课程设计过程中，我学到了好多东西。在此特别感谢老师教诲。老师不仅上课生动、幽默，平时上机时又悉心的指导。同时感谢学校给我们提供了非常优越的设计环境，对于我顺利完成这次课程设计起到了关键性的作用。通过对本次实验的操作，我较全面的掌握了化为子句集的九步法，并在实验操作中进一步的提高我的能力，但是自己还有一些不足之处有待提高。

7

本文来源：https://www.bwwdw.com/article/c22o.html