离散数学第四章谓词演算的推理理论-归结推理系统共51页文档

格式：ppt
大小：707.50 KB
文档页数：51

下载文档原格式

离散数学第四章谓词演算的推理理论归结推理系统

证明：令 P(e)表示“e为人”； W(e)表示“e喜欢步行”； D(e)表示“e喜欢乘汽车”； R(e)表示“e喜欢骑自行车”
证明(续)
则已知知识可以翻译为：（1） ∀x(P(x) →(W(x) → D(x))) （2） ∀x(P(x) →(D(x) ∨ R(x))) （3） ∃x(P(x) ∧ R(x)) 结论为：
例设有 P(x，g(a))Q(y) P(z，g(a))Q(z)
可得归结式如下：
Q(y) Q(z)
{ z/x}
Q(y) Q(x) P(x，g(a))P(z，g(a))
{ x/z} { z/y}
归结反演系统——产生式系统
子句集看作为一个综合数据库，而规则表就是归结，表中的规则用到数据库中的
子句对，产生一个新的子句，把新子句加入数据库中产生新的数据库，形成新的归结，重复此过程，观察数据库中是否含有空子句。
三、归结反演算系统的应用
在人工智能领域中的规划生成问题。
例(p48)给机器人r 编制一程序，使它能够登上一只椅子c以取下挂在房顶的香蕉b。
4.3.3 霍恩子句逻辑程序
一、子句的蕴含表示形式二、霍恩子句逻辑程序
超逻辑的控制信息
许多人工智能系统中使用的知识是由一般的蕴含表达式来表示的。如果把蕴含式
(PQ)R 化为等价的析取式
P Q R ，往往会丢失可能包含在蕴含式中的重要的超逻辑的控制信息。
基于规则的演绎系统
将知识分为两类：
一类是规则，其由蕴含式表示，它表达了有关领
域的一般知识，且可作为产生式规则来使用；
另一类是事实，其由不包含蕴含式的陈述组成，
它们用来表达某一领域专门的知识。
{ a/x1} (3)(1)归结 { a/x2} (4)(2)归结 { a/y} (5)(6)归结

离散数学24谓词演算的推理理论

谓词演算的推理理论在谓词逻辑中，除了命题逻辑中的推理规则继续有效外，还有以下四条规则。

设前提Г= {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)。

离散数学的谓词逻辑详解

两种量词: 全称量词和存在量词.
全称量词:
1.全称量词：（任意，所有） x: “对一切x”，“对所有的x”， “对任一x”
如： x P(x) ┐ x P(x) x ┐ P(x)
“对一切x，P(x)是真” “并非对一切x，P(x)是真” “对一切x， ┐ P(x) 是真”
如: “ 所有人都是要死的”
于是令 M（x）：x是人。（1） x（M(x)→D(x)) （2） x (M（x）∧ ┐G（x））
命题符号化(翻译)：
将汉语(或其他自然语言)语句翻译成逻辑表达式，这在数学、逻辑编程、人工智能、软件工程以及许多其他学科中都是一项重要的任务。翻译的目的是生成简单而有用的逻辑表达式。
命题符号化：
1.谓词与个体词
将简单命题分解成个体与谓词这样两个组成部分。谓词，通常是用来描述个体的性质或特征，或者个体之间的关系。谓词逻辑，是命题逻辑的扩充与发展。
例1：下面两个命题 1. 张华是学生 2. 李明是学生
a: 张华 b:李明 H：是学生，则 H（x）:x是学生
1，2可分别表示成 H(a) ，H(b). 这样表示就揭示了两命题间有相同的谓语这一特征。
变元的约束
例1 ：令 P（x， y）：“ x<y ”， Q（x）：x是有理数； F（x）：x可以表示为分数。
判断下列式子那些是命题函数，那些是命题？
P(x， y)
P(x， y)∧Q(x)
Q(x) → F(x) x（Q(x)→ F(x)) x Q(x)→ F(x)
自由变元与约束变元
[定义] 紧接于量词之后最小的子公式称为量词的辖域．(量词的辖域是紧接其后的公式，除非辖域是个原子公式，否则应在公式的两侧插入圆括号。)

人工智能导论课件：第四章谓词逻辑与归结原理

