Presentation is loading. Please wait.

Presentation is loading. Please wait.

第5章 谓词逻辑的等值和推理演算 谓词逻辑研究的对象是重要的逻辑规律,普遍有效式是最重要的逻辑规律,而等值式、推理式都是普遍有效的谓词公式,因此等值和推理演算就成了谓词逻辑的基本内容. 这章的讨论,主要是以语义的观点进行的非形式的描述,而严格的形式化的讨论见第6章所建立的公理系统.

Similar presentations


Presentation on theme: "第5章 谓词逻辑的等值和推理演算 谓词逻辑研究的对象是重要的逻辑规律,普遍有效式是最重要的逻辑规律,而等值式、推理式都是普遍有效的谓词公式,因此等值和推理演算就成了谓词逻辑的基本内容. 这章的讨论,主要是以语义的观点进行的非形式的描述,而严格的形式化的讨论见第6章所建立的公理系统."— Presentation transcript:

1 第5章 谓词逻辑的等值和推理演算 谓词逻辑研究的对象是重要的逻辑规律,普遍有效式是最重要的逻辑规律,而等值式、推理式都是普遍有效的谓词公式,因此等值和推理演算就成了谓词逻辑的基本内容. 这章的讨论,主要是以语义的观点进行的非形式的描述,而严格的形式化的讨论见第6章所建立的公理系统.

2 5.1 否定型等值式 等值:若给定了两个谓词公式A,B,说A和B是等值的,如果在公式A,B的任一解释(注意在谓词逻辑中,解释的范围还包含论域以外的其他要素,见P65)下,A和B都有相同的真值. 其他说法:A,B等值当且仅当A↔B是普遍有效的公式(注意这里不再说重言式了).记作A=B或AB。

3 5.1.1 由命题公式移植来的等值式 若将命题公式的等值式,直接以谓词公式代入命题变项便可得谓词等值式.由
5.1.1 由命题公式移植来的等值式 若将命题公式的等值式,直接以谓词公式代入命题变项便可得谓词等值式.由 ﹁﹁p=p,p→q=﹁p∨q, (p∧q)∨r=(p∨r)∧(q∨r) 可得(以下每两个为一对:无量词、有量词) ﹁﹁P(x)=P(x) ﹁﹁(x)P(x)=(x)P(x) P(x)→Q(x)=﹁P(x)∨Q(x) (x)P(x)→(x)Q(x)=﹁ (x)P(x)∨(x)Q(x) (P(x)∧Q(x))∨R(x)=(P(x)∨R(x))∧(Q(x)∨R(x)) ((x)P(x)∧Q(y))∨(z)R(z) =((x)P(x)∨(z)R(z))∧(Q(y)∨(z)R(z))

4 5.1.2 否定型等值式 (摩根律的推广) ﹁(x)P(x)=(x)﹁P(x) ﹁(x)P(x)=(x)﹁P(x)
5.1.2 否定型等值式 (摩根律的推广) ﹁(x)P(x)=(x)﹁P(x) ﹁(x)P(x)=(x)﹁P(x) 形式上看这对公式,是说否定词”﹁”可越过量词深入到量词的辖域内,但要把所越过的量词转换为,转换为.

5 (1)从语义上说明 (2)例:在{l,2}域上分析
﹁(x)P(x)=﹁(P(1)P(2))=﹁P(1)v﹁P(2) =(x) ﹁P(x) ﹁(x)P(x)=﹁(P(1)vP(2))=﹁P(1)  ﹁P(2) =(x)﹁P(x)

6 (3)语义上的证明 证明方法:依等值式定义,A=B如果在任一解释I下A真B就真,而且B真A就真.
若证明﹁(x)P(x)=(x)﹁P(x) 1. 设某一解释I下若﹁(x)P(x)=T 从而(x)P(x)=F,即有一个xoD,使P(Xo)=F 于是﹁P(xo)=T 故在I下(x)﹁P(x)=T 2. 反过来,设某一解释I下若 (x) ﹁P(x)=T 即有一个xoD,使﹁P(Xo)=T 从而P(Xo)=F 于是(x) P(x)=F 即﹁ (x)P(x)=T

