河南城建学院
《人工智能》实验报告
实验名称：实现基于谓词逻辑的归结原理
成绩：____
专业班级：
学号：
姓名：
实验日期：20 14 年 05 月 13日
实验器材：一台装PC机。
一、实验目的
熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。
二、实验要求
对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程：
(1) 谓词公式到子句集变换；
(2) 替换与合一算法；
(3) 在某简单归结策略下的归结。
三、实验步骤
步1 设计谓词公式及自居的存储结构，即内部表示。注意对全称量词∀x和存在量词∃x可采用其他符号代替；
步2 实现谓词公式到子句集变换过程；
步3 实现替换与合一算法；
步4 实现某简单归结策略；
步5 设计输出，动态演示归结过程，可以以归结树的形式给出；
步6 实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。
四、代码
谓词公式到子句集变换的源代码：
#include
#include
#include
#include
using namespace std;
//一些函数的定义
void initString(string &ini);//初始化
string del_inlclue(string temp);//消去蕴涵符号
string dec_neg_rand(string temp);//减少否定符号的辖域
string standard_var(string temp);//对变量标准化
string del_exists(string temp);//消去存在量词
string convert_to_front(string temp);//化为前束形
string convert_to_and(string temp);//把母式化为合取范式
string del_all(string temp);//消去全称量词
string del_and(string temp);//消去连接符号合取%
string change_name(string temp);//更换变量名称
//辅助函数定义
bool isAlbum(char temp);//是字母
string del_null_bracket(string temp);//删除多余的括号
string del_blank(string temp);//删除多余的空格
void checkLegal(string temp);//检查合法性
char numAfectChar(int temp);//数字显示为字符
//主函数
void main()
{
cout<<"------------------求子句集九步法演示-----------------------"<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)初始化谓词演算公式"<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<<"消去蕴涵项后是"<<
