实现基于谓词逻辑的归结原理
河南城建学院
《人工智能》实验报告
实验名称：实现基于谓词逻辑的归结原理
成绩：____
专业班级：
学号：
姓名：
实验日期：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<<"消去蕴涵项后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)减少否定符号的辖域"< cin>>command2; if(command2 == 'y' || command2 == 'Y') { do { temp = orign; orign = dec_neg_rand(orign); }while(temp != orign); cout<<"减少否定符号的辖域后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)对变量进行标准化"< cin>>command3; if(command3 == 'y' || command3 == 'Y') { orign = standard_var(orign); cout<<"对变量进行标准化后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)消去存在量词"< cin>>command4; if(command4 == 'y' || command4 == 'Y') { orign = del_exists(orign); cout<<"消去存在量词后是(w = g(x)是一个Skolem函数)"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)化为前束形"< cin>>command5; if(command5 == 'y' || command5== 'Y') { orign = convert_to_front(orign); cout<<"化为前束形后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)把母式化为合取方式"< cin>>command6; if(command6 == 'y' || command6 == 'Y') { orign = convert_to_and(orign); cout<<"把母式化为合取方式后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)消去全称量词"< cin>>command7; if(command7 == 'y' || command7 == 'Y') { orign= del_all(orign); cout<<"消去全称量词后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)消去连接符号"< cin>>command8; if(command8 == 'y' || command8 == 'Y') { orign = del_and(orign); cout<<"消去连接符号后是"< < } else exit(0); //================================================================= ============ cout<<"请输入(Y/y)变量分离标准化"< cin>>command9; if(command9 == 'y' || command9 == 'Y') { orign = change_name(orign); cout<<"变量分离标准化后是(x1,x2,x3代替变量x)"< < } else exit(0); //================================================================= =========== cout<<"-------------------------完毕-----------------------------------"< cout<<"(请输入Y/y)结束"< do { }while('y' == getchar() || 'Y'==getchar()); exit(0); } void initString(string &ini) { char commanda,commandb; cout<<"请输入您所需要转换的谓词公式"< cout<<"需要查看输入帮助(Y/N)? "< cin>>commanda; if(commanda == 'Y' || commanda == 'y') cout<<"本例程规定输入时蕴涵符号为>,全称量词为@,存在量词为#,"< cout<<"请输入(y/n)选择是否用户自定义"< cin>>commandb; if(commandb =='Y'|| commandb=='y') cin>>ini; else ini = "(@x)(P(x)>((@y)(P(y)>P(f(x, y)))%~(@y)(Q(x,y)>P(y))))"; cout<<"原始命题是"< < } string del_inlclue(string temp)//消去>蕴涵项 { //a>b变为~a!b char ctemp[100]={""}; string output; int length = temp.length(); int i = 0,right_bracket = 0,falg= 0; stack strcpy(ctemp,temp.c_str()); while(ctemp[i] != '\0' && i <= length-1) { stack1.push(ctemp[i]); if('>' == ctemp[i+1])//如果是a>b则用~a!b替代 { falg = 1; if(isAlbum(ctemp[i]))//如果是字母则把ctemp[i]弹出 { stack1.pop(); stack1.push('~'); stack1.push(ctemp[i]); stack1.push('!'); i = i + 1; } else if(')' == ctemp[i]) { 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()) { stack1.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 ctemp[100],tempc; string output; int flag2 = 0; int i = 0,left_bracket = 0,length = temp.length(); stack queue strcpy(ctemp,temp.c_str());//复制到字符数组中 while(ctemp[i] != '\0' && i <= length - 1) { stack1.push(ctemp[i]); if(ctemp[i] == '~')//如果是~否则什么都不做 { char fo = ctemp[i+2]; if(ctemp[i+1] == '(')//如果是(，否则什么都不做 { if(fo == '@' || fo =='#')//如果是全称量词 { flag2 = 1; i++; stack1.pop(); stack1.push(ctemp[i]); if(fo == '@') stack1.push('#'); else stack1.push('@'); stack1.push(ctemp[i+2]); stack1.push(ctemp[i+3]); stack1.push('('); stack1.push('~'); if(isAlbum(ctemp[i+4])) { stack1.push(ctemp[i+4]); i = i + 5; } else i = i + 4; do { queue1.push(temp[i]); if(temp[i] == '(') left_bracket ++; else if(temp[i] == ')') left_bracket --; i ++; }while(left_bracket != 0 && left_bracket >=0); queue1.push(')'); while(!queue1.empty()) { tempc = queue1.front(); queue1.pop(); stack1.push(tempc); } } } } i ++; } while(!stack1.empty()) { stack2.push(stack1.top()); stack1.pop(); } while(!stack2.empty()) { output += stack2.top(); stack2.pop(); } if(flag2 == 1) temp = output; /************************************************************/ char ctemp1[100]; string output1; stack int falg1 = 0; int times = 0; int length1 = temp.length(),inleftbackets = 1,j = 0; strcpy(ctemp1,temp.c_str()); while(ctemp1[j] != '\0' && j <= (length1 -1)) { stack11.push(ctemp1[j]); if(ctemp1[j] == '~') { if(ctemp1[j+1] == '(' /*&& ctemp1[j + 2] != '~'*/) { j = j + 2; stack11.push('(');//////////////// while(inleftbackets != 0 && inleftbackets >=0 && times <= (length1 - j) && times >= 0) { stack11.push(ctemp1[j]); if(ctemp1[j] == '(') inleftbackets ++; else if(ctemp1[j] == ')') inleftbackets --; if(inleftbackets == 1 && ctemp1[j+1] == '!' && ctemp1[j+2] != '@' && ctemp1[j+2] != '#') { falg1 =1; stack11.push(')');////////// stack11.push('%'); stack11.push('~'); stack11.push('(');////////// j = j+1; } if(inleftbackets == 1 && ctemp1[j+1] == '%' && ctemp1[j+2] != '@' && ctemp1[j+2] != '#') { falg1 =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(); } while(!stack22.empty()) { output1 += stack22.top(); stack22.pop(); } if(falg1 == 1) temp = output1; /************************************************************/ char ctemp3[100]; string output3; int k = 0,left_bracket3 = 1,length3 = temp.length(); stack int flag = 0,bflag = 0; strcpy(ctemp3,temp.c_str());//复制到字符数组中 while(ctemp3[k] != '\0' && k <= length3-1) { stack13.push(ctemp3[k]); if(ctemp3[k] == '~') { if(ctemp3[k+1] == '(') { if(ctemp3[k + 2] == '~') { flag = 1; stack13.pop(); k =k + 2; while(left_bracket3 != 0 && left_bracket3 >=0) { stack13.push(ctemp3[k+1]); if(ctemp3[k+1] == '(') left_bracket3 ++; if(ctemp3[k+1] == ')') left_bracket3 --; if(ctemp3[k+1] == '!' || ctemp3[k+1] == '%') bflag = 1; k ++; } stack13.pop(); } } } k ++; } while(!stack13.empty()) { stack23.push(stack13.top()); stack13.pop(); } while(!stack23.empty()) { output3 += stack23.top(); stack23.pop(); } if(flag == 1 && bflag == 0) temp = output3; return temp; } string standard_var(string temp)//对变量标准化,简化,不考虑多层嵌套{ char ctemp[100],des[10]={" "}; strcpy(ctemp,temp.c_str()); stack int l_bracket = 1,falg = 0,bracket = 1; int i = 0,j = 0; string output; while(ctemp[i] != '\0' && i < temp.length()) { stack1.push(ctemp[i]); if(ctemp[i] == '@' || ctemp[i] == '#') { stack1.push(ctemp[i+1]); des[j] = ctemp[i+1]; j++; stack1.push(ctemp[i+2]); i = i + 3; stack1.push(ctemp[i]); i++; if(ctemp[i-1] == '(') { while(ctemp[i] != '\0' && l_bracket != 0) { if(ctemp[i] == '(') l_bracket ++; if(ctemp[i] == ')') l_bracket --; if(ctemp[i] == '(' && ctemp[i+1] == '@' ) { des[j] = ctemp[i+2]; j++; } if(ctemp[i+1] == '(' && ctemp[i+2] == '#' ) { falg = 1; int kk = 1; stack1.push(ctemp[i]); stack1.push('('); stack1.push(ctemp[i+2]); i = i+3; if(ctemp[i] == 'y') ctemp[i] ='w'; stack1.push(ctemp[i]); stack1.push(')'); stack1.push('('); i = i+3; while(kk != 0) { if(ctemp[i]=='(') kk++; if(ctemp[i] ==')') kk--; if(ctemp[i] == 'y') ctemp[i] ='w'; stack1.push(ctemp[i]); i++; } } stack1.push(ctemp[i]); i ++; } } } 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 del_exists(string temp)//消去存在量词{ char ctemp[100],unknow; strcpy(ctemp,temp.c_str()); int left_brackets = 0,i = 0,falg = 0; queue string output; while(ctemp[i] != '\0' && i < temp.length()) { if(ctemp[i] =='(' && ctemp[i+1] =='#') { falg = 1; unknow = ctemp[i+2]; i = i+4; do { if(ctemp[i] == '(') left_brackets ++; if(ctemp[i] == ')') left_brackets --; if(ctemp[i] == unknow) { queue1.push('g'); queue1.push('('); queue1.push('x'); queue1.push(')'); } if(ctemp[i] != unknow) queue1.push(ctemp[i]); i++; }while(left_brackets != 0); } queue1.push(ctemp[i]); i++; } while(!queue1.empty()) { output+= queue1.front(); queue1.pop(); } if(falg == 1) return output; else return temp; } string convert_to_front(string temp)//化为前束形{ char ctemp[100]; strcpy(ctemp,temp.c_str()); int i = 0; string out_var = "",output = ""; while(ctemp[i] != '\0' && i < temp.length()) { if(ctemp[i] == '(' && ctemp[i+1] == '@') { out_var = out_var + ctemp[i] ;//(@) out_var = out_var + ctemp[i+1] ; out_var = out_var +ctemp[i+2]; out_var = out_var +ctemp[i+3]; i = i + 4; } output = output + ctemp[i]; i++; } output = out_var + output; return output; } string convert_to_and(string temp)//把母式化为合取范式,Q/A? { temp = "(@x)(@y)((~P(x)!(~P(y))!P(f(x,y)))%((~P(x)!Q(x,g(x)))%((~P(x))!(~P(g(x)))))"; return temp; } string del_all(string temp)//消去全称量词 { char ctemp[100]; strcpy(ctemp,temp.c_str()); int i = 0,flag = 0; string output = ""; while(ctemp[i] != '\0' && i < temp.length()) { if(ctemp[i] == '(' && ctemp[i+1] == '@') { i = i + 4; flag = 1; } else { output = output + ctemp[i]; i ++; } } return output; } string del_and(string temp)//消去连接符号合取% { char ctemp[100]; strcpy(ctemp,temp.c_str()); int i = 0,flag = 0; string output = ""; while(ctemp[i] != '\0' && i < temp.length()) { if(ctemp[i] == '%' ) { ctemp[i] = '\n'; } output = output +ctemp[i]; i++; } return output; } 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]) { #include } } j=count; if(k==j)return; count=k; for(int i=1;i 有限单元法学习报告 在对力学问题分析求解过程中，方法可以概括为两种方法，一种为解析法，对具体问题具体分析，通过一定的推导用具体的表达式获得解答，由于实际工程中结构物的复杂性，此方法在处理工程问题是十分困难的；另一种是数值法，有限元法是其中一种方法，其数学逻辑严谨，物理概念清晰，又采用矩阵形式表达基本公式，便于计算机编程，因此在工程问题中获得广泛的应用。 有限元法基本原理是，将复杂的连续体划分为简单的单元体；将无限自由度问题化为有限自由度问题，因为单元体个数是有限的；将偏微分方程求解问题化为有限个代数方程组的求解问题。通常以位移为基本未知量，通过虚功原理和最小势能原理来求解。 基本思想是先化整为零，即离散化整体结构，把整体结构看作是由若干个通过结点相连的单元体组成的整体；再积零为整，通过结点的平衡来建立代数方程组，最后计算出结果。我将采用最简单的三结点三角形为基本单元体，解决弹性力学中的平面问题为例，解释有限单元法的基本原理、演示数值计算过程和一般性应用结论。 一、离散化 解决平面问题时，主要单元类型包括三角形单元（三结点、六结点）和四边形单元（四结点矩形、四结点四边形、八结点四边形）等。选用不同的单元会有不同的精度，划分的单元数越多，精度越高，但计算量也会越大。因此在边界曲折，应力集中处单元的尺寸要小些，但最大与最小单元的尺寸倍数不宜过大。在集中力作用点及分布力突变的点宜选为结点，不同厚度，不同材料不能划分在同一单元中。三角形单元以内角接近60°为最好。充分利用对称性与反对称性。 二、单元分析 将一个单元上的所有未知量用结点位移表示，并将分布在单元上的外力等效到结点上。 1、位移函数选取： 根据有限元法的基本思路，将连续体离散为有限的单元集合后，此时单元体满足连续性、均匀性、各向同性、完全线弹性假设。单元与单元之间通过结点连接并传递力，位移法（应用最广）以结点位移δi=(u i v i)T为基本未知量，以离散位移场代替连续位移场。单元体内的位移变化可以用位移函数（位移模式）来表示，因为有限元分析所得结果是近似结果，为了保证计算精度和收敛性，x位移函数应尽可能反应物体中的真实位移，即满足完备性和连续性的要求： 谓词演算的 推理理论 在谓词逻辑中，除了命题逻辑中的推理规则继续有效外，还有以下四条规则。设前提Г= {A 1,A 2,…,A k }. 1. 全称指定规则（全称量词消去规则）US ： 例1 取个体域为实数域，F(x, y): x>y, P(x)=(?y) F(x,y), 则(?x)P(x) ?P(z)=(?y) F(z,y). 而不能(?x) P(x) ?P(y)=(?y) F(y,y). 其中x,y 是个体变项符号，c 为任意的个体常量. 或 (?x ) P (x ) ∴ P (y ) (?x) P (x ) ∴ P (c ) 2 . 全称推广规则（全称量词引入规则） UG： P(x) ∴ (?x)P(x) 其中x是个体变项符号，且不在前提的任何公式中 自由出现. 3. 存在指定规则（存在量词消去规则） ES： (?x)P(x) ∴ P(c) 1)c是使P(x)为真的特定的个体常量，不是任意的. 2)c不在前提中或者先前推导公式中出现或自由出现， 换句话说，此c是在该推导之前从未使用过的. 4. 存在推广规则（存在量词引入规则) EG： P(c) ∴ ( x)P(x) 其中x是个体变项符号, c是个体常项符号. 谓词逻辑的推理理论由下列要素构成. 1. 等价公式 2. 蕴含式 3. 推理规则： (1) 前提引入规则 (2) 结论引入规则 (3) CP推理规则 (4)归谬论 (5) US规则 (6) UG规则 (7) ES规则 (8) EG规则 1)在推导的过程中，可以引用命题演算中的规则P、规则T、 规则CP . 2)为了在推导过程中消去量词，可以引用规则US和规则ES来 消去量词. 3)当所要求的结论可能被定量时，此时可引用规则UG和规则 EG将其量词加入. 4)证明时可采用如命题演算中的直接证明方法和间接证明方法. 5)在推导过程中，对消去量词的公式或公式中没含量词的子公 式，完全可以引用命题演算中的基本等价公式和基本蕴涵公式. 6)在推导过程中，对含有量词的公式可以引用谓词中的基本等 价公式和基本蕴涵公式. 有限元分析概念 有限元法：把求解区域看作由许多小的在节点处相互连接的单元（子域）所构成，其模型给出基本方程的分片（子域）近似解，由于单元（子域）可以被分割成各种形状和大小不同的尺寸，所以它能很好地适应复杂的几何形状、复杂的材料特性和复杂的边界条件 有限元模型：它是真实系统理想化的数学抽象。由一些简单形状的单元组成，单元之间通过节点连接，并承受一定载荷。 有限元分析：是利用数学近似的方法对真实物理系统（几何和载荷工况）进行模拟。并利用简单而又相互作用的元素，即单元，就可以用有限数量的未知量去逼近无限未知量的真实系统。 线弹性有限元是以理想弹性体为研究对象的，所考虑的变形建立在小变形假设的基础上。在这类问题中，材料的应力与应变呈线性关系，满足广义胡克定律；应力与应变也是线性关系，线弹性问题可归结为求解线性方程问题，所以只需要较少的计算时间。如果采用高效的代数方程组求解方法，也有助于降低有限元分析的时间。 线弹性有限元一般包括线弹性静力学分析与线弹性动力学分析两方面。 非线性问题与线弹性问题的区别： 1）非线性问题的方程是非线性的，一般需要迭代求解； 2）非线性问题不能采用叠加原理； 3）非线性问题不总有一致解，有时甚至没有解。 有限元求解非线性问题可分为以下三类： 1）材料非线性问题 材料的应力和应变是非线性的，但应力与应变却很微小，此时应变与位移呈线性关系，这类问题属于材料的非线性问题。由于从理论上还不能提供能普遍接受的本构关系，所以，一般材料的应力与应变之间的非线性关系要基于试验数据，有时非线性材料特性可用数学模型进行模拟，尽管这些模型总有他们的局限性。在工程实际中较为重要的材料非线性问题有：非线性弹性（包括分段线弹性）、弹塑性、粘塑性及蠕变等。 2）几何非线性问题 几何非线性问题是由于位移之间存在非线性关系引起的。 当物体的位移较大时，应变与位移的关系是非线性关系。研究这类问题一般都是假定材料的应力和应变呈线性关系。它包括大位移大应变及大位移小应变问题。如结构的弹性屈曲问题属于大位移小应变问题，橡胶部件形成过程为大应变问题。 3）非线性边界问题 在加工、密封、撞击等问题中，接触和摩擦的作用不可忽视，接触边界属于高度非线性边界。 平时遇到的一些接触问题，如齿轮传动、冲压成型、轧制成型、橡胶减振器、紧配合装配等，当一个结构与另一个结构或外部边界相接触时通常要考虑非线性边界条件。 实际的非线性可能同时出现上述两种或三种非线性问题。 2.5 谓词演算的推理理论 1．推理定律 谓词演算中也存在一些基本的等价与蕴含关系，参见表2-2。我们以此作为推理的基础，即推理定律。 表2-2 序号 等价或蕴含关系 含义 E27 E28 ┐?xA(x)??x┐A(x) ┐?xA(x)??x┐A(x) 量词否定等值式 E29 E30?x(A(x)∧B(x))??xA(x)∧?xB(x) ?x(A(x)∨B(x))??xA(x)∨?xB(x) 量词分配等值式（量词分配律） E31 E32 E33 E34 E35 E36 E37 E38 E39 E40 E41 E42 E43?x(A(x)∨B)??xA(x)∨B ?x(A(x)∧B)??xA(x)∧B ?x(A(x)∨B)??xA(x)∨B ?x(A(x)∧B)??xA(x)∧B ?x(B∨A(x))? B∨?xA(x) ?x(B∧A(x))? B∧?xA(x) ?x(B∨A(x))? B∨?xA(x) ?x(B∧A(x))? B∧?xA(x) ?x(A(x)→B(x))??xA(x)→?xB(x) ?x(A(x)→B)??xA(x)→B ?xA(x)→B??x(A(x)→B) A→?xB(x)??x(A→B(x)) A→?xB(x)??x(A→B(x)) 量词作用域的扩张与收缩 I21 I22?xA(x)∨?xB(x)??x(A(x)∨B(x)) ?x(A(x)∧B(x))??xA(x)∧?xB(x) I23 ?xA(x)→?xB(x)??x(A(x)→B(x)) 表2-2中的I、E序号是接着表1-5和1-8排列的，表明它们都是谓词逻辑的推理定律。E31~E34与E35~E38只是A和B的顺序不同。 2．量词的消除与产生规则 谓词推理可以看作是对命题推理的扩充。除了原来的P规则（前提引入）、T规则（命题等价和蕴含）及反证法、CP规则外，为什么还需引入新的推理规则呢？ 命题逻辑中只有一种命题，但谓词逻辑中有2种，即量词量化的命题和谓词填式命题。如果仅由表2-2的推理定律就可推证，并不需要引入新的规则，但这种情况十分罕见，也失去了谓词逻辑本身的意义。为此，要引入如下4个规则完成量词量化命题与谓词填式之间的转换，其中的A(x)表示任意的谓词。 (1) 全称指定（消去）规则US（Ubiquity Specification，或记为?-） 3命题逻辑形式系统（FSPC） 3.1 命题逻辑与命题演算 Leibniz提出逻辑推理变成符号演算不久，英国数学家BOOL提出了布尔代数。布尔代数把逻辑命题与逻辑推理归结为代数计算。把命题看作是计算对象；把联结词看作算子；讨论计算的性质。 1、命题（Propositions）：可以判断真假的陈述句。不涉及任何联结词的命题称为原 子命题。 2、联结词：?, →, ?, ∨, ∧为联结词，用于联结一个或者多个命题。 ~A=1-A →如果A成立则B成立，<->如果A成立则B成立，并且如果B成立则A成立； A→B A∨B，或者A成立或者B成立；A∧B，A成立并且B成立。 3、真值表：命题的真假称为命题的真值，用0表示假；用1表示真。 A←→B T(~A)=1-T(A) A=1, ~A=0, 1-A True(?A)＝1- True(A)，如果True(A)＝0，True(?A)=1：True(A)=1, True(?A) ＝0 T(A→B)=1 或者A不成立，或者B成立； A=1, B=1, A→B =1 A=0, B=1, A→B=1 A=0, B=0, A→B=1 A=1,B=0 A→B=0 或者A=0, 或者B＝1 ~AvB=A→B A<=B;;;; A<=B A=0,B=1 A=0时，B=?,1;A=1,B=1,1;A=1,B=0,0; A=0,B=0,T(A→B)=1;A=0,B=1,T(A→B)=1;A=1,B=0,T(A→B)=1;A=1,B=1,T(A→B) =1; A=0;T(A→B)=1 B=1;T(A→B)=1 A→B是或者A=0,或者B=1；=～AvB A<=B A∨B=MAX(A,B) A=1, B=0, 1;A=1,B=1, 1, A=0,B=1;1, A=0,B=0, 0 A∧B=MIN(A,B) =~(~A v ~B) DEMORGAN ~A ∨B True(A->B)：True（A）《＝True（B） 有限单元法 有限元方法的基础是变分原理和加权余量法，其基本求解思想是把计算域划分为有限个互不重叠的单元，在每个单元内，选择一些合适的节点作为求解函数的插值点，将微分方程中的变量改写成由各变量或其导数的节点值与所选用的插值函数组成的线性表达式，借助于变分原理或加权余量法，将微分方程离散求解。采用不同的权函数和插值函数形式，便构成不同的有限元方法。有限元方法最早应用于结构力学，后来随着计算机的发展慢慢用于流体力学的数值模拟。在有限元方法中，把计算域离散剖分为有限个互不重叠且相互连接的单元，在每个单元内选择基函数，用单元基函数的线形组合来逼近单元中的真解，整个计算域上总体的基函数可以看为由每个单元基函数组成的，则整个计算域内的解可以看作是由所有单元上的近似解构成。在河道数值模拟中，常见的有限元计算方法是由变分法和加权余量法发展而来的里兹法和伽辽金法、最小二乘法等。根据所采用的权函数和插值函数的不同，有限元方法也分为多种计算格式。从权函数的选择来说，有配置法、矩量法、最小二乘法和伽辽金法，从计算单元网格的形状来划分，有三角形网格、四边形网格和多边形网格，从插值函数的精度来划分，又分为线性插值函数和高次插值函数等。不同的组合同样构成不同的有限元计算格式。对于权函数，伽辽金(Galerkin)法是将权函数取为逼近函数中的基函数；最小二乘法是令权函数等于余量本身，而内积的极小值则为对代求系数的平方误差最小；在配置法中，先在计算域内选取N个配置点。令近似解在选定的N个配置点上严格满足微分方程，即在配置点上令方程余量为0。插值函数一般由不同次幂的多项式组成，但也有采用三角函数或指数函数组成的乘积表示，但最常用的多项式插值函数。有限元插值函数分为两大类，一类只要求插值多项式本身在插值点取已知值，称为拉格朗日(Lagrange)多项式插值；另一种不仅要求插值多项式本身，还要求它的导数值在插值点取已知值，称为哈密特(Hermite)多项式插值。单元坐标有笛卡尔直角坐标系和无因次自然坐标，有对称和不对称等。常采用的无因次坐标是一种局部坐标系，它的定义取决于单元的几何形状，一维看作长度比，二维看作面积比，三维看作体积比。在二维有限元中，三角形单元应用的最早，近来四边形等参元的应用也越来越广。对于二维三角形和四边形电源单元，常采用的插值函数为有Lagrange插值直角坐标系中的线性插值函数及二阶或更高阶插值函数、面积坐标系中的线性插值函数、二阶或更高阶插值函数等。 对于有限元方法，其基本思路和解题步骤可归纳为 (1)建立积分方程，根据变分原理或方程余量与权函数正交化原理，建立与微分方程初边值问题等价的积分表达式，这是有限元法的出发点。 (2)区域单元剖分，根据求解区域的形状及实际问题的物理特点，将区域剖分为若干相互连接、不重叠的单元。区域单元划分是采用有限元方法的前期准备工作，这部分工作量比较大，除了给计算单元和节点进行编号和确定相互之间的关系之外，还要表示节点的位置坐标，同时还需要列出自然边界和本质边界的节点序号和相应的边界值。 (3)确定单元基函数，根据单元中节点数目及对近似解精度的要求，选择满足一定插值条件的插值函数作为单元基函数。有限元方法中的基函数是在单元中选取的，由于各单元具有规则的几何形状，在选取基函数时可遵循一定的法则。 (4)单元分析：将各个单元中的求解函数用单元基函数的线性组合表达式进行逼近；再将近似函数代入积分方程，并对单元区域进行积分，可获得含有待定系数(即单元中各节点的参数值)的代数方程组，称为单元有限元方程。 (5)总体合成：在得出单元有限元方程之后，将区域中所有单元有限元方程按一定法则进行累加，形成总体有限元方程。 总复习 本章对高级数理逻辑所讲述的内容总结，并对已经学习的内容进行回顾。在对所讲述的内容回顾之前，首先对整个数理逻辑学科的组成进行回顾，从而使大家有更深刻的认识。 数理逻辑学科 学科发展 从数理逻辑学中衍生出来的学科有很多，如：递归论、可计算理论、模型论、机器证明、知识工程、布尔代数等。这些理论都是以数理逻辑学为基础的。针对数理逻辑本身，由于这些学科的需求产生了很多不同种类的逻辑系统。 数理逻辑的不同种类，基本上都是从经典的逻辑系统中扩展而来的。这种扩展通常有语法扩展和语义扩展。 ●语法扩展：在经典逻辑系统中，扩充一些符号，从而衍生出新的逻辑系统。如模态 逻辑，二阶谓词逻辑等。 ●语义扩展：对逻辑系统中语义的范围等进行扩展，如模糊逻辑等。 数理逻辑通常划分成以下不同种类的逻辑系统： 1、经典逻辑：传统的命题逻辑、一阶谓词逻辑等。认为世界是黑白的，对于一个命题 非真既假。 2、模态逻辑：认为世界上任何事情的真假是与时间有着密切的关系的。 3、多值逻辑：认为世界上的对与错是没有绝对的，命题的真假是可以是多个甚至连续 值的。 4、非单调逻辑：讨论如何将人类的常识加入到逻辑系统中去。经典逻辑是单调逻辑， 既事实越多，已有的结论不会消失；而单调逻辑中，可能随着事实的增加原有的结论被否定。 体系构成 在高级数理逻辑（计算逻辑）中，每一种逻辑都自成体系。逻辑的体系过程主要包括以下几个方面： 1、形式系统：用符号的方式来描述一个逻辑系统的构成。类似于形式语言系统。 2、语义系统：针对形式进行解释的一套体系，这套体系确定了符号的含义的解释方法 和规则。 3、元理论：对形式系统组成、语义系统特性和形式与语义之间关系进行研究。从而保 证了数理逻辑的初衷（利用数学演算的方法来研究人类思维过程）。 4、自动化推理：在形式系统的基础上，研究利用计算机自动进行推理的理论和方法。 以及自动推理的效率提高方法和自动推理完备性研究。 2.4 归结原理 本节在上节的基础上，进一步具体介绍谓词逻辑的归结方法。谓词逻辑的归结法是以命题逻辑的归结法为基础，在Skolem 标准性的子句集上，通过置换和合一进行归结的。 下面先介绍一些本节中用到的必要概念： 一阶逻辑：谓词中不再含有谓词的逻辑关系式。 个体词：表示主语的词 谓词：刻画个体性质或个体之间关系的词 量词：表示数量的词 个体常量：a,b,c 个体变量：x,y,z 谓词符号：P,Q,R 量词符号：, 归结原理正确性的根本在于，如果在子句集中找到矛盾可以肯定命题是不可满足的。 2.4.1 合一和置换 置换：置换可以简单的理解为是在一个谓词公式中用置换项去置换变量。 定义： 置换是形如{t1/x1, t2/x2, …, t n/x n}的有限集合。其中，x1, x2, …, x n是互不相同的变量，t1, t2, …, t n是不同于x i的项（常量、变量、函数）；t i/x i表示用t i置换x i，并且要求t i与x i不能相同，而且x i 不能循环地出现在另一个t i中。 例如 {a/x，c/y，f(b)/z}是一个置换。 {g(y)/x，f(x)/y}不是一个置换，原因是它在x和y之间出现了循环置换现象。置换的目的是要将某些变量用另外的变量、常量或函数取代，使其不在公式中出现。但在{g(y)/x，f(x)/y}中，它用g(y)置换x，用f(g(y))置换y，既没有消去x，也没有消去y。若改为{g(a)/x，f(x)/y}就可以了。 通常，置换用希腊字母θ、σ、α、λ来表示的。 定义：置换的合成 设θ＝{t1/x1, t2/x2, …, t n/x n}，λ＝{u1/y1, u2/y2, …, u n/y n}，是两个置换。则θ与λ的合成也是一个置换，记作θ·λ。它是从集合{t1·λ/x1, t2·l/x2, …, t n·λ/x n, u1/y1, u2/y2, …, u n/y n} 即对ti先做λ置换然后再做θ置换，置换xi 中删去以下两种元素： i. 当t iλ＝x i时，删去t iλ/x i(i = 1, 2, …, n); ii. 当y i∈{x1,x2, …, x n}时，删去u j/y j(j = 1, 2, …, m) 最后剩下的元素所构成的集合。 例： 设θ＝{f(y)/x, z/y}，λ＝{a/x, b/y, y/z}，求θ与λ的合成。 解： 先求出集合 1.1 有限单元法中“离散”的含义是什么？有限单元法是如何将具有无限自由度的连续介质问题转变成有限自由度问题的？位移有限元法的标准化程式是怎样的？ （1）离散的含义即将结构离散化，即用假想的线或面将连续体分割成数目有限的单元，并在其上设定有限个节点；用这些单元组成的单元集合体代替原来的连续体，而场函数的节点值将成为问题的基本未知量。 （2）给每个单元选择合适的位移函数或称位移模式来近似地表示单元内位移分布规律，即通过插值以单元节点位移表示单元内任意点的位移。因节点位移个数是有限的，故无限自由度问题被转变成了有限自由度问题。 （3）有限元法的标准化程式：结构或区域离散，单元分析，整体分析，数值求解。 1.3 单元刚度矩阵和整体刚度矩阵各有哪些性质？各自的物理意义是什么?两者有何区别?单元刚度矩阵的性质：对称性、奇异性（单元刚度矩阵的行列式为零）。整体刚度矩阵的性质：对称性、奇异性、稀疏性。单元 Kij 物理意义 Kij 即单元节点位移向量中第 j 个自由度发生单位位移而其他位移分量为零时，在第 j 个自由度方向引起的节点力。整体刚度矩阵 K 中每一列元素的物理意义是：要迫使结构的某节点位移自由度发生单位位移，而其他节点位移都保持为零的变形状态，在所有个节点上需要施加的节点荷载。 2.2 什么叫应变能？什么叫外力势能？试叙述势能变分原理和最小势能原理，并回答下述问题：势能变分原理代表什么控制方程和边界条件？其中附加了哪些条件？ (1)在外力作用下，物体内部将产生应力σ和应变ε，外力所做的功将以变形能的形式储存起来，这种能量称为应变能。 (2)外力势能就是外力功的负值。 (3)势能变分原理可叙述如下：在所有满足边界条件的协调位移中，那些满足静力平衡条件的位移使物体势能泛函取驻值，即势能的变分为零 δ∏p=δ Uε+δV=0 此即变分方程。对于线性弹性体，势能取最小值，即 δ2∏P=δ2Uε+δ2V≥0 此时的势能变分原理就是著名的最小势能原理。 势能变分原理代表平衡方程、本构方程和应力边界条件，其中附加了几何方程和位移边界条件。 2.3 什么是强形式？什么是弱形式？两者有何区别？建立弱形式的关键步骤是什么？ 等效积分形式通过分部积分，称式 ∫ΩCT(v)D(u)dΩ+∫ΓET(v)F(u)dΓ 为微分方程的弱形式，相对而言，定解问题的微分方程称为强形式。 区别：弱形式得不到解析解。建立弱形式的关键步骤：对场函数要求较低阶的连续性。2.4 为了使计算结果能够收敛于精确解，位移函数需要满足哪些条件？为什么？ 只要位移函数满足两个基本要求，即完备性和协调性，计算结果便收敛于精确解。 2.6 为什么采用变分法求解通常只能得到近似解？变分法的应用常遇到什么困难？Ritz 法收敛的条件是什么？ （1）在 Ritz 法中，N 决定了试探函数的基本形态，待定参数使得场函数具有一定的任意性。如果真实场函数包含在试探函数之内，则变分法得到的解答是精确的；如果试探函数取自完全的函数序列，则当项数不断增加时，近似解将趋近于精确解。然而，通常情况下试探函数不会将真实场函数完全包含在内，实际计算时也不可能取无穷多项。因此，试探函数只能是真实场函数的近似。可见，变分法就是在某个假定的范围内找出最佳解答，近似性就源于此。 （2）采用变分法近似求解，要求在整个求解区域内预先给出满足边界条件的场函数。通常情况下这是不可能的，因而变分法的应用受到了限制。 （3）Ritz 法的收敛条件是要求试探函数具有完备性和连续性，也就是说，如果试探函数满足完备性和连续性的要求，当试探函数的项数趋近于无穷时，则 Ritz 法的近似解将趋近于数学微分方程的精确解。 3.1 构造单元形函数有哪些基本原则？ 形函数是定义于单元内坐标的连续函数。单元位移函数通常采用多项式，其中的待定常数应该与单元节点自由度数相等。为满足完备性要求，位移函数中必须包括常函数和一次式，即完全一次多项式。多项式的选取应由低阶到高阶，尽量选择完全多项式以提高单元的精度。若由于项数限制而不能选取完全多项式时，也应使完全多项式具有坐标的对称性，并且一 河南城建学院 《人工智能》实验报告 实验名称：实现基于谓词逻辑的归结原理 成绩：____ 专业班级： 学号： 姓名： 实验日期：20 14 年 05 月 13日 实验器材：一台装PC机。 一、实验目的 熟练掌握使用归结原理进行定理证明的过程，掌握基于谓词逻辑的归结过程中，子句变换过程、替换与合一算法、归结过程及简单归结策略等重要环节，进一步了解机器自动定理证明的实现过程。 二、实验要求 对于任意给定的一阶谓词逻辑所描述的定理，要求实现如下过程： (1) 谓词公式到子句集变换； (2) 替换与合一算法； (3) 在某简单归结策略下的归结。 三、实验步骤 步1 设计谓词公式及自居的存储结构，即内部表示。注意对全称量词?x和存在量词?x可采用其他符号代替； 步2 实现谓词公式到子句集变换过程； 步3 实现替换与合一算法； 步4 实现某简单归结策略； 步5 设计输出，动态演示归结过程，可以以归结树的形式给出； 步6 实现谓词逻辑中的归结过程，其中要调用替换与合一算法和归结策略。 四、代码 谓词公式到子句集变换的源代码： #include 大学研究生学位课程论文论文题目：学习数理逻辑的意义 摘要：数理逻辑就是用数学方法研究思维形式的逻辑结构及其规律的科学。数理逻辑发展到今天，已经成熟为一门崭新的科学，具有强大的生命力和广泛的影响。学习数理逻辑可直接提高数理逻辑智能，如有利于学生思维能力的增强、思维效率的提高和创新能力的提升。数理逻辑在数学、计算机科学、语言研究、哲学等领域都已应用，数理逻辑学的任务在于探讨如何为整个数学建立严格的逻辑基础，其特点在于使用形式化的方法包括公理化的方法，因而比较抽象和艰深。本文介绍了数理逻辑的产生，数理逻辑主要贡献者的思想，数理逻辑的应用及学习数理逻辑学的意义。 关键词：数理逻辑；逻辑演算；应用 数理逻辑是一门新兴学科，至今有300年的历史。近百年来，它取得了长足发展。在现代的数学和计算机科学中以及在自然科学和社会科学的一些部门中都有广泛应用。在这样的背景下来研究数理逻辑的产生和发展，具有十分重要的意义。数理逻辑是用特制符号和数学方法来研究、处理演绎方法的逻辑学，包括各种逻辑演算（经典的和非经典的）和“四论”模型论、集合论、递归论和证明论。数理逻辑的定义:数理逻辑是用数学方法研究诸如推理的有效性、证明的真实性、数学的真理性和计算的可行性等这类问题中的逻辑问题的一门学问.当然，对此也可等价地这样说:数理逻辑是用数学方法研究各种推理中之逻辑问题的一门学问.其中主要包括推理的有效性、证明的真实性、数学的真理性、计算的能行性等这类问题中的逻辑问题.数理逻辑的研究对象:数理逻辑以推理本身作为自己的研究对象，其中主要包括演绎推理、形式推理、数学推理和各种近现代的非经典推理.数理逻辑的研究领域:作为数理逻辑之研究领域的历史性确认部分包括逻辑演算、集合论、模型论、递归论和证明论等五大块.但作为数理逻辑研究领域之近现代发展部分，还应包括诸如模态逻辑、多值逻辑、非单调逻辑、归纳逻辑、似然逻辑、不协调逻辑、信念修正、开放逻辑、中介逻辑和中介公理集合论等等各种各样的非经典逻辑分支.数理逻辑的学科归属:数理逻辑是逻辑和数学互相交织在一起的一门边缘性学科，或者说，数理逻辑既是一门逻辑化了的数学分科，又是一个数学化了的逻辑分支。 那么数理逻辑的的主要基础是什么？逻辑是研究推理的科学，分为形式逻辑和辨证逻辑。数理逻辑开始于用数学方法对形式逻辑中推理规律的研究，后来进一步发展到对数学中基础性问题及逻辑性问题的研究。现在数理逻辑是用数学方法研究形式逻辑的一门科学，也就是用数学方法研究推理的科学。所谓数学方法［1］，主要是指引进一套符号体系的方法，因此数理逻辑又叫符号逻辑。现代数理逻辑主要有四大分支：证明论、模型论、递归论和公 第一讲引言 一、课程内容 ·数理逻辑：是计算机科学的基础，应熟练掌握将现实生活中的条件化成逻辑公式，并能做适当的推理，这对程序设计等课程是极有用处的。 ·集合论：数学的基础，对于学习程序设计、数据结构、编译原理等几乎所有计算机专业课程和数学课程都很有用处。熟练掌握有关集合、函数、关系等基本概念。 ·代数结构：对于抽象数据类型、形式语义的研究很有用处。培养数学思维，将以前学过的知识系统化、形式化和抽象化。熟练掌握有关代数系统的基本概念，以及群、环、域等代数结构的基本知识。 ·图论：对于解决许多实际问题很有用处，对于学习数据结构、编译原理课程也很有帮助。要求掌握有关图、树的基本概念，以及如何将图论用于实际问题的解决，并培养其使用数学工具建立模型的思维方式。 ·讲课时间为两个学期，第一学期讲授数理逻辑与集合论，第二学期讲授代数结构和图论。考试内容限于书中的内容和难度，但讲课内容不限于书中的内容和难度。 二、数理逻辑发展史 1. 目的 ·了解有关的背景，加深对计算机学科的全面了解，特别是理论方面的了解，而不限于将计算机看成是一门技术或工程性的学科。 ·通过重要的历史事件，了解计算机科学中的一些基本思维方式和一些基本问题。 2. 数理逻辑的发展前期 ·前史时期——古典形式逻辑时期：亚里斯多德的直言三段论理论 ·初创时期——逻辑代数时期（17世纪末） ·资本主义生产力大发展，自然科学取得了长足的进步，数学在认识自然、发展技术方面起到了相当重要的作用。 ·人们希望使用数学的方法来研究思维，把思维过程转换为数学的计算。 ·莱布尼兹(Leibniz, 1646~1716)完善三段论，提出了建立数理逻辑或者说理性演算的思想：·提出将推理的正确性化归于计算，这种演算能使人们的推理不依赖于对推理过程中的命题的含义内容的思考，将推理的规则变为演算的规则。 ·使用一种符号语言来代替自然语言对演算进行描述，将符号的形式和其含义分开。使得演算从很大程度上取决与符号的组合规律，而与其含义无关。 ·布尔(G. Boole, 1815~1864)代数：将有关数学运算的研究的代数系统推广到逻辑领域，布尔代数既是一种代数系统，也是一种逻辑演算。 3. 数理逻辑的奠基时期 ·弗雷格(G. Frege, 1848~1925)：《概念语言——一种按算术的公式语言构成的纯思维公式语言》(1879)的出版标志着数理逻辑的基础部分——命题演算和谓词演算的正式建立。 ·皮亚诺(Giuseppe Peano, 1858~1932)：《用一种新的方法陈述的算术原理》(1889)提出了自然数算术的一个公理系统。 ·罗素(Bertrand Russell, 1872~1970)：《数学原理》(与怀特黑合著，1910, 1912, 1913)从命题演算和谓词演算开始，然后通过一元和二元命题函项定义了类和关系的概念，建立了抽象的类演算和关系演算。由此出发，在类型论的基础上用连续定义和证明的方式引出了数学（主要是算术）中的主要概念和定理。 ·逻辑演算的发展：甘岑(G. Gentzen)的自然推理系统(Natural Deduction System)，逻辑演算的元理论：公理的独立性、一致性、完全性等。 ·各种各样的非经典逻辑的发展：路易斯(Lewis, 1883~1964)的模态逻辑，实质蕴涵怪论和严格蕴涵、 谓词逻辑-归结原理例题 习题3.5, 1. (1) ()P x ：x 是大学生 ()Q x ：x 是诚实的 则命题可表示为： 已知：1:(()())G x P x Q x ?→， 2:()G Q a ? 证明：()P a ? 习题3.5, 1. (2) 将下面的命题符号化，并证明之：已知每一个运动员都是强壮的，而每一个既强壮又聪明的人在他所从事的事业中都能获得成功，彼得是运动员并且是聪明的，证明彼得在他的事业中将会成功。 提示：定义谓词 ()P x ：x 是运动员 ()Q x ：x 是强壮的 ()R x ：x 是聪明的 ()S x ：x 在他所从事的事业中获得成功。 则命题可表示为： 已知：1:(()())G x P x Q x ?→， 2:(()()())G x Q x R x S x ?∧→，()P a ，()R a 证明：()S a 提示：可用归结原理证明：（1）先把公式都化成Skolem 范式，（2）然后利用US ，ES 将公式中的量词除去，（3）化成合取范式，（4）化成蕴涵式，（5）化成子句集（结论用否定加入）， （6）进行归结，直至引出矛盾。 可化成如下子句集： {()()P x Q x →，()()()Q x R x S x ∧→，()P a →，()R a →，}()S a → 归结： （1）()()P x Q x → （2）()P a → （3）()Q a → 由（1）（2） （4）()()()Q x R x S x ∧→ （5）()()R a S a → 由（3）（4） （6）()R a → （7）()S a → 由（5）（6） （8）()S a → （9） 由（7）（8） 习题3.5, 1. (3) ()E x ：x 进入国境 ()V x ：x 是重要人物 ()C x ：x 是海关人员 ()P x ：x 是走私者 (,)S x y ：y 检查x 已知： 1:((()())(()(,)))G x E x V x y C y S x y ?∧?→?∧， 2:(()()((,)()))G x P x E x y S x y P y ?∧∧?→ 3:(()())G x P x V x ?→? 证明：(()())x P x C x ?∧ 先化成子句集： {} 1((()())(()(,))) ((()())(()(,))) ((()()())(()()(,))) ()()(()),()()(,())G x E x V x y C y S x y x y E x V x C y S x y x y E x V x C y E x V x S x y E x V x C f x E x V x S x f x =??∧?∨?∧=???∨∨∧=???∨∨∧?∨∨?→∨→∨ {}2(()()((,)()))(),(),(,)()G x y P x E x S x y P y P a E a S a y P y =??∧∧→?→→→ 注意G2，如果理解成(()()(,)())x y P x E x S x y P y ??∧∧→，则还需有条件(()())x P x E x ?∧，最后同样能得到如上的子句集{}(),(),(,)()P a E a S a y P y →→→。不 5.5 归结策略 归结算法：：： 用归结原理来证明定理，我们最终倒出空子句。怎么样最快的得到空子句是我们考虑的最主要问题。如果人用归结的方法，得到空子句通常是根据人们对子句集中子句的认识，可以最快的得到空子句。 然而，归结原理的主要思想是用机械的方法使计算机能够快速得到空子句。这需要我们考虑高效的计算算法来提高得到空子句的效率。本节主要目的是给出各种得到空子的算法，这些算法都从不同角度提高了得到空子句的归结效率。这些算法又称作为归结策略。 5.5.1 宽度优先 宽度优先是归结策略中最简单的算法。下图说明了，宽度优先策略的主要思想： S 将S 重所有能归结的子句间都归结 S 1 归结产生的子句集 S ∨S 1 将归结产生的子句集与原子句集析取 将S ∨S 1与S 1上能归结的子句间都归结 S 2 归结产生的子句集 ┆ 重复以上过程 □ 这样的归结过程中，有大量的冗余存在。因为，在每个归结步骤中，将有所能够归结的子句之间都归结，从而避免不了产生大量多余的归结步骤。 例如：对于子句集{P ?，Q P ∨，Q P ?∨，Q P ?∨?}，宽度优先归结策略将产生以下步骤完成： {Q,~Q,~P,P } （1） 对子句集中，能够归结的子句之间进行归结。归结产生的子句集为：{Q ?，Q ， Q Q ∨?，P P ∨?，Q Q ?∨?} （2） 将归结得到的子句集与原子句集合并得到{P ?， Q P ∨，Q P ?∨，Q P ?∨?，Q ?，Q ，Q Q ∨?，P P ∨?，Q Q ?∨?}，与{Q ?， Q ，Q Q ∨?，P P ∨? }子句进行归结。 （3） 在进行归结得到{□，…}. 这个归结过程中存在了Q Q ∨?，P P ∨?两个多余的归结步骤。 4.5 一阶谓词语义系统 4. 5.1 什么是形式系统语义 抽象公理系统或者形式系统，具有较高的抽象性。因此，已经脱离了任何一个具体的系统，但是我们可以对形式系统作出各种解释。通过这种解释将形式系统对应到各种具体的系统中取。例如可以将一阶谓词逻辑系统，解释到平面几何系统中。 怎样将形式系统解释成具体系统呢？我们先看下面的例子： 如果我们要知道)),1((x f xP ?的具体的真值=1，我们至少要知道以下事情： 1、 x 在什么范围之内，x 范围是实数。 2、 f 是什么？ (X+1) 3、 P 是什么？P 代表的是大于＝0 4、 a=？a=1 5、 x=?，x ＝5，－4 例如，我们可以作出以下解释： 1、解释1： ● x 在实数中取值 ● P 表示等于0 ● ),(a x f 表示x-a ● a=5 因此，公式解释为05==-x 。 令x=5, 则1))),(((=x a f P v s(x) ->5 s(f(a,x) ->I(f)(I(a),s(x)) 令x=6，则0))),(((=x a f P u 2、解释2： ● x 在实数中取值 ● P 表示大于等于0 ● ),(a x f 表示2)(a x - 因此，公式解释为0)(2 >=-a x 。这个公式不必对a 和x 作出具体解释，就可以确定公式的真值。即对于任何实数x ，和赋值映射v ，1)))(((2 =-a x P v 。 由上面的例子可以看出，要对形式系统作出解释，我们要了解以下问题： ?x取值于哪里？即规定讨论问题的领域。 ?给出谓词的含义和谓词的真值 ?给出函数的解释 ?给出变量和常量的值 ?根据连接词的赋值规则，赋值 这就是我们要研究的语义系统－指称语义的主要内容。 现代逻辑语义学理论的创始人是美籍波兰逻辑学家、哲学家A. Tarski，其奠基性文章是 他在1933年发表的《形式语言中的真实概念》。后来被称为模型论—标准语义学理论。进一步的发展由维特根斯坦最早提出设想，卡尔纳普最早把它展开为系统。这体现在他1947年发表的《意义和必然性》一书中；卡普兰·克里普克(S.kripke)和蒙太古作出了进一步的贡献，提出了非经典逻辑的语义学理论—模态逻辑语义学(克里普克结构)。 4.5.2形式语义基本概念 1、指称语义：语义是由语义结构和以及在这种结构下公式赋真值的规定构成的。 2、语义结构：对于抽象公理系统或形式系统作出的一种解释。包括个体域和在这种个 体域上的个体运算和个体间关系。 下面给出形式系统语义的定义： 3、形式语义：设FS是已经存在的形式系统，FS的语义有语义结构和赋值两个部分组 成： a)语义结构：当FS的项集TERM不为空时，由非空集合U和规则组I所组成二 元组（U，I），称为形式系统FS的语义结构。其中U和I的性质如下： i.U为非空集合，称为论域或者个体域； ii.规则组I，称为解释，根据规则组的规定对项集TERM中的成员指称到U 中的个体；规定对原子公式如何指称到U中的个体性质（U的子集）、关 U的子集）。 系（n b)指派：若形式系统FS中的变量集合Variables非空，那么下列映射称为指派： s：varibles－>U。 对于给定的语义结构，可以将指派扩展到项集TERM上： s：TERM－>U； s＝S(t) 当t 为变元 S指派t中变元由解释确定当t为非变元 F(x,a) = I(f) (x, I(a)) = s1( I(f) (x, I(a))) = I(f) (s(x), I(a)) P(f(a,x)) =I(P)(I(f)(a,s(x))) c)赋值：是指一组给公式赋值的规则，据此规则可对每一结构U和指派S确定一 由原子公式到值域的映射v：atomic－>value。根据这个赋值规则，可以将赋值 映射进行扩展：v为v：谓词逻辑归结原理源代码
有限单元法基本思想,原理,数值计算过程
离散数学24谓词演算的推理理论
有限元分析理论基础
谓词演算的推理理论(牛连强)
高级数理逻辑第2讲全解
有限单元法
高级数理逻辑第11讲全解
人工智能原理教案02章 归结推理方法2.4 归结原理
最新有限单元法部分课后题答案
实现基于谓词逻辑的归结原理
学习数理逻辑的意义-论文
数理逻辑的推理及形式证明
谓词逻辑_归结原理习题
高级数理逻辑第7讲
高级数理逻辑第5讲全解