7 (4)举例 例1 “并非所有的动物都是猫”的表示 设 A(x):x是动物 B(x):x是描 原语句可表示成﹁(x)(A(x)B(x))
例1 “并非所有的动物都是猫”的表示 设 A(x):x是动物 B(x):x是描 原语句可表示成﹁(x)(A(x)B(x)) 依否定型公式得

8 例2 “天下乌鸦—般黑”的表示 设 F(x):x是乌鸦 G(x,y):x与y是一般黑 原语句可表示成 (x)(y)(F(x)^F(y) →G(x,y)) 不难知道与之等值的公式是 ﹁(x)(y)(F(x)^F(y)^﹁G(x,y)) 即不存在x,y是乌鸦但不一般黑.这两句话含义是相同的.经计算有

9

10 5.2 量词分配等值式 一、含单独的命题变项,与x无关 5.2.1 量词对、的分配律
这是一组量词对、的分配律,其中q是命题变项,与个体变元x无关,这是很重要的条件. 我们仅对第一个等式给出证明,其余三个同样可证.

11 设在一解释I下,(x)(P(x)q)=T,从而对任一x D ,有P(x)q=T
若q=T,则(x)P(x)q=T 若q=F,从而对任一x D ,有P(x) =T ,即有(x)P(x)=T,故仍有,(x)P(x)q=T 反过来,设在一解释I下,(x)P(x)q=T,若q=T,则(x)(P(x)q)=T 若q=F,必有(x)P(x)=T,从而对任一xD有P(x)=T,于是对任一x D有P(x)q=T故(x)(P(x)q)=T.

12 5.2.2 量词对→的分配律 这是一组量词对→的分配律,其中p,q是命题变项,与个体变元x无关,这是很重要的条件.
5.2.2 量词对→的分配律 这是一组量词对→的分配律,其中p,q是命题变项,与个体变元x无关,这是很重要的条件. 5.2节介绍的等值公式中仅有这里的第一、二个公式有量词的改变!!

13 先证明其中的第一个等式. 依5.2.1的等值式 依5.l.2的等值式

14 再证明其中的第三个等式 依5.2.l的等值式 其余两个等值式同样可证.

15 二、辖域中无单独的命题变项 5.2.3 量词对 、量词对V的分配律
这是当P(x),Q(x)都含有个体变元x时,量词对^,量词对V所遵从的分配律.然而对V,对^的分配律一般并不成立.证明中使用了5.2.1中的解释方法。 (x)P(x)v(x)Q(x)=>(x)(P(x)vQ(x)) (x)(P(x)^Q(x))=>(x)P(x)^(x)Q(x)

16 一些例子

17 5.2.4 变元易名后的分配律 (在求前束范式时有很大作用)
5.2.4 变元易名后的分配律 (在求前束范式时有很大作用) 这两个等值式,说明了通过变元的易名,仍可实现对V,对^的分配律. 证明是容易的.首先有变元易名等值式 (x)P(x)= (y)P(y) (x)P(x)= (y)P(y) 于是(x)P(x)v(x)Q(x)=(x)P(x)v(y)Q(y)

18 对x而言(y)Q(y)相当于命题变项,与x无关,可推得
(x)P(x)v(y)Q(y)=(x)(P(x)v(y)Q(y)) 对y而言,P(x)相当于命题变项与y无关,又可推得 (x)(P(x)v(y)Q(y))=(x)(y)(P(x)vQ(y)) 同理(x)(y)(P(x)^Q(y))=(x)P(x)^(x)Q(x) 然而(x)(y)(P(x)vQ(y))与(x)(P(x)vQ(x)) 是不等值的(x)(y)(P(x)^Q(y))与(x)(P(x)^Q(x)) 也是不等值的

19 5.3 范 式 在命题逻辑里.每一公式都有与之等值的范式,范式是一种统一的表达形式.
5.3 范 式 在命题逻辑里.每一公式都有与之等值的范式,范式是一种统一的表达形式. 对谓词逻辑的公式来说也有范式,其中前束范式与原公式是等值的,而其他范式与原公式只有较弱的关系。

20 5.3.1 前束范式 定理5.3.1 谓词逻辑的任一公式都可化为与之等值的前束范式.但其前束范式并不唯一.
5.3.1 前束范式 定义5.3.1 说公式A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词)且这些量词的辖域都延伸到公式的末端,前束范式A的一般形式为 (Q1x1)…(Qnxn)M(xl,…,xn) 其中Qi为量词或(i=l,…,n),M称作公式A的母式(基式),M中不再有量词. 定理5.3.1 谓词逻辑的任一公式都可化为与之等值的前束范式.但其前束范式并不唯一.

