计算机科学学院
刘芳
第5章 一阶逻辑等值演算与推理
5.1 一阶逻辑等值式 5.2 一阶逻辑前束范式
5.3 一阶逻辑的推理理论
2015-1-9 1
计算机科学学院
刘芳
5.1 一阶逻辑等值式
定义5.1
设A,B是一阶逻辑中的 任意两公式，若A B为永真
式，称A和B等值，记为AB，称AB 是等值式。
④ F(c) →G(c) ⑤ G(c)
⑥ xG(x)
⑤ +
26
2015-1-9
?能否将③④步与①②步互换。 注意：必须先消存在量词！
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
例5.10 （习题23-1）
前提：x (F(x)→G(x)) ， x(F(x) H(x)) 结论： x(G(x) H(x ) )
Group 2: 由基本等值式生成的推理定律
2015-1-9
17
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
Group 3:一阶逻辑的两个重言蕴含式
一 阶 逻 辑 等 值 式 和 前 束 范 式
（1） xA(x)∨ xB(x) x(A(x)∨B(x))
证明：
若xA(x)∨xB(x) 为1，即xA(x)为1，或xB(x) 为
则称A为前束范式。
例如:
xy(F(x)(G(y)H(x,y))) x(F(x)G(x)) x(F(x)y(G(y)H(x,y))) x(F(x)G(x))
2015-1-9
13
计算机科学学院
刘芳
5.2一阶逻辑前束范式
例5.6 (P71) ：求如下公式的前束范式：
5.量词的交换
xyA(x,y) yxA(x,y) xyA(x,y) y xA(x,y)
5
2015-1-9
计算机科学学院
刘芳
5.1 一阶逻辑等值式
例5.3：设个体域D={a,b,c}, 消去下面公式中的量词:
(1) x(F(x)G(x))
(F(a)G(a))(F(b)G(b))(F(c)G(c))
x(BA(x))BxA(x)
2015-1-9
4
计算机科学学院
刘芳
5.1 一阶逻辑等值式
4.量词分配等值式
设A(x) 和B(x)都是包含自由变元x的谓词公式，则：
x(A(x) ∧B(x)) xA(x) ∧ xB(x) x(A(x)∨ B(x)) xA(x)∨ xB(x)
换名规则
将公式A中某量词的指导变元及其在辖域内的所有 约束出现改成该量词辖域内未曾出现的某个个体 变项, 其余部分不变, 记所得公式为A, 则AA。
2015-1-9 9
计算机科学学院
刘芳
5.1 一阶逻辑等值式
例如：
xP(x) →Q(x) yP(y) →Q(x)
x (P(x,y) →Q(x,y) ) ∨P(x,z)
(2) x(F(x)yG(y))
xF(x)yG(y) 量词辖域收缩 (F(a)F(b)F(c))(G(a)G(b)G(c))
(3) xyF(x,y) x(F(x,a)F(x,b)F(x,c)) (F(a,a)F(a,b)F(a,c))(F(b,a)F(b,b)F(b,c)) (F(c,a)F(c,b)F(c,c))
1，故x(A(x)∨B(x)) 为1。
找反例说明二者不等值
D ：正整数集合 A(x) ：x是奇数
B(x) ：x是偶数
2015-1-9
18
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
一 阶 逻 辑 等 值 式 和 前 束 范 式
Group 3:一阶逻辑的两个重言蕴含式 （2） x(A(x)∧B(x)) xA(x)∧ xB(x) 证明： 若 x(A(x)∧B(x))为1，即至少有一个c∈D，使A(c) ∧
3
计算机科学学院
刘芳
5.1 一阶逻辑等值式
3.量词辖域收缩与扩张等值式 设A(x)是含x自由出现的公式，B中不含x的出现 关于全称量词的：
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(A(x)B) xA(x)B x(A(x)B)xA(x)B x(BA(x))BxA(x)
21
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
Group 4:量词的消去与引入规则
3.存在量词引入规则(Existential Generalization， +)
A( c ) xA( x )
c是论域中的某个个体。
2015-1-9
22
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
Group 4:量词的消去与引入规则 4.存在量词消去规则(Existential Identification， -)
xA( x ) A( c )
c是论域中的某个个体。
2015-1-9
23
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
一 阶 逻 辑 推 理 理 论
例: 证明苏格拉底论证是有效的。 证明：
设F(x):x是人， G(x):x是要死的， a：苏格拉底 则格拉底论证符号化为： 前提： x(F(x) →G(x))， F(a) 结论：G(a)
2015-1-9
16
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
一阶逻辑的推理定律
一 阶 逻 辑 推 理 理 论
Group 1: 命题逻辑推理定律的代换实例；
命题演算中的永真蕴涵式，以及由代入规则生成的永
真蕴涵式； （ P →Q）∧P Q （xP(x) → yE(y)） ∧ xP(x) yE(y)
t (P(t,y) →Q(t,y) ) ∨P(x,z)
2015-1-9
10
计算机科学学院
刘芳
5.1 一阶逻辑等值式
3.自由变元的代替规则
一 阶 逻 辑 公 式 及 解 释
将公式A中某个自由出现的个体变项的所有出现用A
中未曾使用过的个体变项符号代替，A中其余部分不 变，所得公式A’， 则AA。
刘芳
5.3 一阶逻辑的推理理论
例5.9：在自然推理系统N中，构造下面推理的证明：
前提： x(F(x) →G(x)) ， xF(x) 一 阶 逻 辑 推 理 理 论 结论： xG(x) 证明： ① xF(x) 前提引入 ① -
② F(c)
③ x(F(x) →G(x))
前提引入
③ ②④假言推理
基本等值式
Group 1.命题逻辑中基本等值式的代换实例


