4第四章-一阶谓词逻辑

上传人:壹****1 文档编号:569180222 上传时间:2024-07-28 格式:PPT 页数:67 大小:231KB
返回 下载 相关 举报
4第四章-一阶谓词逻辑_第1页
第1页 / 共67页
4第四章-一阶谓词逻辑_第2页
第2页 / 共67页
4第四章-一阶谓词逻辑_第3页
第3页 / 共67页
4第四章-一阶谓词逻辑_第4页
第4页 / 共67页
4第四章-一阶谓词逻辑_第5页
第5页 / 共67页
点击查看更多>>
资源描述

《4第四章-一阶谓词逻辑》由会员分享,可在线阅读,更多相关《4第四章-一阶谓词逻辑(67页珍藏版)》请在金锄头文库上搜索。

1、第四章 一阶谓词逻辑有些推理的有效性不能用命题逻辑和词项逻辑所讲的方法判定: (1)白马是马(p) 所以,骑白马是骑马(q)pq (不是重言式,在p=1,q=0, 的赋值值为假) (2) 2是小于3的 3是小于4的 所以,2是小于4的没有相同的中项(小于3的;3),前提和结论之间建立不起任何的关系但实际上(1)和(2)的推理都是有效的。命题逻辑和词项逻辑有局限性。命题逻辑和词项逻辑的局限性:1. 都不能处理关系命题及其推理;2. 都不能处理量词内部含联结词结构的命题及其推理。需要用另外的逻辑理论谓词逻辑谓词逻辑。一阶谓词逻辑语言一阶谓词逻辑公式公式赋值/语义普遍有效式逻辑推论形式推演前束范式专

2、名、 常项及其指称专名是用来指称、指向或命名某个东西的表达式。“长江”“黄河”“美国的首都常项就是有所指的专名。变项: x y z 变项的作用在于它在某个范围内可以取不同的值。变项的作用在于它在某个范围内可以取不同的值。例如:例如: 我们令下列城市为我们令下列城市为x的取值范围:的取值范围:西安、南京、荆州、襄阳、平遥西安、南京、荆州、襄阳、平遥x的城墙的城墙论域,有时也称个体域,是讨论中涉及的所有个体对象的集合。函数和函数符号函数是一种映射或指派关系。设A是前面列出的所有城市的集合,B是所有这些城市的现有的城墙的集合。那么f可以是这样一个函数,它把A中的每一个城市映射到B中该城市的城墙。于是

3、,f(西安)西安的城墙.在我们的讨论中,也可以有函数符号,用f, g, h来表示。函数符号的定义域和值域都是论域。项项类似于自然语言中的名词或名词词组,包括所有的个体常项和个体变项,并且包括用函数符号加上适当的常项或变项序列组成的符号串。例如:fx: x的父亲 a: 张山 fa: 张三的父亲这里的函数符号可以叠加,例如 gx: x的母亲张三的祖母?gfa第一节 一阶谓词逻辑语言个体词个体词就是表示对象域中的个体的符号,包括个体变项和个体常项。个体变项:某个特定的范围内的某个不确定的对象,用x,y,z个体常项:某个特定的范围内的某个确定的对象,用a,b,c来表示论域:由一定对象所组成的类或者集合

4、,规定了个体变项的取值范围,也叫做个体变项的“值域”。论域一般是全域。谓词:F、G、H、R1. 一元谓词(表示性质)F(x):自然数是整数F(a) :3是整数G(b) 春江花月夜是中国古代名曲2. n元谓词(表示n元关系)H(c,d):牛郎爱织女F(y,e):张三比李四跑的快。 谓词:F、G、H、R词典我们可以用下面方式直观表明:形式语言中的个体常项、函数符号和谓词等表示个体、函数、性质及关系 论域: 自然数集合 Px:x是素数 a:0 Rxy: xy fx:x+1当我们对汉语的句子做符号化或形式翻译时候,类似上述表格被称为“词典”量词全称量词:(所有、任何、一切)x F(x):对于所有的x,