21

22 经过这几步,便可求得任一公式的前束范式.由于每一步变换都保持着等值性,所以,所得到的前束形与原公式是等值的.
这里的S(a,b,x,y,z)便是原公式的母式.其中a,b为自由个体变项。 由于前束中量词的次序排列,以及对母式都没有明确的限制,自然前束范式不是唯一的,如例1的前束范式也可以是 (x)(z)(y)(S(a,b,x,y,z)P) 其中P可以是任一不含量词的普遍有效的公式。

23 5.3.2 Skolem标准形 前束范式对前束量词没有次序要求,也没有其他要求.如果对前束范式进而要求所有存在量词都在全称量词之左得到存在前束范式(略),或是只保留全称量词而消去存在量词得到Skolem标准形。不难想像,仍保持与原公式的等值性就不可能了,只能保持在某种意义下的等值关系.

24 (1) 前束范式(略) 一个公式的前束范式为 (x1)…(xi)(xi+1)…(xn )M(x1,…,xn) 即存在量词都在全称量词的左边,且可保持至少有一个存在量词(i≥1),其中M(x1,…,xn)中不再含有量词也无自由个体变项 定理 谓词逻辑的任一公式A,都可化成相应的前束范式,并且A是普遍有效的当且仅当其前束范式是普遍有效的。 这定理是说对普遍有效的公式,它与其前束范式是等值的,而一般的公式与其前束范式并不是等值的.自然仅当A是普遍有效的,方使用前束范式.

25 例2 求( x)( y)( u)P(x,y,u)的前束范式(P中无量词).
将一公式化成前束形,首先要求出前束形,再做前束,这个例子已是前束形了,便可直接求前束形.

26 首先将全称量词( y)改写成存在量词( y),其次是引入谓词S和一个变元z,得S(x,z),建立公式
( x)((y)(u)(P(x,y,u)^﹁S(x,y))V(z)S(x,z)) 其中﹁S(x,y)的变元,是(y)的变元y和(y)左边存在量词( x)的变元x, 附加的(z)S(x,z)中的变元z是新引入的未在原公式中出现过的个体,S也是不曾在M中出现过的谓词. 进而将(z)左移(等值演算),便得前束范式 ( x)(y)(u)(z)((P(x,y,u)^﹁S(x,y))VS(x,z)). 当原公式中,有多个全称量词在存在量词的左边,可按这办法将全称量词逐一地右移. 前束范式仅在普遍有效的意义下与原公式等值. 前束形对谓词逻辑完备性的证明是重要的.

27 改写前=>改写后:简单 改写后=>改写前:反证 若A=( x)( y)( u)P(x,y,u)不是普遍有效,则存在解释I使A为F,于是 ( x)( y)( u)P(x,y,u)为F. 因此在解释I下,改写后B= ( x)(z)S(x,z)可为F,因为S是谓词变元。

28 (2) Skolem标准形 另一种Skolem标准形是仅保留全称量词的前束形.
定理 谓词逻辑的任一公式A,都可化成相应的Skolem标准形(只保留全称量词的前束形),并且A是不可满足的当且仅当其Skolem标准形是不可满足的. 这定理是说对不可满足的公式,它与其Skolem标准形是等值的,而一般的公式与其Skolem标准形并不是等值的.自然仅当A是不可满足的方使用Skolem标准形.

29 (x)(y)(z)(u)(v)(w)P(x,y,z,u,v,w) 的Skolem标准形.
例3 求公式 (x)(y)(z)(u)(v)(w)P(x,y,z,u,v,w) 的Skolem标准形. 将一公式化成Skolem标准形,首先也要求出前束形.这个例子已是前束形了,便可直接求Skolem标准形了. 首先将最左边的(x)消去,而将谓词P中出现的所有变元x均以论域中的某个常项a(a未在P中出现过,且不知道a具体是哪个常量)代入。