5
谓词逻辑
是一种形式语言，具有严密的理论体系是一种常用的知识表示方法, 例：
City（北京） City（上海） Age（张三，23） (X)(Y)(Z)(father(X, Y)father(Y,
Z)gf(X, Z)
6
归结原理
归结原理是一种定理证明方法，1965年由 J.A.Robinson提出，从理论上解决了定理证明问题。当时被认为是人工智能领域的重大突破。
例如:令E为p(x,y,f(a))
={b/x,f(x)/y},则 E= ?
E=p(b,f(x),f(a)) 此例显示了同时置换的含义. 可以看到E是
在E上的作用,也就是将E中的(i=1, ,n)同时换成相应的ti所得到的公式.
34
ห้องสมุดไป่ตู้
置换乘法
定义令 ={s1/y1,,sm/ym}, ={t1/x1,,tn/xn},则与的复合是
32
置换
定义: 置换是形如{t1/x1,,tn/xn}的有限集,其中xi是互不相同的变量,ti是不等于xi的项,且xi与ti互不循环出现. 如果ti都是不含变量的项(基项),称该置换为基置换. 若={ },则称为空置换(表示不做置换),记为.
例如:1) {a/x,g(y)/y,f(g(b))/z}是一个置换? (是, 但不是基置换).
F1F2…Fn~W为永假，可以通过证明F所对应的子句集S=S0∪{~W}是不可满足的。
22
命题： P|=F P{F}是不可满足的。证明: ① 若P {~F}是不可满足的，则 P|= F ② 若P|=F 则 P {~F}是不可满足的。（反证法）
23
归结原理
基本思想将待证明的逻辑公式的结论（F），通过等值公式转换成附加前提，再证明该逻辑公式是不可满足的。

离散数学(第四章)解读.

§2.1 一阶逻辑命题符号化
例如，下列推理：所有的人都是要死的。苏格拉底是人。苏格拉底是要死的。众所周知,这是真命题。但在命题逻辑中,如果用P,Q,R表示以上三个命题，则上述推理过程为：（P∧Q）R。借助命题演算的推理理论不能证明其为重言式。

§2.1 一阶逻辑命题符号化
原因：命题逻辑不能将命题之间的内在联系和数量关系反映出来。解决办法：将命题进行分解。
§2.1 一阶逻辑命题符号化
设谓词H表示“是劳动模范”, a表示个体名称张明, b表示个体名称李华,c表示个体名称这只老虎，那么H(a) 、 H(b)、 H(c)表示三个不同的命题,但它们有一个共同的形式,即H(x).一般地， H(x)表示客体x具有性质H。这里x表示抽象的或泛指的客体，称为个体变元，常用小写英文字母x, y, z, …表示。相应地，表示具体或特定的客体的词称为个体常项，常用小写英文字母a,b,c, …表示。
§2.1 一阶逻辑命题符号化
刻划一个个体性质的词称之为一元谓词 ,刻划 n 个个体之间关系的词称之为n元谓词. 一般我们用大写英文字母表示谓词，用小写英文字母表示客体名称，例如，将上述谓词分别记作大写字母F、G、H、R，S则上述命题可表示为： (1) F(a) a：张明 (2) F(b) b：李华 (3) G(c) c：王红 (4) H(s,t) s：小李 t：小赵 (5) R(a,b,c) (6) S(a,b) a:阿杜 b:阿寺其中(1)、(2)、 (3)为一元谓词， (4) 、 (6)为二元谓词， (5)为三元谓词。
2.5谓词演算的推理理论(Inference theory of
predicate calculus)
§2.1 一阶逻辑命题符号化

《谓词演算推理理论》课件

3
前向链归结和向前式归结
研究前向链归结和向前式归结的思想和实践。
归结推理的优化策略
1 归结定理和完备性定理
深入了解归结定理和完备性定理，以及其在优化策略中的应用。
Hale Waihona Puke 2 应用领域探索归结推理在人工智能等领域中的实际应用，如自动定理证明。
谓词演算推理的拓展研究
谓词演算与基因组学的应用
探索谓词演算在基因组学研究中的应用，如基因表达分析。
谓词演算与知识表示的联系
研究谓词演算与知识表示技术的联系和互动。
谓词演算在数据分析和挖掘中的应用
了解谓词演算在数据分析和挖掘领域中的实际应用。
1
一阶谓词演算的语法和语义
学习一阶谓词演算的基本语法和语义，掌握谓词符号和项的使用。
2
一阶谓词演算的规则
了解一阶谓词演算的推理规则，包括合一、替换和归结等。
归结推理的基本思想和步骤
1
特征集归结和集合论归结
探索特征集归结和集合论归结的基本思想和步骤。
2
树剖归结和深度优先归结
了解树剖归结和深度优先归结的原理和应用。
《谓词演算推理理论》 PPT课件
本PPT课件将介绍谓词演算推理理论的基本概念和方法，以及其在人工智能、基因组学、计算机科学等领域中的重要性和应用。
什么是谓词演算推理理论
1 基本概念
了解谓词演算推理理论的起源、定义和基本原理。
2 形式和语义
探讨谓词逻辑公式的形式和语义，以及其在推理中的作用。
谓词演算推理的基本方法

