文档介绍：第12章逻辑式程序设计语言
程序要对数据结构实施某个算法过程,算法实现计算逻辑
算法= 逻辑+ 控制
逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系
对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述,根据规则找出合乎逻辑的事实就是推理
逻辑程序设计范型是陈述事实、制定规则,程序设计就是构造证明。程序的执行就在推理

谓词演算是符号化事实的形式逻辑系统,它也是逻辑程序设计语言的模型
谓词演算诸元素
用形式方法研究论域上的对象需要一种语言,它能表达该域对象具有什么性质(properties), 以及对象间有些什么关系(relations)
描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换,即谓词演算(predicate calculus)
(1)公式由一组约定的符号组成的序列,它包括常量、变量、逻辑连接、命题函数、谓词、量词
(2)常量指明论域上的对象
(3)变量可束定到特定域上某个范围的对象上
(4)函数表征对象具有的映射关系
(5)谓词表征对象某种性质的符号
(6)量词量词限定的变量名作用域是整个公式
(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) False
divide (23, 7, 3,2) Ture
father (changshan, changping) True
divide (23, 7, 3, N) N未例化, 不知真假
谓词的量化
量化谓词结果值
Xodd(X) False
Xodd(X) True
X(X=2*Y+1→odd (X)) True
XYdivide (X,3,Y,0) False
XYdivide (X,3,Y,0) True, 如X =3,Y=1
XYdivide(X,3,Y,0) False, 但很难证明
证明一个全称谓词是比较难的,因为最可靠的证明方法是枚举例证。于是采取反证的方法,全称量化的谓词取反
量化谓词取反
Xodd(X) Xnot odd(X) [1]
Xodd(X) Xnot odd(X) [2]
X(X=2*Y+1→odd(X)) Xnot(X+2*Y+1→odd(X)) [3]
Xnot(X=2*Y+1)or odd (X)) [4]
X((X=2*Y+1)and not add(X)) [5]
XY divide (X,3,Y,0) XY not divide (X,3,Y,0) [6]
XY divide (X,3,Y,0) XY not divide (X,3,Y,0) [7]
XY divide (X,3,Y,0) XY not divide (X,3,Y,0) [8]
谓词演算的等价变换
[1]以∧,∨, 消除→、<=>符号
[2]化为前束范式,消除最外的符号,否定符号内移(XP(X)┠X( p(X))
[3]用斯柯林变换消去存在量词
X(a ( X) ∧ 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
因此,任一公式均可化为'∨'连接的子句的集合
自动定理证明
证明系统
事实即证明系统中的公理(axioms)
证明系统(proof system)是应用公理演绎出定理
(theorems)的合法演绎规则的集合
演绎也叫归约(deduction),是对证明系统中合法
推理规则的一次应用
演绎从公理导出结论(conclusion), 中间可利用以
这些规则演绎出的定理
证明(proof)是个语句序列, 以每个