30 进而消去从左边数第二个存在量词(u),因(u)的左边有全称量词(y)(z),需将谓词P中出现的所有变元u均以y,z的某个二元函数f(y,z) (f未在P中出现过,且不知道f具体是哪个函数)代入. 最后按同样的方法消去存在量词(w),因(w)的左边有全称量词(y)(z)和(v),需将谓词P中出现的所有变元w均以y,z,v的某个三元函数g(y,z,v)(g未在P中出现过也不同于f)代入. 这样便得消去全部存在量词的Skolem标准形 (y)(z)(v)P(a,y,z,f(y,z),v,g(y,z,v)).

31 5.4 基本的推理公式 命题逻辑中有关推理形式、重言蕴涵以及基本的推理公式的讨论和所用的术语,都可引入到谓词逻辑中.并可把命题逻辑的推理作为谓词逻辑推理的一个部分来看待. 这里所介绍的是谓词逻辑所特有的,在命题逻辑里不能讨论的推理形式和基本的推理公式。

32 5.4 .1 推理形式举例 例1 所有的整数都是有理数,所有的有理数都是实数,所以所有的整数都是实数.
5.4 .1 推理形式举例 例1 所有的整数都是有理数,所有的有理数都是实数,所以所有的整数都是实数. 引入谓词将这三句话形式化,可得如下推理形式: (x)(P(x)→Q(x))(x)(Q(x)→R(x)) →(x)(P(x)→R(x))

33 例2 所有的人都是要死的,孔子是人,所以孔子是要死的,引入谓词将这三句话形式化,可得如下推理形式:
(x)(A(x)→B(x))A(孔子)→B(孔子).

34 例3 有一个又高又胖的人,必有一个高个子而且有—个胖子。
引入谓词将这两句话形式化,可得如下推理形式: (x)(C(x)D(x))→(x)C(x)(x)D(x).

35 例4 若某一个体a具有性质E,那么所有的个体x都具有性质E.
这两句话形式化,可得如下推理形式: E(a)→(x)E(x) 不难看出,由例1,2,3所建立的推理形式是正确的,而例4的推理形式是不正确的

36 5.4.2 基本的量词推理公式 (x)P(x)V(x)Q(x)=>(x)(P(x)VQ(x)) 量词分配律p73
基本的量词推理公式 (x)P(x)V(x)Q(x)=>(x)(P(x)VQ(x)) 量词分配律p73 (x)(P(x)Q(x))=>(x)P(x) (x)Q(x) 注意(1)的逆否,例3 (x)(P(x)→Q(x))=>(x)P(x)→(x)Q(x) 5.2.2的推广 (x)(P(x)→Q(x))=>(x)P(x)→(x)Q(x) (5) (x)(P(x)Q(x) )=>(x)P(x) (x)Q(x) (3)的推广 (6) (x)(P(x)  Q(x))=>(x)P(x) (x)Q(x) (4)的推广

37 (7) (x)(P(x)→Q(x))  (x)(Q(x)→R(x))=>
(x)(P(x)→R(x)) 例1 (8) (x)(P(x)→Q(x))  P(a)=>Q(a) 例2 (x)(y)P(x,y)=>(x)(y)P(x,y) 易理解 (x)(y)P(x,y)=>(y)(x)P(x,y) 易理解,注意右边x是y的函数 这些推理公式或称推理定理的逆一般是不成立的,所以正确地理解这些定理的前提与结论的不同是重要的。

38 5.5 推理演算 命题逻辑中引入推理规则的推理演算,可推广到谓词逻辑,有关的推理规则都可直接移入到谓词逻辑,除此之外还需介绍4条有关量词的消去和引入规则. (代入规则需补充说明:保持合式公式和普遍有效性不被破坏,见p58)

39 5.5.1 推理规则 (1)全称量词消去规则 (x)P(x)=>P(y) 注: 1其中y是论域中任意一个体.
5.5.1 推理规则 (1)全称量词消去规则 (x)P(x)=>P(y) 注: 1其中y是论域中任意一个体. 2需限制y不在P(x)中约束出现(右侧量不在左侧约束出现) . 如(x)P(x)=(x)((y)(x<y))在实数上成立,不应有(x)P(x)=>P(y)因P(y)会有问题.

40 (2)全称量词引入规则 P(y) =>(x)P(x) 注: 1任一个体y(自由变项)都具有性质P
2仍需限制x不在P(y)中约束出现(右侧量不在左侧约束出现) .如P(y)=(x)(x>y)时,P(x)会有问题