离散数学-谓词演算的推理规则

解： P(x) ：x 是液体， G(x)：x是金属， R(x, y)：x 溶解 y ，
xG(x) y p(y) R(y, x)
20
例2、将下列命题译成自然语言，并确定其真值。
(个体域为 Z ) (1) xyG(x, y) ，其中G(x, y) : xy y 解：对任意正整数 x ，存在正整数 y，
F(x),G(x, y) 中的 x 是约束变元， G(x, y) 中的 y是自由变元； y 的辖域是F( y) ， F( y) 中的 y 是约束变元； R(x, y, z)中的 x, y, z 都是自由变元。
24
例5、设个体域为 A a,b,c将下面谓词公式中的
量词消除，写出与之等值的命题公式。 (1) xP(x) xR(x) 解 xP(x) xR(x)
§2.3 谓词演算的推理规则
重点：全称指定规则（US）（Universal Specification）存在指定规则（ES）（Existential Specification）全称推广规则（UG）（Universal Generalization）存在推广规则（EG）（Existential Specification）
3
3、全称推广规则（UG）
A( y) xA(x) 要求：（1）y是个体域中任一个体，且都有A( y)为真。
4、存在推广规则（EG）
A( y) xA(x)
要求：(1) y 是个体常元或变元，
(2)在公式A(y)中，y不出现在量词 x或x
的辖域内。
4
注：考察以下推理过程
① xyP x, y
②
yP(c, y)
谓词公式；辖域，约束变项，自由变项；代换实例；重言式，矛盾式，可满足式。 2、应用。 (1) 求某些公式在给定解释下的真值。 (2) 判断某些简单公式的类型。

离散数学L4谓词

谓词是命题函数
• 一元谓词P可视为从个体域D到集合{T,F} 上的映射:
P: D {T,F}
• n元谓词也是一样:
P: Dn {T,F}
• 注意:P(x)是命题形式但不是命题,因为其真值不确定.
– 仅当P取定为谓词常项,x取定为个体常项时, P(x)才成为命题.
Lu Chaojun, SJTU
谓词逻辑的基本概念
本章主要内容
• 谓词 • 量词 • 一阶谓词公式 • 自然语句的形式表示 • 公式的解释及真假性
Lu Chaojun, SJTU
谓词逻辑与命题逻辑的区别
• 命题逻辑:简单命题是分析的基本单元,不再对简单命题的内部结构进行分析.
– 例如P:“柏拉图是人”和Q:“亚里士多德是人”是两个相互独立的命题,看不出P和Q有什么联系.
Lu Chaojun, SJTU
14
量词的辖域
• 量词所约束的范围称为量词的辖域.即:
(x) (…辖域…) (x) (…辖域…)
• 在x(或x)的辖域内的自由x都被该量词约束.
– 例如(x)(P(x) Q(x)) – 但在(x)(P(x) (x)Q(x))中, Q(x)还处于最近
的(x)的辖域中,此x非自由,故不被(x)约束.
Lu Chaojun, SJTU
15
命题形式P(x)如何化为命题?
• 假设P含义确定,是谓词常项
– 若x用个体常项代入,则P(x) 真假就定了; – 或者将x量化,形如(x)P(x)或(x)P(x),这时也
确定了真假.
• 总之:命题中是不能有自由变元的. • 变元易名规则:约束变元改名不改变命题
的真值,即(x)P(x) = (y)P(y).

离散数学--第四章谓词逻辑推理