2015-1-9
P →Q ┐P ∨Q xP(x) → yE(y) ┐ xP(x) ∨ yE(y) x(P(x) → Q(x)) x (┐P (x) ∨ Q(x))
2
计算机科学学院
刘芳
5.1 一阶逻辑等值式
group2 1.消去量词等值式 • 对有限个体域D＝{a1,a2, …,an}中
xF(x) ∧ ┐xG(x) xF(x) ∨ ┐ xG(x)
定理5.1：(前束范式存在定理) 例5.7 (P73)
一阶逻辑中的任何公式都存在与之等值的前束范式。
2015-1-9
14
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
1.推理的形式结构
一 阶 逻 辑 的 推 理 理 论
形式1： A1A2…AkB 形式2： 前提： A1, A2, … , Ak
B(c)为1，也就是A(c) 为1， B(c)为1，故 xA(x)∧ xB(x)为1。
找反例说明二者不等值


D ：正整数集合
A(x)：x是奇数； B(x)：x是偶数
19
2015-1-9
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
Group 4:量词的消去与引入规则
1.全称量词消去规则(Universal Identification， - )
例5.11(习题21)
前提：┐x (F(x) H(x))， x( G(x)→H(x)) 结论： x(G(x) → ┐F(x ) )
2015-1-9
27
xA( x) A(c)
c是论域中的任意个体。
2Байду номын сангаас15-1-9
20
计算机科学学院
刘芳
5.3 一阶逻辑的推理理论
Group 4:量词的消去与引入规则
2.全称量词引入规则(Universal Generalization， + )
A(c) xA( x)
c是论域中的任意个体。
2015-1-9
7
计算机科学学院
刘芳
5.1 一阶逻辑等值式
置换规则、换名规则、代替规则
1.置换规则
若AB, 则(A) (B).
2015-1-9
8
计算机科学学院
刘芳
5.1 一阶逻辑等值式
2.换名规则
约束变元的换名依据
一个公式的约束变元可使用多个名称，具体符号 无关紧要，故可对约束变元进行换名。 例如：xP(x) yP(y)
xA(x) A(a1)∧A(a2)∧……∧A(an) xA(x) A(a1)∨A(a2)∨……∨A(an)
2.量词的否定等值式
（全称量词和存在量词之间的关系, A(x)是含x自由出现的公式）

2015-1-9
┐xA(x) x┐A(x) ┐ xA(x) x┐A(x)