【数理逻辑】谓词逻辑 ( 前束范式 | 前束范式转换方法 | 谓词逻辑基本等值式 | 换名规则 | 谓词逻辑推理定律 )
文章目录
- 一、 前束范式
- 二、 前束范式转换方法
- 三、 前束范式示例
- 四、 谓词逻辑推理定律
一、 前束范式
公式 AAA 有如下形式 :
Q1x1Q2x2⋯QkxkBQ_1 x_1 Q_2 x_2 \cdots Q_kx_k BQ1x1Q2x2⋯QkxkB
则称 AAA 是 前束范式 ; 前束范式 AAA 的相关元素 说明 :
量词 : QiQ_iQi 是量词 , 全称量词 ∀\forall∀ , 或 存在量词 ∃\exist∃ ;
指导变元 :xix_ixi 是 指导变元 ;
BBB 公式 : BBB 是谓词逻辑公式 , 其中不含有量词 , BBB 中 可以含有 前面的 x1,x2,⋯,xkx_1 , x_2 , \cdots , x_kx1,x2,⋯,xk 指导变元 , 也 可以不含有 其中的某些变元 ;
( BBB 中一定不能含有量词 )
二、 前束范式转换方法
求一个谓词逻辑公式的前束范式 , 使用 基本等值式 , 或 换名规则 ;
基本等值式 : 参考博客 【数理逻辑】谓词逻辑 ( 谓词逻辑基本等值式 | 消除量词等值式 | 量词否定等值式 | 量词辖域收缩扩张等值式 | 量词分配等值式 )
换名规则 : 公式 AAA 中 , 某个量词辖域中 , 某个约束 出现的 个体变元 对应的 指导变元 xix_ixi , 使用公式 AAA 中没有出现过的 变元 xjx_jxj 进行替换 , 所得到的公式 A′⇔AA' \Leftrightarrow AA′⇔A ;
如 : ∀xF(x)∨∀x¬G(x,y)\forall x F(x) \lor \forall x \lnot G(x, y)∀xF(x)∨∀x¬G(x,y) 如果要求其前束范式 , 前后有两个 xxx , 这里使用换名规则 , 将某个换成没有出现过的 指导变元 zzz , 换名后为 ∀xF(x)∨∀z¬G(z,y)\forall x F(x) \lor \forall z \lnot G(z, y)∀xF(x)∨∀z¬G(z,y) ;
三、 前束范式示例
求 ∀xF(x)∨¬∃xG(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) , 两个辖域都没有覆盖完整的公式 ;
使用 等值演算 和 换名规则 , 求前束范式 ;
∀xF(x)∨¬∃xG(x,y)\forall x F(x) \lor \lnot \exist x G(x, y)∀xF(x)∨¬∃xG(x,y)
使用 量词否定等值式 , 先把 否定联结词 移动到量词后面 , 使用的等值式为 ¬∃xA(x)⇔∀x¬A(x)\lnot \exist x A(x) \Leftrightarrow \forall x \lnot A(x)¬∃xA(x)⇔∀x¬A(x) ;
⇔∀xF(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) 中的 xxx 换成 zzz ;
⇔∀xF(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)⇔∀xA(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)⇔∀xA(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))
四、 谓词逻辑推理定律
下面推理定律是单向的 , 从左边可以推理出右边 , 从右边不能推理出左边 ; ( 不是等值式 )
① ∀xA(x)∨∀xB(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))⇒∃xA(x)∧∃xB(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))⇒∀xA(x)→∀xB(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))⇒∃xA(x)→∃xB(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)
【数理逻辑】谓词逻辑 ( 前束范式 | 前束范式转换方法 | 谓词逻辑基本等值式 | 换名规则 | 谓词逻辑推理定律 )相关推荐
- 离散数学-谓词逻辑与前束范式
谓词逻辑 三段论 谓词公式 命题与命题函数,命题与命题函数的表达 谓词公式的赋值 谓词公式的等价 谓词公式的永真蕴含式 谓词公式中量词的消去与转换 有限论域消去量词 量词转换 量词辖域的扩充与收缩 量 ...
- 【数理逻辑】谓词逻辑 ( 判断一阶谓词逻辑公式真假 | 解释 | 示例 | 谓词逻辑公式类型 | 永真式 | 永假式 | 可满足式 | 等值式 )
文章目录 一. 判断谓词逻辑公式真假 ( 语义 ) 二. 谓词逻辑 "解释" 三. 谓词逻辑 "解释" 示例 四. 谓词逻辑公式类型 一. 判断谓词逻辑公式真假 ...
- 【数理逻辑】谓词逻辑 ( 谓词逻辑基本等值式 | 消除量词等值式 | 量词否定等值式 | 量词辖域收缩扩张等值式 | 量词分配等值式 )
文章目录 一. 消除量词 等值式 二. 量词否定 等值式 三. 量词辖域收缩扩张 等值式 四. 量词分配 等值式 一. 消除量词 等值式 消除量词等值式 : 有限个体域 D={a1,a2,⋯,an}D ...
- 【数理逻辑】命题逻辑 ( 等值演算 | 幂等律 | 交换律 | 结合律 | 分配律 | 德摩根律 | 吸收率 | 零律 | 同一律 | 排中律 | 矛盾律 | 双重否定率 | 蕴涵等值式 ... )
文章目录 一.等值演算 二.等值式 三.基本等值式 四.基本运算 五.等值演算 基于上一篇博客 [数理逻辑]命题逻辑 ( 命题与联结词回顾 | 命题公式 | 联结词优先级 | 真值表 可满足式 矛盾式 ...
- 离散数学蕴含等值式前件为假命题为真的理解
蕴含等值式:P->Q<=>~PvQ,如何理解P为假时,P->Q为真命题? 蕴含式P->Q表示,如果P那么Q,显然:如果P为真则Q为真,P→Q是真命题,当P为真命题,而Q为 ...
- 离散数学 第二章 谓词逻辑 2-6 前束范式
在命题演算中,常常要将公式化成规范形式,对于谓词演算,也有类似情况,一个谓词演算公式,可以化为与它等价的范式. 定义2-6.1 一个公式,如果量词均在全式的开头,它们的作用域,延伸到整个公式的末尾,则 ...
- 离散数学 基本等值式
提示:图片像素够大(2878 x 3451),可直接保存 欢迎转载!如转载请附上本文地址 若您在上文发现了错误,请在评论区处反馈,谢谢!
- 每个计算机系的学生都学离散数学,离散数学一阶逻辑精要.ppt
离散数学一阶逻辑精要.ppt 2.谓词公式 中量词 的辖域是( ). A. B. C. D. 3.谓词公式 中变元 是( ). A. 自由变元 B. 约束变元 C. 既不是自由变元也不是约束变元 D. ...
- 一阶逻辑等值式及前束范式
一阶逻辑等值式及前束范式 定义2.10 等值式 定理2.1 量词否定等值式 定理2.2 量词辖域收缩与扩张等值式 定理2.3 量词分配等值式 定理2.4 定理2.11 前束范式 例 定义2.10 等值 ...
最新文章
- matplotlib error - no module named tkinter
- [Java学习］Striing StringBuffer StringBuilder 的比
- 全局变量、静态全局变量、静态局部变量和局部变量的区别
- Redis分布式锁原理解析
- c#中BackGroundWorker控件
- Layui导航、面包屑
- 美国要贩卖网民隐私：最大成人网站出手反击
- vs2010旗舰版产品密钥
- 处理机调度之时间片轮转调度算法实现
- 信息安全技术及应用 系统安全防护技术
- 单片机应用系统设计技术——单片机出租车计费器
- 【备忘】【No5】微信公众平台开发入门到实战开发视频教程（Java+PHP)
- python手机屏幕自动点击代码_鼠标隔段时间自动点击屏幕
- MyBatis 遇到 Error updating database.问题
- ElasticSearch（狂神说笔记）
- 安卓开发——android8.0应用崩溃，报错： Only fullscreen opaque activities can request orientation
- 计算机毕业设计springboot+vue基本微信小程序的校园二手闲置物品交易小程序 uniapp
- 需求评审会议如何召开
- [Computer Architecture读书笔记] H.2 Detecting and Enhancing Loop-Level Parallelism
- linux 第十一天 linuxprobe