【数理逻辑】谓词逻辑 ( 前束范式 | 前束范式转换方法 | 谓词逻辑基本等值式 | 换名规则 | 谓词逻辑推理定律 )

韩曙亮

发布于 2023-03-28 09:55:53

1.8K0

文章目录

一、前束范式

公式

A

$A$

有如下形式 :

Q_{1} x_{1} Q_{2} x_{2} \dots Q_{k} x_{k} B

$Q_1 x_1 Q_2 x_2 \cdots Q_kx_k B$

则称

A

$A$

是 前束范式 ; 前束范式

A

$A$

的相关元素说明 :

量词 :

Q_{i}

$Q_i$

是量词 , 全称量词

\forall

$\forall$

, 或存在量词

Undefined control sequence \exist

$\exist$

;

指导变元 :

x_{i}

$x_i$

是指导变元 ;

B

$B$

公式 :

B

$B$

是谓词逻辑公式 , 其中不含有量词 ,

B

$B$

中可以含有前面的

x_{1}, x_{2}, \dots, x_{k}

$x_1 , x_2 , \cdots , x_k$

指导变元 , 也可以不含有其中的某些变元 ;

(

B

$B$

中一定不能含有量词 )

二、前束范式转换方法

求一个谓词逻辑公式的前束范式 , 使用基本等值式 , 或换名规则 ;

基本等值式 : 参考博客【数理逻辑】谓词逻辑 ( 谓词逻辑基本等值式 | 消除量词等值式 | 量词否定等值式 | 量词辖域收缩扩张等值式 | 量词分配等值式 )

换名规则 : 公式

A

$A$

中 , 某个量词辖域中 , 某个约束出现的个体变元对应的指导变元

x_{i}

$x_i$

, 使用公式

A

$A$

中没有出现过的变元

x_{j}

$x_j$

进行替换 , 所得到的公式

$A' \Leftrightarrow A$

;

如 :

$\forall x F(x) \lor \forall x \lnot G(x, y)$

如果要求其前束范式 , 前后有两个

$x$

, 这里使用换名规则 , 将某个换成没有出现过的指导变元

$z$

, 换名后为

$\forall x F(x) \lor \forall z \lnot G(z, y)$

;

三、前束范式示例

求

$\forall x F(x) \lor \lnot \exist x G(x, y)$

的前束范式 ;

上述公式不是前束范式 , 其量词

$\forall x$

的辖域是

$F(x)$

, 量词

$\exist x$

的辖域是

G (x, y)

$G(x, y)$

, 两个辖域都没有覆盖完整的公式 ;

使用等值演算和换名规则 , 求前束范式 ;

Undefined control sequence \exist

$\forall x F(x) \lor \lnot \exist x G(x, y)$

使用量词否定等值式 , 先把否定联结词移动到量词后面 , 使用的等值式为

Undefined control sequence \exist

$\lnot \exist x A(x) \Leftrightarrow \forall x \lnot A(x)$

;

\Leftrightarrow \forall x F (x) \lor \forall x \neg G (x, y)

$\Leftrightarrow \forall x F(x) \lor \forall x \lnot G(x, y)$

使用换名规则 , 将第二个

\forall x \neg G (x, y)

$\forall x \lnot G(x, y)$

中的

x

$x$

换成

z

$z$

;

\Leftrightarrow \forall x F (x) \lor \forall z \neg G (z, y)

$\Leftrightarrow \forall x F(x) \lor \forall z \lnot G(z, y)$

使用辖域扩张等值式 , 将

\forall x

$\forall x$

辖域扩张 , 使用的等值式为

\forall x (A (x) \lor B) \Leftrightarrow \forall x A (x) \lor B

$\forall x ( A(x) \lor B ) \Leftrightarrow \forall x A(x) \lor B$

\Leftrightarrow \forall x (F (x) \lor \forall z \neg G (z, y))

$\Leftrightarrow \forall x ( F(x) \lor \forall z \lnot G(z, y) )$

再次使用辖域扩张等值式 , 将

\forall z

$\forall z$

辖域扩张 , 使用的等值式为

\forall x (A (x) \lor B) \Leftrightarrow \forall x A (x) \lor B

$\forall x ( A(x) \lor B ) \Leftrightarrow \forall x A(x) \lor B$

\Leftrightarrow \forall x \forall z (F (x) \lor \neg G (z, y))

$\Leftrightarrow \forall x \forall z ( F(x) \lor \lnot G(z, y) )$

此时已经是前束范式了 ;

使用命题逻辑等值式中的蕴涵等值式

\Leftrightarrow \forall x \forall z (G (z, y) \to F (x))

$\Leftrightarrow \forall x \forall z ( G(z, y) \to F(x) )$

四、谓词逻辑推理定律

下面推理定律是单向的 , 从左边可以推理出右边 , 从右边不能推理出左边 ; ( 不是等值式 )

①

\forall x A (x) \lor \forall x B (x) \Rightarrow \forall x (A (x) \lor B (x))

$\rm \forall x A(x) \lor \forall x B(x) \Rightarrow \forall x ( A(x) \lor B(x) )$

对应全称量词分配率 , 等值式中只适用于合取联结词 , 就是因为上述析取时 , 从右往左是错误的 , 只能从左往右推理 ;

②

Undefined control sequence \exist

$\rm \exist x ( A(x) \land B(x) ) \Rightarrow \exist x A(x) \land \exist x B(x)$

③

\forall x (A (x) \to B (x)) \Rightarrow \forall x A (x) \to \forall x B (x)

$\rm \forall x ( A(x) \to B(x) ) \Rightarrow \forall x A(x) \to \forall x B(x)$

④

Undefined control sequence \exist

$\rm \forall x ( A(x) \to B(x) ) \Rightarrow \exist x A(x) \to \exist x B(x)$

本文参与腾讯云自媒体同步曝光计划，分享自作者个人站点/博客。

原始发表：2020-09-28，如有侵权请联系 cloudcommunity@tencent.com 删除

博客

本文分享自作者个人站点/博客前往查看

如有侵权，请联系 cloudcommunity@tencent.com 删除。

本文参与腾讯云自媒体同步曝光计划，欢迎热爱写作的你一起参与！

博客

登录后参与评论

暂无评论