《实现基于谓词逻辑的归结原理》由会员分享，可在线阅读，更多相关《实现基于谓词逻辑的归结原理（23页珍藏版）》请在金锄头文库上搜索。
1、河南城建学院河南城建学院 人工智能人工智能实验报告实验报告 实验名称：实现基于谓词逻辑的归结原理实验名称：实现基于谓词逻辑的归结原理 成成 绩：绩：_ 专业班级：专业班级： 学学 号：号： 姓姓 名：名： 实实 验验 日日 期期 ：2020 1414 年年 0505 月月 1313 日日 实验器材： 一台装 PC 机。 1、实验目的实验目的 熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过 程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节， 进一步了解机器自动定理证明的实现过程。 2、实验要求实验要求 对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程
2、： (1) 谓词公式到子句集变换； (2) 替换与合一算法； (3) 在某简单归结策略下的归结。 3、实验步骤实验步骤 步 1 设计谓词公式及自居的存储结构，即内部表示。注意对全称量词x 和存在量词x 可采用其他符号代替； 步 2 实现谓词公式到子句集变换过程； 步 3 实现替换与合一算法； 步 4 实现某简单归结策略； 步 5 设计输出，动态演示归结过程，可以以归结树的形式给出； 步 6 实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。 4、代码代码 谓词公式到子句集变换的源代码： #include #include #include #include using namesp
3、ace std; /一些函数的定义 void initString(string /初始化 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);/把母式化为合取范式
4、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)
5、;/数字显示为字符 /主函数 void main() coutP)“; /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; /= = coutcommand; if(command = y | command = Y) ini
6、tString(orign); else exit(0); /= = coutcommand0; if(command0 = y | command0 = Y) /del_blank(orign);/undone coutcommand1; if(command1 = y | command1 = Y) orign =del_inlclue(orign); coutcommand2; if(command2 = y | command2 = Y) do temp = orign; orign = dec_neg_rand(orign); while(temp != orign); coutco
7、mmand3; if(command3 = y | command3 = Y) orign = standard_var(orign); coutcommand4; if(command4 = y | command4 = Y) orign = del_exists(orign); coutcommand5; if(command5 = y | command5= Y) orign = convert_to_front(orign); coutcommand6; if(command6 = y | command6 = Y) orign = convert_to_and(orign); cou
8、tcommand7; if(command7 = y | command7 = Y) orign= del_all(orign); coutcommand8; if(command8 = y | command8 = Y) orign = del_and(orign); coutcommand9; if(command9 = y | command9 = Y) orign = change_name(orign); coutcommanda; if(commanda = Y | commanda = y) cout,全称量词为,存在量词为#,“commandb; if(commandb =Y|
9、 commandb=y) cinini; else ini = “(x)(P(x)(y)(P(y)P(f(x, y)%(y)(Q(x,y)P(y)“; cout蕴涵项 /ab 变为a!b char ctemp100=“; string output; int length = temp.length(); int i = 0,right_bracket = 0,falg= 0; stack stack1,stack2,stack3; strcpy(ctemp,temp.c_str(); while(ctempi != 0 if(isAlbum(ctempi)/如果是字母则把 ctempi弹出
10、stack1.pop(); stack1.push(); stack1.push(ctempi); stack1.push(!); i = i + 1; else if() = ctempi) right_bracket+; do if( = stack1.top() right_bracket-; stack3.push(stack1.top(); stack1.pop(); while(right_bracket != 0); stack3.push(stack1.top(); stack1.pop(); stack1.push(); while(!stack3.empty() stack
11、1.push(stack3.top(); stack3.pop(); stack1.push(!); i = i + 1; i+; while(!stack1.empty() stack2.push(stack1.top(); stack1.pop(); while(!stack2.empty() output += stack2.top(); stack2.pop(); if(falg = 1) return output; else return temp; string dec_neg_rand(string temp)/减少否定符号的辖域 char ctemp100,tempc; st
12、ring output; int flag2 = 0; int i = 0,left_bracket = 0,length = temp.length(); stack stack1,stack2; queue queue1; strcpy(ctemp,temp.c_str();/复制到字符数组中 while(ctempi != 0 queue1.push(); while(!queue1.empty() tempc = queue1.front(); queue1.pop(); stack1.push(tempc); i +; while(!stack1.empty() stack2.pus
13、h(stack1.top(); stack1.pop(); while(!stack2.empty() output += stack2.top(); stack2.pop(); if(flag2 = 1) temp = output; /*/ char ctemp1100; string output1; stack stack11,stack22; int falg1 = 0; int times = 0; int length1 = temp.length(),inleftbackets = 1,j = 0; strcpy(ctemp1,temp.c_str(); while(ctemp
14、1j != 0 if(ctemp1j = () inleftbackets +; else if(ctemp1j = ) inleftbackets -; if(inleftbackets = 1 stack11.push();/ stack11.push(%); stack11.push(); stack11.push();/ j = j+1; if(inleftbackets = 1 stack11.push();/ stack11.push(!); stack11.push(); stack11.push();/ j = j+1; j = j +1; if(falg1 = 1) stack11.push(); stack11.pop(); stack11.push();/此处有 bug stack11.push();/此处有 bug j +; while(!stack11.empty() stack22.push(stack11.top(); stack11.pop(); whil
