1、 第六章 逻辑式程序设计语言逻辑式语言基本形式：用一种 符号逻辑 作为程序设计语言来进行程序设计，通常称为逻辑程序设计语言，或声明性语言第 六章 逻辑式程序设计语言 程序要对数据结构实施某个算法过程 ,算法实现计算逻辑算法 = 逻辑 + 控制 逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系 对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述，根据规则找出合乎逻辑的事实就是推理 逻辑程序设计范型是陈述事实、制定规则，程序设计就是构造证明。程序的执行就在推理6.1谓词演算谓词演算是符号化事实的形式逻辑系统，它也是逻辑程序设计语言的模型 表示命题 表示命题
2、之间的关系 描述如何根据假设为真的命题推断出新命题 谓词演算诸元素 用形式方法研究论域上的对象需要一种语言，它能表达该域对象具有什么性质 (properties)， 以及对象间有些什么关系 (relations)描述以公式 (Formulas)表达。谓词公式中各元素按一定逻辑规则变换，即谓词演算 (predicate calculus)(1)公式 由一组约定的符号组成的序列，它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量 指明论域上的对象(3)变量 可束定到特定域上某个范围的对象上(4)函数 表征对象具有的映射关系(5)谓词 表征对象某种性质的符号(6)量词 量词限定的变量名作用域
3、是整个公式(7) 逻辑操作 and， or， not， ( 蕴含 ) (全等 )当谓词应用到的变元是常量或已被束定的变量上时，就叫做句子(sentence)或命题 (proposition)谓词变元的个数称作目 (arity)， 有单目、 N目谓词之称N-目谓词的例子。谓词 目 含义odd(X) 1 X是奇数father(F， S) 2 F是 S的父亲divide(N， D， Q， R) 4 N除 D得商 Q和余数 R谓词例化 结果值odd(2) Falsedivide (23， 7， 3， 2) Turefather (changshan， changping) Truedivide (23
4、， 7， 3， N) N未例化， 不知真假谓词的量化量化谓词 结果值Xodd(X) FalseXodd(X) TrueX(X=2*Y+1odd (X) TrueXYdivide (X， 3， Y， 0) True， 如 X =3， Y=1XYdivide (X， 3， Y， 0) FalseXYdivide(X， 3， Y， 0) False， 但很难证明证明一个全称谓词是比较难的，因为最可靠的证明方法是枚举例证。 于是采取反证的方法，全称量化的谓词取反量化谓词 取反Xodd(X) Xnot odd(X) 1Xodd(X) Xnot odd(X) 2X(X=2*Y+1odd(X) Xnot(X
5、+2*Y+1odd(X) 3Xnot(X=2*Y+1)or odd (X) 4X(X=2*Y+1)and not add(X) 5XY divide (X， 3， Y， 0) XY not divide (X， 3， Y， 0) 6XY divide (X， 3， Y， 0) XY not divide (X， 3， Y， 0) 7XY divide (X， 3， Y， 0) XY not divide (X， 3， Y， 0) 8谓词演算的等价变换1以 ， ， 消除 、 符号2化为前束范式 ,消除最外的 符号 ,否定符号内移(XP(X) X( p(X)3用斯柯林变换消去存在量词X(a ( X
6、) b(X) Y c (X， Y) X(a (X) b(X) c (X， g(X)4 消除前束范式的全称量词 a(X) b(X) c (X， g(X) 一般谓词公式变换为子句的实例。 号为 “可推出 ”5用分配率 P (Q R)=(P Q) (P R)化成合取范式 (a(X) c(X， g(X) (b(X) c(X， g(X) 经过以上变换 ,任何一复合公式均可成为如下形式 : F = C1 C2 Cn且其中 Ci称为子句若以 ;代 则有 : Ci = L1 L2 Lv = L1;L2;Lv因此，任一公式均可化为 连接的子句的集合6.2 自动定理证明 证明系统 事实即证明系统中的公理 (axioms)证明系统 (proof system)是应用公理演绎出定理 (theorems)的合法演绎规则的集合演绎也叫归约 (deduction)， 是对证明系统中合法推理规则的一次应用演绎从公理导出结论 (conclusion)， 中间可利用以这些规则演绎出的定理证明 (proof)是个语句序列， 以每个语句得到证明而结束， 即每个句子要么演绎成公理， 要么演绎成前此导出的定理
