化为子句集的九步法

化为子句集的九步法

一、实验目的：

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

二、实验原理

产生式系统用来描述若干个不同的以一个基本概念为基础的系统，这个基本概念就是产生式规则或产生式条件和操作对。在产生式系统中，论域的知识分为两部分：用事实表示静态知识；用产生式规则表示推理过程和行为。任一谓词公式通过九步法可以化成一个子句集。九步法消解包括消去蕴含和等价符号、把否定符号移到紧靠谓词的位置上、变量标准化、消去存在量词、化为前束型、化为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