5、x是F特称量词: (存在、有些、有一个)x F(x):存在x使得x是F联结词:,辅助符号: (),量词的辖域量词的辖域量词的辖域是它后面第一个完整的公式。个体变项的自由出现和约束出现个体变项的自由出现和约束出现设x为一个个体变项,是任意公式,x在中的一个出现是约束的(bound),当且仅当这一出现或是在中的某个使用x的量词中,或者在这样的量词的辖域内。x在中的一个出现是自由的(free)当且仅当这一出现既不是在中出现的任何量词中,也不是在他们的辖域内。开公式开公式一个含有至少一个自由变项的公式,叫做“开公式”。闭公式闭公式如果一个公式中所有个体变项的出现是约束出现,那么我们就把该公示称为闭公式

6、或句子。特别的,没有任何个体变项出现的公式都是闭公式。G(a)在给定论域之后,闭公式有确定的意义。直言句及其符号化直言句及其符号化1.无量词的句子例:用给出的词典将下列句子符号化:论域: 现有的人 a: 张三Px: x是成年人 b: 李四Rxy: x比y 年长 c: 王五如果李四是成年人并且没有王五年长,那么王五也是成年人。 虽然张三不是成年人,但他还是比李四和王五年长。2.自然语言中性质命题的符号化1. SAP 符号化为: x(S(x) P(x)2. SEP符号化为: x(S(x) P(x) x(S(x) P(x) x(S(x) P(x)3. SIP符号化为: x(S(x) P(x)4. S

7、OP符号化为: x(S(x) P(x)5. 单称直言命题符号化: 原子公式“春江花月夜是一只中国古典名曲”F(a) 所有的鱼都生活在水中没有猫生活在水中有些生活在水中的是鱼有些生活在水中的不是鱼论域:所有生物 Gx: x生活在水里 Fx: x是鱼 Hx: x是猫自然语言中关系命题符号化论域:所有生物 Lxy: x帮助yPx: x是人 b:张三所有人都帮助张三。没有人帮助张三。有些人帮助张三。有些人没有帮助张三。张三帮助每一个人。张三没帮助任何人。论域:所有的人 Px: x是学生 b: 张三 Lxy: x帮助y Rxy:与y住同一个宿舍与张三同宿舍的学生都帮助张三与张三同宿舍的学生没人帮助张三。

8、张三帮助他同宿舍的每一个学生。与张三同宿舍的某些学生没有帮助张三。更进一步论域:所有的人 Px: x是学生 b: 张三 Lxy: x帮助 yRxy: x与y住同一个宿舍1.与张三同宿舍的学生都帮助张三。2. 与张三同宿舍的学生中没人帮助张三。3. 与张三同宿舍的某些学生帮助张三。4. 与张三同宿舍的某些学生没帮助张三。5. 张三帮助他同宿舍的每一个学生。6. 张三帮助他同宿舍的某些学生。更进一步论域: 所有人 Qx: x是文科专业的 Sx: x是学生 Fx: x学理科知识Px: x聪明 Gx: x学文科知识1. 聪明的文科生都既学文又学理。2. 有些聪明的文科生既学文又学理。3. 没有哪个聪明

9、的文科生是既学文又学理。4. 有些聪明的文科生没有既学文又学理。关于“和”的处理论域: 所有动物 Cx: x是猪Ax: x是哺乳动物 Dx: x是狗Bx:是鸟Fx:x是鱼1.猫和狗都是哺乳动物。2.鸟和鱼都不是哺乳动物。 嵌入量词的句子的形式化 嵌入量词是指出现在某个量词辖域中的量词。论域:所有的动物 Px: x是人Lxy:x爱y 1. 每个人都爱所有的人2. 没有人爱所有的人。 3. 有些人爱所有的人。 4. 每个人都爱某些人。论域: 所有的动物 Dx: x是狗Px: x是人 Rxy: x见过y Qx: x是家养动物 Lxy: x喜欢ySx: x是流浪动物 Bxy: x咬过y 1.见过流浪狗

10、的人喜欢所有家养的狗。 2. 有些见过家养狗的人不喜欢任何流浪狗。 3. 每个被狗咬过的人都不喜欢任何流浪狗。函数符号和等词的运用“是”至少有两种意思,一种是属于某类或有某性质,二是等于或相等。“张三是男人”。“张小三的父亲是张三”。用给出的词典将下列句子符号化 论域:所有的人 gx: x的母亲 a: 张三 Px:x 是女人 b: 李四 Lxy: x喜欢y fx: x的父亲 Tx:x是教师张三的祖母是教师。张三的祖母是李四的外祖母。张三的祖父不是李四的外祖父。 每个人的母亲都是女人。有些女士不喜欢自己的父亲。二元关系的逻辑性质1. 自返性 : 一关系R是自返的,当且仅当, 对任一 x而言,x与

11、它自身有R关系。即x R(x,x).2. 对称性:一关系R是对称的,当且仅当,对任一x和y而言,如果R(x,y),则R(y,x)3. 传递性:一关系R是传递的,当且仅当,对任一x,y和z 而言,如果R(x,y)且R(y,z), 则R(x,z)符号系统个体变项:x,y,z(自由/约束变元)个体常项:a,b,c谓词:F、G、H、R一元谓词(表示性质)二元谓词(表示关系)量词全称量词:特称量词:联结词:,辅助符号: (),真假值: “1”(或T), “0”(或F)项的形成规则形式语言L的项是如下递归定义的1. 常项符号是项;2. 变元符号是项; 3. 如果t1, t2, tn是项, f是任意n元函数

12、符号, 则f(t1, t2, tn也是项;4. 只有这些是项。 第二节 一阶谓词逻辑公式 公式形成规则对于任意n元谓词P和任意序列t1, t2, tn ,P(t1, t2, tn)是公式, 也称为原子公式;如果A是公式,则A是公式;如果A和B都是公式,则AB,AB,AB ,A B是公式;如果A是公式,则xA, xA是公式;只有按以上方式形成的符号串才是公式。xA为全称公式xA为存在公式辖域:如果xA或xA是B的段,则称A为在它左边的x或x在B中的辖域。量词的辖域不是公式公式xyzF(x,y,z),x的辖域是y zF(x,y,z), y的辖域是zF(x,y,z),z的辖域是F(x,y,z)约束变

13、元:如果处于量词x或x的辖域之内并且与量词所含变项相同,或作为与该量词一起出现的变项。否则称为自由变元。x(F(x) H(x),x为约束变元G(y)y (F(x) G(y), 第一个G(y)中的y是自由变元,y (F(x) G(y)中的x是自由变元,y是约束变元闭公式:不含自由变元符号的公式F(a,b), yF(a,y), xyF(x,y)是闭公式开公式:含至少一个自由变元符号的公式F(u,v), yF(u,y), xyF(x,y,w)闭公式意义确定,有确定的真值开公式的意义不确定,没有确定的真值FxF(x) yH(y)此公式是不是一阶谓词中的公式?不是,一阶谓词逻辑的变元指论域中的对象,而不

14、是谓词变元。只有在高阶逻辑中才允许使用谓词变元。高阶逻辑的引入是为了解决一阶逻辑不能表达/处理的命题。模型和赋值1. 一阶语言的一个模型M(解释)包括一下要素: (1)一个个体域D, 即由具有一定性质的个体所有构成的集合。 (2)个体常项在个体域D中的值, 即个体常项表示该个体域中的某个特定个体。(3)谓词符号在个体域D上的解释,即表示该个体域中个体的性质和个体之间的关系。D:自然数集合a:1F(x):x是偶数R(x,y):x小于yS(x,y,z):x乘y等于zF(a):1是偶数xyR(x,y):对于任一自然数,都可以找到另一个自然数,使得前者小于后者xS(x,a,x):任一自然数与1相乘都等

15、于该自然数本身yR(y,x):有的自然数小于10(给x指派10的值)yR(y,z):有的自然数小于5(给z指派5的值)一个模型M和模型M上的一个指派称为一个赋值,记为=。 从而一个公式A 在赋值下的的值(A)可以递归定义如下:1. (F(t1,tn)= T, iff, F2. (B)=T, iff, (B)=T3. (BC)=T, iff, (B)=T 且(C)=T 4. (B C)=T, iff, (B)=T 或(C)=T 5. (B C)=T, iff, (B)=F 或(C)=T 6. (B C)=T, iff, (B)=(C)=T 或(B)=(C)=F7. ( xB(x)=T,iff,

16、8. . ( xB(x)=TIff, 如果由B(x)构作B(u)(取u不在B(x)中出现并且u取代A(x)中的x)且对任何aD,A(u)(u/a)=1如果由B(x)构作B(u)(取u不在B(x)中出现并且u取代A(x)中的x)且存在aD,A(u)(u/a)=1A=F(g(a),g(b),g(c)D:自然数集合F(x,y,z):x加y等于zg(x):x的平方a=3,b=4,c=5A为32+42=52 A在此赋值下为真 a=3,b=6,c=5 A为32+62=52 A在此赋值下为假存在赋值可使A为真和为假B=F(u)F(u)任何赋值都使B为真第四节 普遍有效式(普遍)有效性A是有效的,当且仅当对于

17、(以任何不空集为论域的)任何赋值A=1有效公式是永真式可满足性A是可满足的,当且仅当存在(以某个不空集为论域的)赋值,使得A=1当A=1时,称此赋值满足A不可满足性A是非有效的,当且仅当对于(以任何不空集为论域的)任何赋值A=0不可满足公式是永假式注意有效公式相当于命题逻辑中的重言式,但它们之间有区别。可用算法(真值表法)判定命题逻辑中的公式是不是重言式。但若要判断谓词逻辑中的公式是否有效,须考虑所有不同大小的集合以及以它们为论域的所有指派。在无限论域D的情形,这个过程一般不是有限的。如我们没有方法在有限步内求出xA(x)或xA(x)的值,因为这要求先给出对应无限多个aD的A(x)的值普遍有效

18、式 :书P186普遍有效式的判定问题:书P187判定问题机器判定公式A是不是Theorem中的定理。存在一个算法T(机械可实现的)可判定:If A Theorem, 机器回答=YES else 机器回答= NO半可判定:If A Theorem, 机器回答=YES else 机器回答= ?不可判定:If A Theorem, 机器回答=? else 机器回答= ?“停机问题”:一个任给的图灵机对于一个任给的输入而言,是否停机不可判定一阶谓词逻辑的半可判定性可判定:存在算法判定公式的真值不可判定:不存在算法判定公式的真值半可判定:公式可满足,有算法可验证 公式不可满足,无算法可验证命题逻辑是可判

19、定的,判定算法的基本原理:穷尽每个命题变元的一切取值,分别计算各种取值下命题的真值这一原理不适合一阶谓词逻辑,因为对公式A来说,由于结构、指派是不能穷尽的,从而A所涉及的取值也是不可穷尽的。丘奇首先指出:“任何至少含有一个二元谓词的一阶谓词演算系统都是不可判定的。”一阶谓词逻辑是半可判定的,即存在一个可机械实现的过程,能对其定理做出肯定的判定,但对非定理的公式却未必能做出否定的判定例子:书P193-194例12、13、14、15练习:书可满足公式是相对于以特定的不空集为论域的特定赋值而是真的。公式在给以赋值之后就有了具体内容,可满足性刻划了由内容确定的命题的真的概念。有效公式的真是由它的形式结

20、构确定的,与其中的各种符号在赋值下产生的涵义没有关系,而注重命题的内容抽象出的逻辑形式第五节 逻辑推论是命题逻辑的公式集,A是公式集中一公式,A是的逻辑推论逻辑推论(即A是 中公式的逻辑推逻辑推论论), 记作 A,(读作逻辑蕴涵)当且仅当对于任何赋值, =1蕴涵A=1。注意:“”不是形式语言中的符号, A不是形式语言中的公式,而是关于和A的元语言中的命题。 A表示 A不成立,即存在真假赋值使=1并且A=0。是公式集,当是空集时,是 A,且A的真是无条件的,即A是有效公式。例xA(x) xA(x) 用反证法,设xA(x) xA(x) ,即存在以D为论域的赋值使得(1) xA(x)=1(2) xA

21、(x)=0由A(x)构作A(u),取u不在A(x)中出现。由(1)得,存在aD,使得(A(u)(u/a)=1,因此有(3)存在aD,使得A(u)(u/a)=0由(2)得xA(x)=1,和(3)矛盾证xA(x) xA(x)例xA(x) B(x) xA(x) xB(x)设xA(x) B(x) xA(x) xB(x),即有以D为论域的赋值,使得(1) xA(x)B(x)=1(2) xA(x)xB(x)=0 由(2)得(3) xA(x) =1(4) xB(x)=0由A(x)和B(x)分别构作A(u)和B(u),取不在A(x)和B(x)中出现。得(5)对于任何aD,A(u)B(u)(u/a)=1 由(1

22、) (6)对于任何aD,A(u)(u/a)=1由 由(3) (7)任何a D,B(u)(u/a)=0 由(5)(6)得对于任何aD, B(u)(u/a)=1 与(7)矛盾上面的两个例子都是证明逻辑推论,在证明中并不要构作赋值;若要否证逻辑推论,要在否证中构作赋值例xF(x) xG(x) xF(x) G(x)令D=a,b,由F(x)和G(x)分别构作F(u)和G(u)(u 不在F(x)和G(x)中出现),F(x)=a,G(x)=b或(1) F(u)(u/a)=1(2) F(u)(u/b)=0(3) G(u)(u/a)=0(4) G(u)(u/b)=1或0(5) xF(x) =0 由(2)(6)

23、xF(x) xG(x)=1 由(5)(7) F(u)G(u) (u/a)=0 由(1)(3)(8) xF(x) G(x)=0 由(7)由(6)(8)得 xF(x) xG(x) xF(x) G(x)xF(x) xG(x) xF(x) G(x)则有xF(x)xG(x)=1 ,xF(x)G(x)=0。此时若令D=a,(1) F(u)(u/a)=1(2) G(u)(u/a)=0(3) xF(x) =1 由(1) (4) xG(x)=0 由(2)(5) F(u)G(u) (u/a)=0 由(1)(2)(6) xF(x) xG(x)=0 由(3)(4)(7) xF(x) G(x)=0 由(5)(6)与前提

24、矛盾,不能令D=a来证明xF(x) xG(x) xF(x) G(x)第六节 形式推演一阶谓词逻辑推演规则包括了命题逻辑中的13条形式推演规则,增加量词规则(其中A,B,C为任何公式)(,-) 如果 xA(x) , 则 A(t) (消去) (,+) 如果 A(u) ,u不在中出现, 则 xA(x) (引入) (,-) 如果, A(u) B,u不在或B中出现, 则, xA(x) B ( 消去)(,+) 如果 A(t) 则 xA(x),其中A(x)是在A(t)中把t的某些(不一定全部)出现替换为x 而得 ( 引入) 形式可推演性A是在一阶谓词逻辑中由形式可推演形式可推演(或形式形式证明证明)的,记作

25、 A ,当且仅当 A 能由(有限次使用)一阶谓词逻辑的形式推演规则生成。定理1 x1xnA(x1,xn) A(t1,tn) A(t1,tn) x1 xnA(x1,xn),其中A(x1,xn)是在A(t1,tn) 中把ti的某些(不一定是全部)出现替换为xi而得(1in) xA(x)yA(y) xA(x)yA(y) xyA(x,y)yxA(x,y) xyA(x,y)yxA(x,y) xA(x) xA(x) xyA(x,y)yxA(x,y)证xA(x)yA(y)A(u) A(u) (取u不在A(y)中出现)A(u) yA(y) (,+) xA(x) yA(y) (,-) 同上定理2 xA(x)xA

26、(x) xA(x)xA(x) 选证xA(x)xA(x) A(u) xA(x) (取u不在A(x)中出现) xA(x) ,A(u) xA(x) (+)(ref) xA(x) A(u) ( ,) xA(x) xA(x) (,+) xA(x) ,xA(x) xA(x) (+)(ref) xA(x) xA(x) ( ,) xA(x) A(u) (取u不在A(x)中出现) A(u) xA(x) (如果AB,则B A) xA(x) xA(x) (,-) 定理3 xA(x) B(x) xA(x) xB(x) xA(x) B(x) xA(x) xB(x) xA(x) B(x) , xB(x) C(x) xA(

27、x) xC(x)AxB(x) xAB(x) x不在A中出现AxB(x) xAB(x) x不在A中出现xA(x)B xA(x)B x不在B中出现xA(x)B xA(x)B x不在B中出现定理4AxB(x) xAB(x) x不在A中出现AxB(x) xAB(x) x不在A中出现xA(x)xB(x) xA(x)B(x) xA(x)B(x) xA(x) xB(x) Q1xA(x)Q2yB(y) Q1xQ2y A(x)B(y) x不在B(y)中出现,y不在A(x)中出现定理5 A xB(x) xA B(x) x不在A中出现A xB(x) xA B(x) x不在A中出现xA(x) xB(x) xA(x)

28、B(x) xA(x) xB(x) xA(x) B(x) Q1xA(x) Q2yB(y) Q1xQ2y A(x) B(y) x不在B(y)中出现,y不在A(x)中出现定理6 xA(x)B(x) xA(x)xB(x)xA(x)B(x) xA(x)xB(x)xA(x)B(x) , xB(x)C(x) xA(x)xC(x)xA(x)B(x) xA(x) B(x)xA(x)B(x) xB(x) A(x)xA(x) B(x),xB(x) A(x) xA(x)B(x) 可靠性定理 A A 每个可证明的一阶逻辑句子是普遍有效的,就是在所有域上有效 完备性定理 A A )每个普遍有效的一阶公式是可证明的 一阶逻

29、辑是可靠和完备的例子书 P199例17、P203例18苏格拉底三段论:所有人都会死,苏格拉底是人,所以苏格拉底会死。H(x): x是人M(x):x会死a:苏格拉底xH(x) M(x) H(a) M(a)xH(x)M(x) ,H(a) xH(x)M(x) (ref)xH(x)M(x) ,H(a) H(a)M(a) (,-) xH(x)M(x) ,H(a) H(a) (ref) xH(x)M(x) ,H(a) M(a) ( ) 任何人违反交通规则,则要受到罚款,因此,如果没有罚款,则没有人违反交通规则。S(x,y):x违反yM(y):y是交通规则P(z):z是罚款R(x,z):x受到zxy(S(x

30、,y)M(y) z(P(z)R(x,z)zP(z)xy(S(x,y)M(y)xy(S(x,y)M(y) z(P(z)R(x,z)zP(z)xy(S(x,y)M(y)xy(S(x,y)M(y) z(P(z)R(x,z)y(S(b,y)M(y) z(P(z)R(b,z)xy(S(x,y)M(y) z(P(z)R(x,z), z(P(z) z(P(z) (+)(ref)xy(S(x,y)M(y) z(P(z)R(x,z), z(P(z) z(P(z) 定理2xy(S(x,y)M(y) z(P(z)R(x,z), z(P(z) (P(a)xy(S(x,y)M(y) z(P(z)R(x,z), z(P(

31、z) (P(a) R(b,a) ( ,+)xy(S(x,y)M(y) z(P(z)R(x,z), z(P(z) z (P(z) R(b,z) ) (,+)xy(S(x,y)M(y) z(P(z)R(x,z), z(P(z) z (P(z) R(b,z) ) 定理2xy(S(x,y)M(y) z(P(z)R(x,z), z(P(z) z(P(z)R(b,z) y(S(b,y)M(y) (如果AB,则B A)xy(S(x,y)M(y) z(P(z)R(x,z) , z(P(z) y(S(b,y)M(y) (,-) xy(S(x,y)M(y) z(P(z)R(x,z) , z(P(z) y(S(b,

32、y)M(y) 定理2xy(S(x,y)M(y) z(P(z)R(x,z) , z(P(z) y(S(b,y)M(y) xy(S(x,y)M(y) z(P(z)R(x,z) , z(P(z) xy(S(x,y)M(y) ( ,+) xy(S(x,y)M(y) z(P(z)R(x,z)zP(z)xy(S(x,y)M(y) (,+)课堂练习:书第七节 前束范式前束范式是一阶逻辑中的范式,在一阶逻辑中,公式可以变换为与它等值的前束范式称公式A为前束范式,当且仅当它有下面的形式 Q1x1QnxnB,其中的Q1,Qn是或,并且B不含量词。称Q1x1Qnxn为前束词;称B为母式xA(x) xB(x) xA(

33、x) B(x)xA(x) xB(x) xA(x) B(x)xA(x) xA(x) xA(x) xA(x)步骤:把公式中的和替换为、,并且使的辖域中不出现、,再根据等值公式,逐步把量词移到、的辖域之外,从而使量词放在公式的最前面。例xyF(u,x,y)xyG(y,w)H(x)xyF(u,x,y) xyG(y,w) H(x) xyF(u,x,y) xyG(y,w) H(x)xyF(u,x,y) xyG(y,w) H(x)xyF(u,x,y) xyG(y,w) H(x)xyF(u,x,y) yG(y,w) H(x)xyF(u,x,y) zG(z,w) H(x)xyzF(u,x,y) G(z,w) H(x)

展开阅读全文
相关资源
正为您匹配相似的精品文档
相关搜索

最新文档


当前位置:首页 > 建筑/环境 > 施工组织

电脑版 |金锄头文库版权所有
经营许可证:蜀ICP备13022795号 | 川公网安备 51140202000112号