Dr Chen Guangxi
例4.1.1
注：在对 ∀x ( F ( x ) → G ( x )) 使用UI规则时，可以得 F(y) → G(y)，也可得F(c) → G(c)，其中y是任意的个体常项，c可为任意个体常项，由结论的需要取c为a。
。
Dr Chen Guangxi
例4.1.3
构造下面推理的证明前提： ¬∃ x ( F ( x ) ∧ H ( x )), ∀ x ( G ( x ) → H ( x ))
Dr Chen Guangxi
四条重要的推理规则
2.全称量词引入规则，简记为 UG
A( y) ∴ ∀xA( x)
成立的条件是：（1）y在A(y)中自由出现，且为任意的个体变项；（2）取代y的x不能在A(x)中约束出现过。
Dr Chen Guangxi
四条重要的推理规则
3.存在量词消去规则，简记为EI
∀x( H ( x ) → ¬F ( x))
G ( y) → ¬F ( y)
∀ x ( G ( x ) → H ( x )) G( y) → H ( y)
∀x (G ( x ) → ¬F ( x )) 本例要注意UI规则的用法!!
Dr Chen Guangxi
例题
构造推理
学术委员会的每个成员都是博士并且是教授。有些成员是青年人。因而，有的成员是青年教授。
∃xA( x) ∴ A(c)
成立的条件为：（1）c是使A(c)为真的特定的个体常项；（2）c不在A(x)中出现过；（3）若A(x)中除x外还有其它自由出现的个体变项时，此规则不能使用。
Dr Chen 为EG
A(c ) ∴ ∃ xA ( x )
Dr Chen Guangxi

第四章谓词演算的推理理论-永真推理系统

