IDEA激活码
文章目录
- 一、 前束范式
- 二、 前束范式转换方法
- 三、 前束范式示例
- 四、 谓词逻辑推理定律
一、 前束范式
公式
A
A
A 有如下形式 :
Q
1
x
1
Q
2
x
2
⋯
Q
k
x
k
B
Q_1 x_1 Q_2 x_2 \cdots Q_kx_k B
Q1x1Q2x2⋯QkxkB
则称
A
A
A 是 前束范式 ; 前束范式
A
A
A 的相关元素 说明 :
量词 :
Q
i
Q_i
Qi 是量词 , 全称量词
∀
\forall
∀ , 或 存在量词
∃
\exist
∃ ;
指导变元 :
x
i
x_i
xi 是 指导变元 ;
B
B
B 公式 :
B
B
B 是谓词逻辑公式 , 其中不含有量词 ,
B
B
B 中 可以含有 前面的
x
1
,
x
2
,
⋯
,
x
k
x_1 , x_2 , \cdots , x_k
x1,x2,⋯,xk 指导变元 , 也 可以不含有 其中的某些变元 ;
(
B
B
B 中一定不能含有量词 )
二、 前束范式转换方法
求一个谓词逻辑公式的前束范式 , 使用 基本等值式 , 或 换名规则 ;
基本等值式 : 参考博客 【数理逻辑】谓词逻辑 ( 谓词逻辑基本等值式 | 消除量词等值式 | 量词否定等值式 | 量词辖域收缩扩张等值式 | 量词分配等值式 )
换名规则 : 公式
A
A
A 中 , 某个量词辖域中 , 某个约束 出现的 个体变元 对应的 指导变元
x
i
x_i
xi , 使用公式
A
A
A 中没有出现过的 变元
x
j
x_j
xj 进行替换 , 所得到的公式
A
′
⇔
A
A' \Leftrightarrow A
A′⇔A ;
如 :
∀
x
F
(
x
)
∨
∀
x
¬
G
(
x
,
y
)
\forall x F(x) \lor \forall x \lnot G(x, y)
∀xF(x)∨∀x¬G(x,y) 如果要求其前束范式 , 前后有两个
x
x
x , 这里使用换名规则 , 将某个换成没有出现过的 指导变元
z
z
z , 换名后为
∀
x
F
(
x
)
∨
∀
z
¬
G
(
z
,
y
)
\forall x F(x) \lor \forall z \lnot G(z, y)
∀xF(x)∨∀z¬G(z,y) ;
三、 前束范式示例
求
∀
x
F
(
x
)
∨
¬
∃
x
G
(
x
,
y
)
\forall x F(x) \lor \lnot \exist x G(x, y)
∀xF(x)∨¬∃xG(x,y) 的前束范式 ;
上述公式不是前束范式 , 其 量词
∀
x
\forall x
∀x 的辖域是
F
(
x
)
F(x)
F(x) , 量词
∃
x
\exist x
∃x 的辖域是
G
(
x
,
y
)
G(x, y)
G(x,y) , 两个辖域都没有覆盖完整的公式 ;
使用 等值演算 和 换名规则 , 求前束范式 ;
∀
x
F
(
x
)
∨
¬
∃
x
G
(
x
,
y
)
\forall x F(x) \lor \lnot \exist x G(x, y)
∀xF(x)∨¬∃xG(x,y)
使用 量词否定等值式 , 先把 否定联结词 移动到量词后面 , 使用的等值式为
¬
∃
x
A
(
x
)
⇔
∀
x
¬
A
(
x
)
\lnot \exist x A(x) \Leftrightarrow \forall x \lnot A(x)
¬∃xA(x)⇔∀x¬A(x) ;
⇔
∀
x
F
(
x
)
∨
∀
x
¬
G
(
x
,
y
)
\Leftrightarrow \forall x F(x) \lor \forall x \lnot G(x, y)
⇔∀xF(x)∨∀x¬G(x,y)
使用 换名规则 , 将第二个
∀
x
¬
G
(
x
,
y
)
\forall x \lnot G(x, y)
∀x¬G(x,y) 中的
x
x
x 换成
z
z
z ;
⇔
∀
x
F
(
x
)
∨
∀
z
¬
G
(
z
,
y
)
\Leftrightarrow \forall x F(x) \lor \forall z \lnot G(z, y)
⇔∀xF(x)∨∀z¬G(z,y)
使用 辖域扩张等值式 , 将
∀
x
\forall x
∀x 辖域扩张 , 使用的等值式为
∀
x
(
A
(
x
)
∨
B
)
⇔
∀
x
A
(
x
)
∨
B
\forall x ( A(x) \lor B ) \Leftrightarrow \forall x A(x) \lor B
∀x(A(x)∨B)⇔∀xA(x)∨B
⇔
∀
x
(
F
(
x
)
∨
∀
z
¬
G
(
z
,
y
)
)
\Leftrightarrow \forall x ( F(x) \lor \forall z \lnot G(z, y) )
⇔∀x(F(x)∨∀z¬G(z,y))
再次使用 辖域扩张等值式 , 将
∀
z
\forall z
∀z 辖域扩张 , 使用的等值式为
∀
x
(
A
(
x
)
∨
B
)
⇔
∀
x
A
(
x
)
∨
B
\forall x ( A(x) \lor B ) \Leftrightarrow \forall x A(x) \lor B
∀x(A(x)∨B)⇔∀xA(x)∨B
⇔
∀
x
∀
z
(
F
(
x
)
∨
¬
G
(
z
,
y
)
)
\Leftrightarrow \forall x \forall z ( F(x) \lor \lnot G(z, y) )
⇔∀x∀z(F(x)∨¬G(z,y))
此时已经是前束范式了 ;
使用 命题逻辑 等值式 中的 蕴涵等值式
⇔
∀
x
∀
z
(
G
(
z
,
y
)
→
F
(
x
)
)
\Leftrightarrow \forall x \forall z ( G(z, y) \to F(x) )
⇔∀x∀z(G(z,y)→F(x))
四、 谓词逻辑推理定律
下面推理定律是单向的 , 从左边可以推理出右边 , 从右边不能推理出左边 ; ( 不是等值式 )
①
∀
x
A
(
x
)
∨
∀
x
B
(
x
)
⇒
∀
x
(
A
(
x
)
∨
B
(
x
)
)
\rm \forall x A(x) \lor \forall x B(x) \Rightarrow \forall x ( A(x) \lor B(x) )
∀xA(x)∨∀xB(x)⇒∀x(A(x)∨B(x))
对应 全称量词 分配率 , 等值式中 只适用于 合取联结词 , 就是因为上述 析取时 , 从右往左 是错误的 , 只能从左往右推理 ;
②
∃
x
(
A
(
x
)
∧
B
(
x
)
)
⇒
∃
x
A
(
x
)
∧
∃
x
B
(
x
)
\rm \exist x ( A(x) \land B(x) ) \Rightarrow \exist x A(x) \land \exist x B(x)
∃x(A(x)∧B(x))⇒∃xA(x)∧∃xB(x)
③
∀
x
(
A
(
x
)
→
B
(
x
)
)
⇒
∀
x
A
(
x
)
→
∀
x
B
(
x
)
\rm \forall x ( A(x) \to B(x) ) \Rightarrow \forall x A(x) \to \forall x B(x)
∀x(A(x)→B(x))⇒∀xA(x)→∀xB(x)
④
∀
x
(
A
(
x
)
→
B
(
x
)
)
⇒
∃
x
A
(
x
)
→
∃
x
B
(
x
)
\rm \forall x ( A(x) \to B(x) ) \Rightarrow \exist x A(x) \to \exist x B(x)
∀x(A(x)→B(x))⇒∃xA(x)→∃xB(x)
