离散数学第四章 谓词演算的推理理论 归结推理系统
- 格式:ppt
- 大小:450.00 KB
- 文档页数:53
谓词演算的推理理论在谓词逻辑中,除了命题逻辑中的推理规则继续有效外,还有以下四条规则。
设前提Г= {A 1,A 2,…,A k }.1. 全称指定规则(全称量词消去规则)US :例1 取个体域为实数域,F(x, y): x>y, P(x)=(∃y) F(x,y), 则(∀x)P(x) ⇒P(z)=(∃y) F(z,y).而不能(∀x) P(x) ⇒P(y)=(∃y) F(y,y).其中x,y 是个体变项符号,c 为任意的个体常量.或 (∀x ) P (x ) ∴ P (y ) (∀x) P (x )∴ P (c )2 . 全称推广规则(全称量词引入规则) UG:P(x)∴ (∀x)P(x)其中x是个体变项符号,且不在前提的任何公式中自由出现.3. 存在指定规则(存在量词消去规则) ES:(∃x)P(x)∴ P(c)1)c是使P(x)为真的特定的个体常量,不是任意的.2)c不在前提中或者先前推导公式中出现或自由出现,换句话说,此c是在该推导之前从未使用过的.4. 存在推广规则(存在量词引入规则) EG:P(c)∴ ( x)P(x)其中x是个体变项符号, c是个体常项符号.谓词逻辑的推理理论由下列要素构成.1. 等价公式2. 蕴含式3. 推理规则:(1) 前提引入规则 (2) 结论引入规则(3) CP推理规则 (4)归谬论(5) US规则 (6) UG规则(7) ES规则 (8) EG规则1)在推导的过程中,可以引用命题演算中的规则P、规则T、规则CP .2)为了在推导过程中消去量词,可以引用规则US和规则ES来消去量词.3)当所要求的结论可能被定量时,此时可引用规则UG和规则EG将其量词加入.4)证明时可采用如命题演算中的直接证明方法和间接证明方法.5)在推导过程中,对消去量词的公式或公式中没含量词的子公式,完全可以引用命题演算中的基本等价公式和基本蕴涵公式.6)在推导过程中,对含有量词的公式可以引用谓词中的基本等价公式和基本蕴涵公式.7)在推导过程中,如既要使用规则US又要使用规则ES消去公式中的量词(只要有可能,我们总是先使用规则ES,再使用规则US)。
2.5 谓词演算的推理理论1.推理定律谓词演算中也存在一些基本的等价与蕴含关系,参见表2-2。
我们以此作为推理的基础,即推理定律。
表2-2序号 等价或蕴含关系 含义E27 E28 ┐∀xA(x)⇔∃x┐A(x)┐∃xA(x)⇔∀x┐A(x) 量词否定等值式E29 E30∀x(A(x)∧B(x))⇔∀xA(x)∧∀xB(x)∃x(A(x)∨B(x))⇔∃xA(x)∨∃xB(x)量词分配等值式(量词分配律)E31 E32 E33 E34 E35 E36 E37 E38 E39 E40 E41 E42 E43∀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(B∨A(x))⇔ B∨∀xA(x)∀x(B∧A(x))⇔ B∧∀xA(x)∃x(B∨A(x))⇔ B∨∃xA(x)∃x(B∧A(x))⇔ B∧∃xA(x)∃x(A(x)→B(x))⇔∀xA(x)→∃xB(x)∀x(A(x)→B)⇔∃xA(x)→B∃xA(x)→B⇔∀x(A(x)→B)A→∀xB(x)⇔∀x(A→B(x))A→∃xB(x)⇔∃x(A→B(x))量词作用域的扩张与收缩I21 I22∀xA(x)∨∀xB(x)⇒∀x(A(x)∨B(x))∃x(A(x)∧B(x))⇒∃xA(x)∧∃xB(x)I23 ∃xA(x)→∀xB(x)⇒∀x(A(x)→B(x))表2-2中的I、E序号是接着表1-5和1-8排列的,表明它们都是谓词逻辑的推理定律。
E31~E34与E35~E38只是A和B的顺序不同。
2.量词的消除与产生规则谓词推理可以看作是对命题推理的扩充。
除了原来的P规则(前提引入)、T规则(命题等价和蕴含)及反证法、CP规则外,为什么还需引入新的推理规则呢?命题逻辑中只有一种命题,但谓词逻辑中有2种,即量词量化的命题和谓词填式命题。
如果仅由表2-2的推理定律就可推证,并不需要引入新的规则,但这种情况十分罕见,也失去了谓词逻辑本身的意义。
离散数学基础2017-11-19•一些基本定义:−谓词公式中原子或原子的否定形式称为文字。
−文字的析取式称为子句。
−不包含任何文字的子句称为空子句。
»空子句是不可满足的。
−若干相互形成合取关系的子句以集合元素的形式构成集合,称为子句集。
•定理:谓词公式的子句集化归−任何谓词公式都可应用谓词逻辑等值式及推理规则化成相应的子句集。
−过程(构造性证明):(1)蕴涵消去:消去条件蕴涵符号;(2)否定词深入:否定词直接作用在原子上;(3)变量标准化:处于不同量词辖域的约束变量根据易名规则使用不同的变量名;(4)消去存在量词:对不受约束的存在量词,使用常量符号例化;对被约束的存在量词,引入Skolem函数建立依赖;(5)化为前束形: (前缀)(母式),前缀包含全称量词串,母式中不包含任何量词;(6)将母式化为合取范式;(7)消去全称量词(自由变量默认全称量化);(8)由(6)中各极大项构成子句;(9)变量分离:使各子句不含同名变量。
•例:∀xP(x)→∀x∃y((P(x)∨Q(x))→R(x, y))¬ ∀xP(x) ∨ ∀x∃y(¬(P(x) ∨ Q(x)) ∨ R(x, y)) 蕴涵消去∃x¬P(x) ∨ ∀x∃y ((¬P(x) ˄ ¬Q(x)) ∨ R(x, y))否定词深入∃x¬P(x) ∨ ∀z∃y ((¬P(z) ˄ ¬Q(z)) ∨ R(z, y))变量标准化¬P(c) ∨ ∀z((¬P(z) ˄ ¬Q(z)) ∨ R(z, f Skolem(z))消去存在量词∀z(¬P(c) ∨ ((¬P(z) ˄ ¬Q(z)) ∨ R(z, f Skolem(z))) 化为前束形∀z((¬P(c) ∨ ¬P(z) ∨ R(z, f Skolem(z)) ˄(¬P(c) ∨ ¬Q(z) ∨ R(z, f Skolem(z)))将母式化为合取范式¬P(c) ∨ ¬P(z) ∨ R(z, f Skolem(z), ¬P(c) ∨ ¬Q(z) ∨ R(z, f Skolem(z) 消去全称量词 {¬P(c) ∨ ¬P(u) ∨ R(u, f Skolem(u), ¬P(c) ∨ ¬Q(v) ∨ R(v, f Skolem(v)} 变量分离−说明:»子句中的变量总是被默认为全称量化的;»化归得到的子句集不等价于原公式;»考虑到量词消去和引入规则的应用,若公式 A 在逻辑上遵循公式集 S,则也遵循由 S 变换成的子句集。
第二章谓词逻辑2—1基本概念例题1. 所有的自然数都是整数。
设N(x):x是自然数。
I(x):x是整数。
此命题可以写成∀x(N(x)→I(x))例题2. 有些自然数是偶数。
设E(x):x是偶数。
此命题可以写成∃x(N(x)∧E(x))例题3. 每个人都有一个生母。
设P(x):x是个人。
M(x,y):y是x的生母。
此命题可以写成:∀x(P(x)→∃y(P(y)∧M(x,y))) 2-2 谓词公式及命题符号化例题1. 如果x是奇数,则2x是偶数。
其中客体x与客体2x之间就有函数关系,可以设客体函数g(x)=2x,谓词O(x):x是奇数,E(x):x是偶数,则此命题可以表示为:∀x(O(x)→E(g(x)))例题2 小王的父亲是个医生。
设函数f(x)=x的父亲,谓词D(x):x是个医生,a:小王,此命题可以表示为D(f(a))。
例题3 如果x和y都是奇数,则x+y是偶数。
设h(x,y)=x+y ,此命题可以表示为:∀x∀y((O(x)∧O(y))→E(h(x,y))命题的符号表达式与论域有关系两个公式:一般地,设论域为{a1,a2,....,an},则有(1). ∀xA(x)⇔A(a1)∧A(a2)∧......∧A(an)(2). ∃xB(x)⇔B(a1)∨B(a2)∨......∨B(an)1.每个自然数都是整数。
该命题的真值是真的。
表达式∀x(N(x)→I(x))在全总个体域的真值是真的,因∀x(N(x)→I(x))⇔(N(a1)→I(a1))∧(N(a2)→I(a2))∧…∧(N(an)→I(an))式中的x不论用自然数客体代入,还是用非自然数客体代入均为真。
例如(N(0.1)→I(0.1))也为真。
而∀x(N(x)∧I(x))在全总个体域却不是永真式。
∀x(N(x)∧I(x))⇔(N(a1)∧I(a1))∧(N(a2)∧I(a2)) ∧…∧(N(an)∧I(an))比如x用0.2代入(N(0.2)∧I(0.2))就为假。