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

韩曙亮

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

2.6K0

文章被收录于专栏：韩曙亮的移动开发专栏韩曙亮的移动开发专栏

文章目录

一、前束范式

公式

有如下形式 :

Q_1 x_1 Q_2 x_2 \cdots Q_kx_k B

则称

是 前束范式 ; 前束范式

的相关元素说明 :

量词 :

Q_i

是量词 , 全称量词

\forall

, 或存在量词

\exist

;

指导变元 :

x_i

是指导变元 ;

公式 :

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

中可以含有前面的

x_1 , x_2 , \cdots , x_k

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

(

中一定不能含有量词 )

二、前束范式转换方法

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

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

换名规则 : 公式

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

x_i

, 使用公式

中没有出现过的变元

x_j

进行替换 , 所得到的公式

A' \Leftrightarrow A

;

如 :

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

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

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

, 换名后为

\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)

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

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

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

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

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

;

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

使用换名规则 , 将第二个

\forall x \lnot G(x, y)

中的

换成

;

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

使用辖域扩张等值式 , 将

\forall x

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

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

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

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

\forall z

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

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

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

此时已经是前束范式了 ;

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

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

四、谓词逻辑推理定律

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

①

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

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

②

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

③

\rm \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 \exist x A(x) \to \exist x B(x)

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

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

博客