例 (续 )
证明:
x(P(x))(x P(x))
再证明 (x P(x)) x(P(x))
(3) P(x) xP(x)
公理21 公理3
(4) (P(x)xP(x)) ((xP(x))(P(x))) (5) (xP(x))(P(x)) 分(3)(4)
(4) △ (x (x) (1 ))
两次运用调头公理2
分离Байду номын сангаас1)(2)
存0规则
公理2
(5) △ ((x (x) (1 )) (1(x (x) ))) (6) △(1 (x(x) )) 分离(5)(6)
例(练习4.1(1))
证明:
x(P(x))(xP(x))
回顾: 量词作用域的收缩与扩张
设公式中不含有自由的x，则下面的公式成立:
x((x) → )= ( x(x) → )
x( →(x)) = (→x(x)) x((x)→ )= (x(x) →) x(→(x))= (→x(x)) 全称量词引入存在量词引入
例 (练习4.2)已知公理 (A) △(P(QP)) (B) △(PP) 及分离规则和全称规则，全称规则为： △(1(2(x)))├△(1(2x (x))) 试证：全0规则 △(x)├△x(x)
证: (1) △(x) (2) △ (P(QP)) (3) △ ((x) ((PP) (x) (4) △(PP) (x) (5) △(((PP) (x)) ((PP) ((PP) (x)))) (6) △((PP) ((PP) (x))) (7) △((PP) ((PP) x(x))) (8) △(PP) (9) △((PP) x(x)) (10) △(x(x))
基本符号（续）

1、下载文档前请自行甄别文档内容的完整性，平台不提供额外的编辑、内容补充、找答案等附加服务。
2、"仅部分预览"的文档,不可在线预览部分如存在完整性等问题,可反馈申请退款(可完整预览的文档不适用该条件!)。
3、如文档侵犯您的权益，请联系客服反馈,我们会尽快为您处理(人工客服工作时间：9:00-18:30)。

例已知表达式 P(x，g(y)，b)，考察置换:
P(x，g(a)，b) P(a，g(b)，b) P(f(y)，g(a)，b)
{a/y} {a/x，b/y } {f(y)/x，a/y }
一般地，置换可通过有序对的集合 {t1/v1，t2/v2，…，tn/vn}
来表达，其中ti/vi表示变量vi处处以项ti来代替。
例(p46-47) xP(x)x(A(x)y(B(y)W(x，y)))
解: (1)消去蕴含词
xP(x)x(A(x)y(B(y)W(x，y))) (2)约束变元改名：
利用改名方法对上式施行改名，以保证每一个量词约束的变元不同名。 xP(x)z(A(z)y(B(y)W(z，y)))
(3)化为前束范式 xzy(P(x)(A(z)(B(y)W(z，y))))
例设有 P(x，g(a))Q(y) P(z，g(a))Q(z)
可得归结式如下：
Q(y) Q(z)
{ z/x}
Q(y) Q(x) P(x，g(a))P(z，g(a))
{一个综合数据库，而规则表就是归结，表中的规则用到数据库中的
子句对，产生一个新的子句，把新子句加入数据库中产生新的数据库，形成新的归结，重复此过程，观察数据库中是否含有空子句。
从这些语句出发，证明语句： (4)一些有智慧的个体不能读。x(I(x)R(x))
引例 (p45，提取子句)
对应语句(1)至(3)的子句集为： (1) R(x1) L(x1) (2) H(x2) L(x2) (3) H(a) (4) I(a) 其中子句(3)(4)为对(3)式SKOLEM化而得，a为 SKOLEM常量。要证明的定理的否定式为：
x(I(x)R(x)), 即 x(I(x)R(x)) 化为子句形式为(5)： (5) I(x3)R(x3)
引例 (p45，归结)
(1) R(x1) L(x1) (2) H(x2) L(x2) (3) H(a)
(4) I(a)
(5) I(x3)R(x3) (6) R(a) (7) L(a) (8) H(a) (9) □
A(x1)B(f(x1))，A(x2)W(x2，f(x2))
例 (p47,续)
(2) x(A(x)y(N(y)W(x，y))) = x(A(x)y(N(y) W(x，y))) = x y (A(x) (N(y) W(x，y))) y (A(a) (N(y) W(a，y))) A(a) (N(y) W(a，y))
{a/ x3}(4)(5)归结 {a/ x1}(6)(1)归结 {a/ x2}(7)(2)归结
(8)(3)归结
注意：归结时使用了未讨论过的置换的概念。
4.3.1 置换
——项对变量的替换。置换准则为：
(1)置换必须处处进行。
(2)要求没有变量被含有同一变量的项来代替。如表达式P(x,g(x),b)中的x不能用含有x的项f(x)来置换，即P(f(x),g(f(x)),b)是错误的置换。
得到子句： A(a), N(y) W(a，y)
例 (p47,续)
要证明的结论为：有些作品不是小说。 x(B(x)N(x))
否定结论得到： x(B(x)N(x)) = x(B(x)N(x)) B(x)N(x)
得到子句： B(x)N(x)
例 (p47, 归结)
(1) A(x1)B(f(x1)) (2) A(x2)W(x2，f(x2)) (3) A(a) (4) N(y)W(a，y) (5) B(x)N(x) (6) A(x1) N(f(x1)) (7) N(f(a)) (8) W(a，f(a)) (9) A(a) (10) 口
(4)消去存在量词(按Skolem标准形) 原式z(P(a)(A(z)(B(f(z))W(z，f(z)))))
例 (p47)
(5)消去全称量词(直接去掉) 原式 P(a)(A(z)(B(f(z))W(z，f(z))))
(6)利用分配律化为合取范式原式 P(a)(A(z)B(f(z))) (A(z)W(z，f(z)))
例 (p47, 求子句)
(1) x(A(x)y(B(y)W(x，y))) = x(A(x) y(B(y)W(x，y))) = x y (A(x) (B(y)W(x，y))) x (A(x) (B(f(x))W(x，f(x)))) A(x) (B(f(x))W(x，f(x))) = (A(x) B(f(x))) (A(x) W(x，f(x))) 得到子句：
4.3.2 归结反演系统
一、谓词演算公式子句的形成二、一般归结三、归结反演算系统的应用
一、谓词演算公式子句的形成
一般步骤: (1)消去蕴含词和等价词 (2)否定深入 (3)约束变元改名 (4)化为前束范式 (5)消去存在量词(按Skolem标准形) (6)消去全称量词(直接去掉) (7)化为合取范式 (8)消去合取词得子句集， (9)改变变量的名称 (变量符号不重复使用)
4.3 谓词演算的归结推理系统
问题：从公式集S出发，证明目标公式T。
在归结系统中: 首先否定目标公式，然后将这个公式加到公式集S中，再将该公式化成子句集，若能归结成空子句(用□表示)，则认为证明了该公式T。
引例(p45)
设有语句串及它的符号表示如下： (1)无论谁能读就有知识；x(R(x) L(x)) (2)所有的海豚均没有知识；x(H(x) L(x)) (3)有些海豚有智慧。x(H(x)I(x))
(7)消去合取词得子句集此时公式中只含有一些文字的析取 P(a), A(z)B(f(z)), A(z)W(z，f(z))
(8)改变变量的名称：改名使得每个变量符号不出现在一个以上的子句中 P(a), A(z1)B(f(z1)), A(z2)W(z2，f(z2))
二、一般归结
只需寻找一个置换，把它们作用到母体子句上使它们含有互补的文字对(如P和P) 。
例 (p47)已知知识：
(1)每个作家均写过作品； (2)有些作家没写过小说；结论：有些作品不是小说。
证明：令 A(e)表示“e为作家”； B(e)表示“e为作品”； N(e)表示“e为小说”； W(e1，e2)表示“e1 写了 e2”
知识可以符号化如下： (1) x(A(x)y(B(y)W(x，y))) (2) x(A(x)y(N(y)W(x，y)))

离散数学第四章谓词演算的推理理论-归结推理系统共51页文档

合集下载