41 (3)存在量词消去规则 (x)P(x)=>P(c) 注 1. c是论域中使P为真的某个个体常项.
. 还需限制P(x)中不含有c (右侧量不在左侧出现) .如在实数域上(x)P(x)=(x)(c<x)时,P(c)会出问题. 思考方式:先定P再定c最后讨论(x)P(x)=>P(c)的正确性

42 (4)存在量词引入规则 P(c)=>(x)P(x) 注: 1. c是论域中使P为真的一个特定个体常项.
2. 需限制x不出现在P(c)中(右侧量不在左侧出现) .如实数域上, P(c)=( x)(x>c)时,P(x)会出问题.

43 这4条推理规则是基本的,对多个量词下的量词消去与引入规则的使用也已谈到.再明确说明一下.
(x)(y)P(x,y)=>(y)P(x,y) 的右端,不允许写成(y)P(y,y), (x)P(x,c)=>(y)(x)P(x,y) 的右端不允许写成(x)(x)P(x,x)。

44 (x)(y)P(x,y)=>(y)P(x,y)=>P(x,a)
但不允许再推演出(x)P(x,a)和(y)(x)P(x,y).原因是(x)(y)P(x,y)成立时,所找到的y是依赖于x的,从而P(x,y)的成立是有条件的,不是对所有的x对同一个a都有P(x,a)成立,于是不能再推演出(y)(x)P(x,y).

45 5.5.2 使用推理规则的推理演算举例 和命题逻辑相比,在谓词逻辑里使用推理规则进行推理演算同样是方便的,然而在谓词逻辑里,真值表法不能使用,又不存在判明A→B是普遍有效的一般方法,从而使用推理规则的推理方法已是谓词逻辑的基本推理演算方法. 推理演算过程.首先是将以自然语句表示的推理问题引入谓词形式化,若不能直接使用基本的推理公式便消去量词,在无量词下使用规则和公式推理,最后再引入量词以求得结论.

46 例1 前提 (x)(P(x)→Q(x)),(x)(Q(x)→R(x))
结论 (x)(P(x)→R(x)) 证明 (1)(x)(P(x)→Q(x)) 前提 (2)P(x)→Q(x) 全称量词消去 (3)(x)(Q(x)→R(x)) 前提 (4)Q(x)→R(x) 全称量词消去 (5)P(x)→R(x) (2),(4)三段论 (6)(x)(P(x)→R(x)) 全称量词引入

47 例2 所有的人都是要死的,苏格拉底是人,所以苏格拉底是要死的.
首先引入谓词形式化,令P(x)表x是人,Q(x)表x是要死的,于是问题可描述为 (x)(P(x)→Q(x))^P(苏格拉底)→Q(苏格拉底) 证明 (1)(x)(P(x)→Q(x)) 前提 (2)P(苏格拉底)→Q(苏格拉底) 全称量词消去 (3)P(苏格拉底) 前提 (4)Q(苏格拉底) (2)(3)分离规则

48 例3 前提(x)P(x)→(x)((P(x)VQ(x))→R(x)),(x)P(x)
结论(x)(y)(R(x)^R(y)) 证明 (1)(x)P(x)→(x)((P(x)VQ(x))→R(x)) 前提 (2)(x)P(x) 前提 (3)(x)((P(x)VQ(x))→R(x)) (1),(2)分离 (4)P(c) (2)存在量词消去 (5)P(c)VQ(c)→R(c) (3)全称量词消去 (6)P(c)VQ(c) (4) (7)R(c) (5),(6)分离 (8)(x)R(x) (7)存在量词引入 (9)(y)R(y) (7)存在量词引入 (10)(x)R(x)^(y)R(y) (8),(9) (11)(x)(y)(R(x)^R(y)) (10)置换

49 例4(不正确) 分析下述推理的正确性 (1)(x)(y)(x>y) 前提 (2)(y)(z>y) 全称量词消去,y与z有关 (3)z>b 存在量词消去,b依赖z (4)(z)(z>b) 全称量词引入,b不依赖z (5)b>b 全称量词消去 (6)(x)(x>x) 全称量词引入 推理(1)到(2),应明确指出y是依赖于x的,即(2)中y和z有关.(2)到(3),其中的b是依赖于z的.从而(3)到(4)是不成立的.又由于b是常项,(5)到(6)也是不允许的,因个体常项不能用全称量词量化.

