程序设计-逻辑式程序设计语言-常量指明论域上的对象

证明一个全称谓词是比较难的，因为最可靠的证明方法是枚举例证。于是采取反证的方法，全称量化的谓词取反取反量化谓词VXodd(X)3Xnot odd(X)m85EXodd(X)V Xnot odd(X)VX(X=2*Y+1-→odd(X))3Xnot(X+2*Y+1-→odd(X)Xnot(X=2*Y+1)or odd (X))X((X-2*Y+1)and not add(X))[6]3XvY not divide (X, 3, Y, O)VX3Y divide(X, 3, Y, O)XFY divide (X, 3, Y, O)VXVYnot divide(X, 3, Y, O) [7]VXY not divide (X, 3, Y, O) [8]XvYdivide(X, 3, Y, O)

证明一个全称谓词是比较难的，因为最可靠的证明方法是枚举例 证。 于是采取反证的方法，全称量化的谓词取反 量化谓词 取反 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]以^，V，→消除一→、<=>符号[2]化为前束范式,消除最外的一符号,否定符号内移-(FXP(X) VX(- p(X)[3]用斯柯林变换消去存在量词VX(a(X) ^ b(X) VEY c(X, Y))F VX(a(X) ^ b(X) V c (X, g(X))[4]消除前束范式的全称量词F a(X) ^ b(X) V c(X, g(X))

•谓词演算的等价变换 [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]用分配率PV(Q^R)=(PVQ)^(PVR)化成合取范式F (a(X)Vc(X, g(X)^(b(X) V c(X, g(X)经过以上变换.任何一复合公式均可成为如下形式F=C1^C2 ^...Cn且其中C称为子句若以：代V则有：Ci=L1 VL2 V...Lv = L1;L2....;Lv因此，任一公式均可化为V连接的子句的集合

[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)证明系统(proofsystem)是应用公理演绎出定理(theorems)的合法演绎规则的集合演绎也叫归约(deduction)，是对证明系统中合法推理规则的一次应用中间可利用以演绎从公理导出结论(conclusion)，这些规则演绎出的定理证明(proof)是个语句序列，以每个语句得到证明而结束，即每个句子要么演绎成公理，要么演绎成前此导出的定理

6.2 自动定理证明 • 证明系统 事实即证明系统中的公理(axioms) 证明系统(proof system)是应用公理演绎出定理 (theorems)的合法演绎规则的集合 演绎也叫归约(deduction)，是对证明系统中合法 推理规则的一次应用 演绎从公理导出结论(conclusion)， 中间可利用以 这些规则演绎出的定理 证明(proof)是个语句序列， 以每个语句得到证明而 结束， 即每个句子要么演绎成公理， 要么演绎成前 此导出的定理

一个证明若有N个语句（命题）则称N步证明反驳(refutation)是一个语句的反向证明。它证明一个语句是矛盾的，即不合乎给定的公理一个语句若能从公理出发推演出来，则称合法语句，任何合法语句也叫做定理(theorem)从某一公理集合导出的所有定理集合称为理论(theory)

一个证明若有N个语句(命题)则称N步证明 反驳(refutation)是一个语句的反向证明。 它证明 一个语句是矛盾的， 即不合乎给定的公理 一个语句若能从公理出发推演出来， 则称合法 语句， 任何合法语句也叫做定理(theorem) 从某一公理集合导出的所有定理集合称为理论 (theory)