50 5.6 谓词逻辑的归结推理法 归结方法可推广到谓词逻辑,困难在于出现了量词,变元.证明过程同命题逻辑,只不过每一步骤都要考虑到有变元,从而带来复杂性. 使用推理规则的推理演算过于灵活,技巧性强,而归结法较为机械,容易使用计算机来实现。

51 5.6.1 谓词逻辑归结证明过程四步骤 (从例子来理解步骤)
谓词逻辑归结证明过程四步骤 (从例子来理解步骤) (1)为证明A→B是定理(A,B为谓词公式),即AB, 等价的是证明G=AB是矛盾式,这是归结法的出发点(反证法). (2)通过G的合取形式建立子句集S,在建立子句集S的时.利用前束范式及Skolem标准形(不严格),消去存在量词(以常项代替如a),消去全称量词(注意新的自由变元如x,y)。 理论:S中的前提与G在不可满足的意义下是一致的。

52 (3)对S作归结: (P(x)Q(x))并且(﹁P(a)R(y))可以归结出 Q(a) R(y) 理论:因为(P(a)Q(a) )(﹁P(a)R(y))Q(a)R(y) 理论:变元x统一换成特定个体a称为合一置换{x/a} (4)重复归结方法,最后得到矛盾.

53 5.6.2 归结法证明举例 例1 (x)(P(x)→Q(x))^(x)(Q(x)→R(x))=>(x)(P(x)→R(x))
5.6.2 归结法证明举例 例1 (x)(P(x)→Q(x))^(x)(Q(x)→R(x))=>(x)(P(x)→R(x)) 首先写出公式G G=(x)(P(x)→Q(x))^(x)(Q(x)→R(x))^﹁ (x)(P(x)→R(x)) 为求G的子句集S,可分别对(x)(P(x)→Q(x)),(x)(Q(x)→R(x)),﹁ (x)(P(x)→R(x))作子句集,然后求并集来作为G的“子句集”(这个“子句集”不一定是S,但与S同时是不可满足的,而且较S来得简单,于是为方便可将这个“子句集”视作S). (x)(P(x)→Q(x))的子句集为{﹁P(x)VQ(x)) (x)(Q(x)→R(x))的子句集为{﹁Q(x)VR(x)} ﹁ ( x)(P(x)→R(x))=(x) ﹁(﹁P(x)VR(x))=(x)(P(x)^﹁R(x)) Skolem化,得子句集{P(a),﹁R(a)} 于是G的子句集S={﹁P(x)VQ(x),﹁Q(x)VR(x),P(a),﹁R(a)}

54 证明S是不可满足的,有归结过程: (1) ﹁P(x)VQ(x) (2) ﹁Q(x)VR(x) (3) P(a) (4) ﹁R(a) (5) Q(a) (1)(3)归结 (6) R(a) (2)(5)归结 (7) 口 (4)(6)归结

55 例2 A1=(x)(P(x)^(y)(D(y)→L(x,y)))
A2=(x)(P(x)→(y)(Q(y)→﹁L(x,y))) B=(x)(D(x)→﹁Q(x)) 求证A1^A2=>B. 证明 不难建立A1的子句集为{P(a),﹁D(y)VL(a,y)},A2的子句集为{﹁P(x)V﹁Q(y)V﹁L(x,y)}, ﹁B的子句集为{D(b),Q(b)},求并集得子句集S,进而建立归结过程:

56 (1) P(a) (2) ﹁D(y)VL(a,y) (3) ﹁P(x)V﹁Q(y)V﹁L(x,y) (4) D(b) (5) Q(b) (6) L(a,b) (2)(4)归结 (7) ﹁Q(y)V﹁L(a,y) (1)(3)归结 (8) ﹁L(a,b) (5)(7)归结 (9) 口 (6)(8)归结


Download ppt "第5章 谓词逻辑的等值和推理演算 谓词逻辑研究的对象是重要的逻辑规律,普遍有效式是最重要的逻辑规律,而等值式、推理式都是普遍有效的谓词公式,因此等值和推理演算就成了谓词逻辑的基本内容. 这章的讨论,主要是以语义的观点进行的非形式的描述,而严格的形式化的讨论见第6章所建立的公理系统."

Similar presentations


Ads by Google