版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
人工智能主讲:吴顺祥
教授模式识别与智能系统研究所Powerpoint中南大学智能系统与智能软件研究所第二章知识表示方法2.0引言2.1状态空间法2.2问题归约法2.3谓词逻辑法2.4语义网络法2.5其他方法2.6小结中南大学智能系统与智能软件研究所2.0引言信息科学有机体系的分支学科:信息获取(感知与表示)、信息传输(通信与存储)、信息处理(计算与认知)、信息再生(综合与决策)、信息执行(控制与显示)知识成为由信息到智能的中介。知识的表示方法主要分为结构化方法,包括逻辑方法和产生式方法非结构化方法,包括语义网络和框架等。3中南大学智能系统与智能软件研究所2.0引言:数据、信息与知识2.0.1知识和知识表示数据一般指单独的事实,是信息的载体。信息由符号组成,如文字和数字,但是对符号赋予了一定的意义,因此有一定的用途或价值。信息表示的是数据的含义。4中南大学智能系统与智能软件研究所2.0引言:数据、信息与知识知识是由经验总结升华出来的,因此知识是经验的结晶。知识在信息的基础上增加了上下文信息,提供了更多的意义,因此也就更加有用和有价值。知识是随着时间的变化而动态变化的,新的知识可以根据规则和已有的知识推导出来。因此知识反映了信息之间的内在关系或必然联系。5中南大学智能系统与智能软件研究所2.0引言:数据、信息与知识Feigenbaum认为知识是经过加工的信息,它包括事实、信念和启发式规则。Bernstein说知识是由特定领域的描述、关系和过程组成的。Hayes-Roth认为知识是事实、信念和启发式规则。从知识库观点看,知识是某论域中所涉及的各有关方面、状态的一种符号表示。6中南大学智能系统与智能软件研究所2.0引言:数据、信息与知识人工智能系统所关心的知识
事实:是关于对象和物体的知识。规则:是有关问题中与事物的行动、动作相联系的因果关系的知识。元知识:是有关知识的知识,是知识库中的高层知识。常识性知识:泛指普遍存在而且被普遍认识了的客观事实一类知识。7中南大学智能系统与智能软件研究所2.0引言:数据、信息与知识知识表示就是研究用机器表示上述这些知识的可行性、有效性的一般方法,可以看作是将知识符号化并输入到计算机的过程和方法。知识表示=数据结构+处理机制知识表示的观点:陈述性过程性8中南大学智能系统与智能软件研究所2.0引言:数据、信息与知识陈述性知识表示和过程性知识表示各有优缺点。(1)由于高级的智能行为似乎强烈地依赖于陈述性知识,因此AI的研究应注重陈述性的开发。(2)过程性知识的陈述化表示。(3)以适当方式将过程性知识和陈述性知识综合,可以提高智能系统的性能。9中南大学智能系统与智能软件研究所2.0引言:知识-策略-智能策略就是关于如何解决问题的政策方略,包括在什么时间、什么地点、由什么主体采取什么行动、达到什么目标、注意什么事项等等一整套完整而具体的行动计划规划、行动步骤、工作方式和工作方法。10中南大学智能系统与智能软件研究所2.0引言:知识-策略-智能“智能”应当理解为:在给定的问题-问题环境-主体目的的条件下,智能就是有针对性地获取问题-环境的信息,恰当地对这些信息进行处理以提炼知识达到认知,在此基础上,把已有的知识与主体的目的信息相结合,合理地产生解决问题的策略信息,并利用所得到的策略信息在给定的环境下成功地解决问题达到主体的目的。11中南大学智能系统与智能软件研究所2.0引言:知识-策略-智能4个要素包括信息知识策略行为4个能力包括获取有用信息的能力由信息生成知识(认知)的能力由知识和目的生成策略(决策)的能力实施策略取得效果(施效)的能力12中南大学智能系统与智能软件研究所2.0引言:知识-策略-智能信息、知识、智能之间的关系:信息是基本资源;知识是对信息进行加工所得到的抽象化产物;策略是由客体信息和主体目标演绎出来的智慧化身,智能是把信息资源加工成知识、进而把知识激活成解决问题的策略并在策略信息引导下具体解决问题的全部能力。信息、知识、智能关系,正好符合人类自身认识世界和优化世界活动过程中由信息生成知识、由知识激活智能的过程总结:信息经加工提炼而成知识,知识被目的激活而成智能。13中南大学智能系统与智能软件研究所2.0引言:智能中“信息-知识-策略”关系获取信息的功能由感觉器官完成,传递信息的功能由神经系统完成,处理信息和再生信息的功能由思维器官完成,施用信息的功能由效应器官完成。14中南大学智能系统与智能软件研究所2.0引言:AI对知识表示方法的要求(1)表示能力,要求能够正确、有效地将问题求解所需要的各类知识都表示出来。(2)可理解性,所表示的知识应易懂、易读。(3)便于知识的获取,使得智能系统能够渐进地增加知识,逐步进化。(4)便于搜索,表示知识的符号结构和推理机制应支持对知识库的高效搜索,使得智能系统能够迅速地感知事物之间的关系和变化;同时很快地从知识库中找到有关的知识。(5)便于推理,要能够从己有的知识中推出需要的答案和结论。15中南大学智能系统与智能软件研究所2.0引言:知识的分类形态性知识、内容性知识、效用性知识三者的综合,构成了知识的完整概念16中南大学智能系统与智能软件研究所2.1状态空间法
(StateSpaceRepresentation)问题求解技术主要是两个方面:问题的表示求解的方法状态空间法状态(state)算符(operator)状态空间方法17中南大学智能系统与智能软件研究所2.1.1
问题状态描述定义状态:描述某类不同事物间的差别而引入的一组最少变量q0,q1,…,qn的有序集合。其矢量形式如下:
Q=[q0,q1,…,qn]T式中每个元素qi(i=0,1,…,n)为集合的分量,称为状态变量。给定每个分量的一组值就得到一个具体的状态,如
qk=[q0k,q1k,…,qnk]T
2.1状态空间法18中南大学智能系统与智能软件研究所2.1.1
问题状态描述算符:使问题从一种状态变化为另一种状态的手段称为操作符或算符。操作符可为走步、过程、规则、数学算子、运算符号或逻辑符号等。问题的状态空间(statespace)
:是一个表示该问题全部可能状态及其关系的图,它包含三种说明的集合,即所有可能的问题初始状态集合S、操作符集合F以及目标状态集合G。因此,可把状态空间记为三元状态(S,F,G)。19中南大学智能系统与智能软件研究所2.
状态空间表示概念详释对一个问题的状态描述,必须确定3件事:(1)该状态描述方式,特别是初始状态描述;(2)操作符集合及其对状态描述的作用;(3)目标状态描述的特性。例如下棋、迷宫及各种游戏。OriginalStateMiddleStateGoalState2.1状态空间法20中南大学智能系统与智能软件研究所例:三数码难题
(3puzzleproblem)123123123312312312初始棋局目标棋局2.1状态空间法21中南大学智能系统与智能软件研究所2.1.2状态图示法图论中的几个术语
·
节点(node):图形上的汇合点,用来表示状态、事件和时间关系的汇合,也可用来指示通路的汇合;·弧线(arc):节点间的连接线;·有向图(directedgraph):一对节点用弧线连接起来,从一个节点指向另一个节点。·
后继节点(descendantnode)与父辈节点(parentnode):如果某条弧线从节点ni指向节点nj,那么节点nj就叫做节点ni的后继节点或后裔,而节点ni叫做节点nj的父辈节点或祖先。22中南大学智能系统与智能软件研究所2.1.2状态图示法路径:某个节点序列(ni1,ni2,…,nik)当j=2,3,…,k时,如果对于每一个ni,nj-1都有一个后继节点nij存在,那么就把这个节点序列叫做从节点ni1至节点nik的长度为k的路径。代价:用c(ni,nj)来表示从节点ni指向节点nj的那段弧线的代价。两节点间路径的代价等于连接该路径上各节点的所有弧线代价之和。显式表示:各节点及其具有代价的弧线由一张表明确给出。此表可能列出该图中的每一节点、它的后继节点以及连接弧线的代价。隐式表示:节点的无限集合{si}作为起始节点是已知的。后继节点算符Γ也是已知的,它能作用于任一节点以产生该节点的全部后继节点和各连接弧线的代价。23中南大学智能系统与智能软件研究所图的显示说明和隐示说明一个图可由显式说明也可由隐式说明。显然,显式说明对于大型的图是不切实际的,而对于具有无限节点集合的图则是不可能的。把后继算符应用于节点的过程,就是扩展一个节点的过程。因此,搜索某个状态空间以求得算符序列的一个解答的过程,就对应于使隐式图足够大一部分变为显式以便包含目标的过程。这样的搜索图是状态空间问题求解的主要基础。
问题的表示对求解工作量有很大的影响。人们显然希望有较小的状态空间表示。许多似乎很难的问题,当表示适当时就可能具有小而简单的状态空间。2.1.2状态图示法AB2.1状态空间法24中南大学智能系统与智能软件研究所2.1.3状态空间表示举例产生式系统(productionsystem)一个总数据库:它含有与具体任务有关的信息随着应用情况的不同,这些数据库可能简单,或许复杂。一套规则:它对数据库进行操作运算。每条规则由左部鉴别规则的适用性或先决条件以及右部描述规则应用时所完成的动作。一个控制策略:它确定应该采用哪一条适用规则,而且当数据库的终止条件满足时,就停止计算。2.1状态空间法25中南大学智能系统与智能软件研究所
状态空间表示举例例:猴子和香蕉问题2.1状态空间法26中南大学智能系统与智能软件研究所解题过程
用一个四元表列(W,x,Y,z)来表示这个问题状态.其中:W-猴子的水平位置;x-当猴子在箱子顶上时取x=1;否则取x=0;Y-箱子的水平位置;z-当猴子摘到香蕉时取z=1;否则取z=0。这个问题的操作(算符)如下:
goto(U)表示猴子走到水平位置U或者用产生式规则表示为(W,0,Y,z)
goto(U)(U,0,Y,z)2.1状态空间法27中南大学智能系统与智能软件研究所pushbox(V)猴子把箱子推到水平位置V,即有
(W,0,W,z)
pushbox(V)(V,0,V,z)climbbox猴子爬上箱顶,即有
(W,0,W,z)
climbbox
(W,1,W,z)grasp猴子摘到香蕉,即有
(c,1,c,0)grasp(c,1,c,1)2.1状态空间法28中南大学智能系统与智能软件研究所求解过程令初始状态为(a,0,b,0)。这时,goto(U)是唯一适用的操作,并导致下一状态(U,0,b,0)。现在有3个适用的操作,即goto(U),pushbox(V)和climbbox(若U=b)。把所有适用的操作继续应用于每个状态,我们就能够得到状态空间图,如图所示。从图不难看出,把该初始状态变换为目标状态的操作序列为:
{goto(b),pushbox(c),climbbox,grasp}29中南大学智能系统与智能软件研究所猴子和香蕉问题的状态空间图30中南大学智能系统与智能软件研究所猴子和香蕉问题自动演示:
Ha!Ha!31中南大学智能系统与智能软件研究所九宫排序(宽度优先搜索)23184765
231847652831476523184765283147652831647528314765283164752831647528371465
8321476528143765283145761237846512384765125673123847658432中南大学智能系统与智能软件研究所九宫排序(深度优先搜索)23184765
231847652831476523184765283147652831647528314765283164752831647528371465
83214765281437652831457612378465123847652836417528316754832147652837146528143765283145761238476523456789abcd133中南大学智能系统与智能软件研究所2.2问题归约法
(ProblemReductionRepresentation)子问题1子问题n原始问题子问题集本原问题34中南大学智能系统与智能软件研究所问题归约表示的组成部分:一个初始问题描述;一套把问题变换为子问题的操作符;一套本原问题描述。问题归约的实质:从目标(要解决的问题)出发逆向推理,建立子问题以及子问题的子问题,直至最后把初始问题归约为一个平凡的本原问题集合。2.2问题规约法35中南大学智能系统与智能软件研究所2.2.1问题归约描述
(ProblemReductionDescription)梵塔难题123CBA2.2问题规约法36中南大学智能系统与智能软件研究所解题过程(3个圆盘问题)1231231231231231231231232.2问题规约法37中南大学智能系统与智能软件研究所多圆盘梵塔难题演示2.2问题规约法38中南大学智能系统与智能软件研究所2.2.2与或图表示1.与图、或图、与或图2.2问题规约法ABCD与图ABC或图39中南大学智能系统与智能软件研究所2.2问题规约法BCDEFGAHMBCDEFGAN40中南大学智能系统与智能软件研究所2.一些关于与或图的术语2.2问题规约法HMBCDEFGAN父节点与节点弧线或节点子节点终叶节点41中南大学智能系统与智能软件研究所3.定义2.2问题规约法与或图例子ttttttttt(a)(b)有解节点无解节点终叶节点42中南大学智能系统与智能软件研究所不可解节点的一般定义(1)没有后裔的非终叶节点为不可解节点。(2)全部后裔为不可解的非终叶节点且含有或后继节点,此非终叶节点才是不可解的。(3)后裔至少有一个为不可解的非终叶节点且含有与后继节点,此非终叶节点才是不可解的。与或图构成规则(1)与或图中的每个节点代表一个要解决的单一问题或问题集合。图中所含起始节点对应于原始问题。2.2问题规约法43中南大学智能系统与智能软件研究所(2)对应于本原问题的节点,叫做终叶节点,它没有后裔.(3)对于把算符应用于问题A的每种可能情况,都把问题变换为一个子问题集合;有向弧线自A指向后继节点表示所求得的子问题集合。(4)一般对于代表两个或两个以上子问题集合的每个节点,有向弧线从此节点指向此子问题集合中的各个节点。由于只有当集合中所有的项都有解时,这个子问题的集合才能获得解答,所以这些子问题节点叫做与节点。(5)在特殊情况下,当只有一个算符可应用于问题A,而且这个算符产生具有一个以上子问题的某个集合时,由上述规则3和规则4所产生的图可以得到简化。44中南大学智能系统与智能软件研究所梵塔问题归约图(113)(123)
(111)(113)
(123)(122)
(111)(333)
(122)(322)
(111)(122)
(322)(333)
(321)(331)
(322)(321)
(331)(333)
2.2问题规约法45中南大学智能系统与智能软件研究所2.3命题逻辑法归结推理命题逻辑谓词逻辑Skolem标准形、子句集基本概念谓词逻辑归结原理合一和置换、控制策略数理逻辑命题逻辑归结Herbrand定理46中南大学智能系统与智能软件研究所命题逻辑的归结法命题逻辑基础:定义:合取式:p与q,记做pΛq析取式:
p或q,记做p∨q蕴含式:如果p则q,记做p→q等价式:p当且仅当q,记做p<=>q47中南大学智能系统与智能软件研究所命题逻辑基础定义:若A无成假赋值,则称A为重言式或永真式;若A无成真赋值,则称A为矛盾式或永假式;若A至少有一个成真赋值,则称A为可满足的;析取范式:仅由有限个简单合取式组成的析取式。合取范式:仅由有限个简单析取式组成的合取式。48中南大学智能系统与智能软件研究所命题逻辑基础基本等值式24个(1)交换率:p∨q
<=>q
∨p
;
pΛq<=>qΛp
结合率:(p∨q)∨
r<=>p∨(q
∨r); (pΛ
q)Λ
r<=>pΛ(q
Λ
r)分配率:p∨(q
Λ
r)<=>(p∨q)Λ(p
∨r)
;
pΛ(q
∨
r)<=>(pΛ
q)∨(pΛ
r)49中南大学智能系统与智能软件研究所命题逻辑基础基本等值式(1)摩根率:~
(p∨q)
<=>~
pΛ
~
q
;
~
(pΛq)
<=>~
p∨
~
q
吸收率:p∨(pΛq
)<=>p
;
pΛ(p∨q
)<=>p
同一律:p∨0
<=>p
;
pΛ1
<=>p
蕴含等值式:p→
q
<=>~
p∨q
假言易位式:p→
q
<=>~p→~
q
50中南大学智能系统与智能软件研究所命题逻辑基础命题:能判断真假(不是既真又假)的陈述句。 简单陈述句描述事实、事物的状态、关系等性质。例如:1.
1+1=22.
雪是黑色的。
3.
北京是中国的首都。判断一个句子是否是命题,有先要看它是否是陈述句,而后看它的真值是否唯一。以上的例子都是陈述句,第4句的真值现在是假,随着人类科学的发展,有可能变成真,但不管怎样,真值是唯一的。因此,以上4个例子都是命题。而例如:1.快点走吧!2.到那去?3.x+y>10等.
都不是命题。51中南大学智能系统与智能软件研究所命题表示公式(1)将陈述句转化成命题公式。如:设“下雨”为p,“骑车上班”为q,,1.“只要不下雨,我骑自行车上班”。~p
是q的充分条件, 因而,可得命题公式:~p→q2.“只有不下雨,我才骑自行车上班”。~p
是q的必要条件, 因而,可得命题公式:q→~p52中南大学智能系统与智能软件研究所命题表示公式(2)例如:1.
“如果我进城我就去看你,除非我很累。” 设:p,我进城,q,去看你,r,我很累。 则有命题公式:~r→(p→q)。2.“应届高中生,得过数学或物理竞赛的一等奖, 保送上北京大学。” 设:p,应届高中生,q,保送上北京大学上学,
r,是得过数学一等奖。t,是得过物理一等奖。 则有命题公式公式:p
∧(r∨t)→
q。53中南大学智能系统与智能软件研究所命题逻辑的归结法基本单元:简单命题(陈述句)例:命题:A1、A2、A3
和B求证:A1ΛA2ΛA3成立,则B成立,即:A1ΛA2ΛA3→B反证法:证明A1ΛA2ΛA3Λ~B
是矛盾式(永假式)54中南大学智能系统与智能软件研究所命题逻辑的归结法建立子句集合取范式:命题、命题和的与,如:
PΛ(P∨Q)Λ(~P∨Q)子句集S:合取范式形式下的子命题(元素)的集合例:命题公式:PΛ(P∨Q)Λ(~P∨Q)子句集S:S={P,P∨Q,~P∨Q}55中南大学智能系统与智能软件研究所命题逻辑的归结法归结式消除互补文字对P和~P∨Q,求新子句→得到归结式。如子句:C1,C2,归结式:R(C1,C2)=C1ΛC2
注意:C1ΛC2→R(C1,C2)
,反之不一定成立。56中南大学智能系统与智能软件研究所命题逻辑的归结法归结过程将命题写成合取范式求出子句集对子句集使用归结推理规则归结式作为新子句参加归结归结式为空子句□
,S是不可满足的(矛盾),原命题成立。(证明完毕)。谓词的归结:除了有量词和函数以外,其余和命题归结过程一样。57中南大学智能系统与智能软件研究所命题逻辑的归结法归结式的定义及性质对子句C1和C2,若C1中有一个文字L1,而C2中有一个与L1成互补的文字L2,则分别从C1,C2中删去L1和L2,并将其剩余部分组成新的析取式,则称该子句为归结式。例1:设两个子句C1=L∨C1',C2=(~
L)∨C2',则归结式C=Cl’∨C2’。当C1'=C2’=□时,C=□。例2:PΛ(~P∨Q)=Q定理:二个子句C1和C2的归结式C是C1和C2的逻辑推论。
58中南大学智能系统与智能软件研究所命题逻辑归结例题(1)例题,证明公式:(P→Q)→(~Q→~P)证明:(1)根据归结原理,将待证明公式转化成待归结命题公式:(P→Q)∧~(~Q→~P)(2)分别将公式前项化为合取范式:
P→Q=~P∨Q
结论求~后的后项化为合取范式: ~(~Q→~P)=~(Q∨~P)=~Q∧P
两项合并后化为合取范式:(~P∨Q)∧~Q∧P
(3)则子句集为:{~P∨Q,~Q,P}59中南大学智能系统与智能软件研究所命题逻辑归结例题(2)子句集为: {~P∨Q,~Q,P}(4)对子句集中的子句进行归结可得:1.
~P∨Q2.
~Q3.
P4.
Q, (1,3归结)5.
, (2,4归结) 由上可得原公式成立。60中南大学智能系统与智能软件研究所证明:化成子句集
S={P,~
P∨┐Q∨R,
~
S∨Q,~
T∨Q,
T,~
R}
归结可用图的演绎树表示,由于根部出现空子句,因此命题R得证。
例:设已知前提集为
P……(1)(P∧Q)→R………(2)(S∨T)→Q………(3)T………(4)
求证R。61中南大学智能系统与智能软件研究所2.4一阶谓词逻辑法个体词:表示主语的词谓词:刻画个体性质或个体之间关系的词量词:表示数量的词2.4.1谓词演算
语法和语义基本符号:谓词符号、变量符号、函数符号、常量符号、括号和逗号原子公式(atomicformulas):由若干谓词符号和项组成的谓词演算。原子公式是谓词演算基本积木块。62中南大学智能系统与智能软件研究所2.4一阶谓词逻辑法小王是个工程师。8是个自然数。我去买花。小丽和小华是朋友。其中,“小王”、“工程师”、“我”、“花”、“8”、“小丽”、“小华”都是个体词,而“是个工程师”、“是个自然数”、“去买”、“是朋友”都是谓词。显然前两个谓词表示的是事物的性质,第三个谓词“去买”表示的一个动作也表示了主、宾两个个体词的关系,最后一个谓词“是朋友”表示两个个体词之间的关系。63中南大学智能系统与智能软件研究所2.4一阶谓词逻辑法一阶逻辑公式及其解释个体常量:a,b,c个体变量:x,y,z谓词符号:P,Q,R量词符号:
,
64中南大学智能系统与智能软件研究所例如,要表示“机器人(ROBOT)在1号房间(r1)内”,如图所示,可以应用原子公式:当机器人ROBOT移到房间r2时,原子公式可以表示为:INROOM(ROBOT,r2)这两个原子公式的通用形式就是
65中南大学智能系统与智能软件研究所又如,“李的母亲和他的父亲结婚”这句话的原子公式表示如下:连词和量词(Connective&Quantifiers)连词与及合取(conjunction):合取就是用连词∧把几个公式连接起来而构成的公式。合取项是合取式的每个组成部分。一些合适公式所构成的任一合取也是一个合适公式。例:LIKE(I,MUSIC)∧LIKE(I,PAINTING)(我喜爱音乐和绘画。)66中南大学智能系统与智能软件研究所或及析取(disjunction):析取就是用连词∨把几个公式连接起来而构成的公式。析取项是析取式的每个组成部分。由一些合适公式所构成的任一析取也是一个合适公式。例:PLAYS(LILI,BASKETBALL)∨PLAYS(LILI,FOOTBALL)(李力打篮球或踢足球。)蕴涵(Implication):“=>”表示“如果-那么”的语句。用连词=>连接两个公式所构成的公式叫做蕴涵。如果前项和后项都是合适公式,那么蕴涵也是合适公式。
IF=>THEN前项(左式)=>后项(右式)例:RUNS(LIUHUA,FASTEST)=>WINS(LIUHUA,CHAMPION)(如果刘华跑得最快,那么他取得冠军)2.3谓词逻辑法67中南大学智能系统与智能软件研究所非(Not):表示否定,~、┑均可表示。一个合适公式的否定也是合适公式。例:~INROOM(ROBOT,r2)(机器人不在2号房间内)量词全称量词(UniversalQuantifiers):若一个原子公式P(x),对于所有可能变量x都具有T值,则用
(
x)P(x)表示。例:(
x)[ROBOT(x)=>COLOR(x,GRAY)](
x)[Student(x)=>Uniform(x,Color)]存在量词(ExistentialQuantifiers):若一个原子公式P(x),至少有一个变元X,可使P(X)为T值,则用(
x)P(x)表示。例(
x)INROOM(x,r1)68中南大学智能系统与智能软件研究所例如:(1)所有的人都是要死的。(2)
有的人活到一百岁以上。在个体域D为人类集合时,可符号化为:(1)
xP(x),其中P(x)表示x是要死的。(2)
xQ(x),其中Q(x)表示x活到一百岁以上。在个体域D是全总个体域时,引入特殊谓词R(x)表示x是人,可符号化为:(1)
x(R(x)→P(x)),
其中,R(x)表示x是人;P(x)表示x是要死的。(2)
x(R(x)∧Q(x)), 其中,R(x)表示x是人;Q(x)表示x活到一百岁以上。69中南大学智能系统与智能软件研究所量词否定等值式:~(
x
)
M(x)<=>(
y
)~
M(y)~(
x
)
M(x)<=>(
y
)~
M(y)量词分配等值式:(
x
)(
P(x)ΛQ(x))<=>(
x
)
P(x)Λ(
x
)
Q(x)(
x
)(
P(x)∨Q(x))<=>(
x
)
P(x)∨(
x
)
Q(x)消去量词等值式:设个体域为有穷集合(a1,a2,…an)(
x
)
P(x)<=>P(a1
)ΛP(a2
)Λ…ΛP(an
)(
x
)P(x)<=>P(a1
)∨P(a2
)∨…∨P(an
)70中南大学智能系统与智能软件研究所量词辖域收缩与扩张等值式:(
x
)(
P(x)∨Q)<=>(
x
)
P(x)∨Q(
x
)(
P(x)ΛQ)<=>(
x
)
P(x)ΛQ
(
x
)(
P(x)→Q)<=>(
x
)
P(x)→Q
(
x
)(Q
→P(x))<=>Q
→(
x
)
P(x)(
x
)(
P(x)∨Q)<=>(
x
)
P(x)∨Q(
x
)(
P(x)ΛQ)<=>(
x
)
P(x)ΛQ
(
x
)(
P(x)→Q)<=>(
x
)
P(x)→Q
(
x
)(Q
→P(x))<=>Q
→(
x
)
P(x)71中南大学智能系统与智能软件研究所2.4.2谓词公式原子公式的的定义:用P(x1,x2,…,xn)表示一个n元谓词公式,其中P为n元谓词,x1,x2,…,xn为客体变量或变元。通常把P(x1,x2,…,xn)叫做谓词演算的原子公式,或原子谓词公式。分子谓词公式可以用连词把原子谓词公式组成复合谓词公式,并把它叫做分子谓词公式。2.3谓词逻辑法72中南大学智能系统与智能软件研究所项可递归定义如下:(1)单独一个个体是项(包括常量和变量)。(2)若f是n元函数符号,而是项,则f()是项。(3)任何项仅由规则(1)(2)所生成。定义若P为n元谓词符号,t1,…,tn都是项,则称P(t1,…,tn)为原子公式。73中南大学智能系统与智能软件研究所定义一阶谓词逻辑的合式公式:(1)原子谓词公式是合式公式(也称为原子公式)。(2)若P、Q是合式公式,则
(~
P)、(P∧Q)、(P∨Q)、(P→Q)、(P←→Q)
也是合式公式。(3)若P是合式公式,x是任一个体变元,则
(
x)P、(
x)P也是合式公式。(4)有限次重复(1)和(3)构成的公式也是合式公司。2.3谓词逻辑法74中南大学智能系统与智能软件研究所2.3.3置换与合一置换:在谓词逻辑中,有些推理规则可应用于一定的合适公式和合适公式集,以产生新的合适公式。一个重要的推理规则是假元推理,这就是由合适公式W1和W1=>W2产生合适公式W2的运算。另一个推理规则叫做全称化推理,它是由合适公式(
x)W(x)产生合适公式W(A),其中A为任意常量符号。概念假元推理:全称化推理综合推理75中南大学智能系统与智能软件研究所2.3.3置换与合一置换:就是在该表达式中用置换项置换变量用项(A)替换函数表达式中的变量(x),记为Es,即表示一个表达式E(Expression)用一个置换s(Substitution)而得到的表达式的置换。
例1:表达式P[x,f(y),B]的4个置换为:
s1={z/x,w/y}
s2={A/y}
s3={q(z)/x,A/y}
s4={c/x,A/y}76中南大学智能系统与智能软件研究所2.3.3置换与合一我们用Es来表示一个表达式E用置换s所得到的表达式的置换。于是,可得到P[x,f(y),B]的4个置换的例,如下:
置换置换的例sl={z/x,w/y},P[x,f(y),B]s1=P[z,f(w),B]s2={A/y},P[x,f(y),B]s2=P[x,f(A),B]s3={g(z)/x,A/y},P[x,f(y),B]s3=P[g(z),f(A),B]s4={C/x,A/y},P[x,f(y),B]s4=P[C,f(A),B]77中南大学智能系统与智能软件研究所置换置换的例
sl={z/x,w/y},P[x,f(y),B]s1=P[z,f(w),B]
s2={A/y},P[x,f(y),B]s2=P[x,f(A),B]
s3={g(z)/x,A/y},P[x,f(y),B]s3=P[g(z),f(A),B]
s4={C/x,A/y},P[x,f(y),B]s4=P[C,f(A),B]第一个例叫做原始文字的初等变式,实际上置换后只是对变量作了换名。第四个例称作基例,即置换后项中不再含有变量。用s={t1/v1,t2/v2,….,tn/vn}来表示任一置换,用s对表达式E作置换后的例简记为Es。78中南大学智能系统与智能软件研究所2.3.3置换与合一性质.可结合的:(Ls1)s2=L(s1s2)(s1s2)s3=s1(s2s3)
置换是可结合的。用s1s2表示两个置换s1和s2的合成。L表示一表达式,则有
(Ls1)s2=L(s1s2)以及(s1s2)s3=s1(s2s3)即用s1和s2相继作用于表达式L是同用s1s2作用于L一样的。.不可交换的一般说来,置换是不可交换的,即s1s2≠s2s12.3谓词逻辑法79中南大学智能系统与智能软件研究所合一(Unification)合一:寻找项对变量的置换,以使两表达式一致。可合一:如果一个置换s作用于表达式集{Ei}的每个元素,则我们用{Ei}s来表示置换例的集。我们称表达式集{Ei}是可合一的。例:表达式集P[x,f(y),B],P[x,f(B),B]的合一者设为:
s={A/x,B/y}因为:P[x,f(y),B]s=P[A,f(y),B]=P[A,f(B),B]若s为{Ei}的任一合一者,又存在某个s’,使得
{Ei}s={Ei}gs’成立,则称g为{Ei}的最通用(最一般)的合一者,记为mgu。上例最简单的合一者为:mgu
g={B/y}.
2.3谓词逻辑法80中南大学智能系统与智能软件研究所UNIFY算法
mgug的置换限制最少,所产生的例更一般化,有利于归结过程的灵活使用。UNIFY算法(算法中可合一的表达式要用表结构来表示)如把P(x,f(A,y))表示成(Px(fAy))找到的合一者是可合一表达式的mgu,若表达式不可合一时,则算法失败退出。
81中南大学智能系统与智能软件研究所递归过程UNIFY(E1,E2)(1)IFATOM(E1)ORATOM(E2)THEN交换E1和E2的位置使E1是一个原子(有必要时),do:;
原子包括谓词符号、函数符号、常数符号、变量符号和否定符号。E1不是原子,而E2是原子时,则交换位置,使E1是一个原子。(2)Begin(3)IFE1=E2THENRETURNNIL;82中南大学智能系统与智能软件研究所(4)IFVAR(E1)IFCONTAIN(E2,E1)THENRETURN(FAIL)ELSERETURN({E2/E1});E1是变量且E2中不含有E1,返回置换{E2/E1}。(5)IFVAR(E2)THENRETURN({E1/E2})ELSERETURN(FAIL);
E2是变量返回置换{E1/E2}。(6)End(7)F1:=FIRST(E1),T1:=TAIL(E1);Fl放E1第一个元素,其余元素放在T1中。
83中南大学智能系统与智能软件研究所(8)F2:=FIRST(E2),T2:=TAIL(E2);(9)s1:=UNIFY(F1,F2);递归调用。(10)IFs1=FAILTHENRETURN(FAIL);(11)G1:=T1s1,G2:=T2s1;对未匹配部分作置换。(12)s2:=UNIFY(G1,G2);(13)IFs2:=FAILTHENRETURN(FAIL);(14)
RETURN(s=s1s2);返回s1和s2的合成。UNIFY(E1,E2)算法84中南大学智能系统与智能软件研究所利用该算法可找到可合一表达式集的最一般的合一者,例{Ei}mgug{Ei}g{P(x),P(A)},{A/x}P(A){P(f(x),y,g(y)),P(f(x),z,g(x))}{x/y,x/z}P(f(x),x,g(x))85中南大学智能系统与智能软件研究所谓词归结子句形(Skolem
标准形)SKOLEM标准形前束范式
定义:说公式A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。86中南大学智能系统与智能软件研究所谓词归结子句形(Skolem
标准形)即:把所有的量词都提到前面去,然后消掉所有量词
(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)约束变项换名规则:(Qx
)
M(x)<=>(Qy
)
M(y)(Qx
)
M(x,z)<=>(Qy
)
M(y,z)87中南大学智能系统与智能软件研究所谓词归结子句形(Skolem
标准形)量词消去原则: 消去存在量词“
”,略去全程量词“
”。
注意:左边有全程量词的存在量词,消去时该变量改写成为全程量词的函数;如没有,改写成为常量。88中南大学智能系统与智能软件研究所谓词归结子句形(Skolem
标准形)Skolem定理: 谓词逻辑的任意公式都可以化为与之等价的前束范式,但其前束范式不唯一。SKOLEM标准形定义: 消去量词后的谓词公式。注意:谓词公式G的SKOLEM标准形同G并不等值。89中南大学智能系统与智能软件研究所谓词归结子句形(Skolem
标准形)例:将下式化为Skolem标准形: ~(
x)(
y)P(a,x,y)→(
x)(~(
y)Q(y,b)→R(x))解:第一步,消去→号,得: ~(~(
x)(
y)P(a,x,y))∨(
x)(~~(
y)Q(y,b)∨R(x))第二步,~深入到量词内部,得:
(
x)(
y)P(a,x,y)∨(
x)((
y)Q(y,b)∨R(x))第三步,变元易名,得
(
x)((
y)P(a,x,y)∨(u)(
v)(Q(v,b)∨R(u))第四步,存在量词左移,直至所有的量词移到前面,得:
(
x)(
y)(u)(
v)P(a,x,y)∨(Q(v,b)∨R(u))由此得到前述范式90中南大学智能系统与智能软件研究所谓词归结子句形(Skolem
标准形)第五步,消去“
”(存在量词),略去“
”全称量词消去(
y),因为它左边只有(
x),所以使用x的函数f(x)代替之,这样得到:
(
x)(
z)(P(a,x,f(x))∧~Q(z,b)∧~R(x))消去(
z),同理使用g(x)代替之,这样得到:
(
x)(P(a,x,f(x))∧~Q(g(x),b)∧~R(x))则,略去全称变量,原式的Skolem标准形为:
P(a,x,f(x))∧~Q(g(x),b)∧~R(x)
91中南大学智能系统与智能软件研究所谓词归结子句形子句与子句集文字:不含任何连接词的谓词公式。子句:一些文字的析取(谓词的和)。子句集S的求取:
G→SKOLEM标准形
→消去存在变量
→以“,”取代“Λ”,并表示为集合形式。92中南大学智能系统与智能软件研究所谓词归结子句形G是不可满足的<=>S是不可满足的G与S不等价,但在不可满足得意义下是一致的。定理: 若G是给定的公式,而S是相应的子句集,则G是不可满足的<=>S是不可满足的。
注意:G真不一定S真,而S真必有G真。 即:S=>G93中南大学智能系统与智能软件研究所谓词归结子句形G=G1ΛG2ΛG3Λ…ΛGn
的子句形G的字句集可以分解成几个单独处理。有SG=S1US2US3U…USn
则SG
与S1US2US3U…USn在不可满足得意义上是一致的。 即SG
不可满足<=>S1US2US3U…USn不可满足94中南大学智能系统与智能软件研究所求取子句集例(1)例:对所有的x,y,z来说,如果y是x的父亲,z又是y的父亲,则z是x的祖父。又知每个人都有父亲,试问对某个人来说谁是它的祖父?求:用一阶逻辑表示这个问题,并建立子句集。解:这里我们首先引入谓词:
P(x,y)表示x是y的父亲
Q(x,y)表示x是y的祖父
ANS(x)表示问题的解答95中南大学智能系统与智能软件研究所求取子句集例(2)对于第一个条件,“如果x是y的父亲,y又是z的父亲,则x是z的祖父”,一阶逻辑表达式如下:
A1:(
x)(
y)(
z)(P(x,y)∧P(y,z)→Q(x,z)) SA1:~P(x,y)∨~P(y,z)∨Q(x,z)对于第二个条件:“每个人都有父亲”,一阶逻辑表达式:
A2:(
y)(
x)P(x,y) SA2:P(f(y),y)对于结论:某个人是它的祖父
B:(
x)(
y)Q(x,y)
否定后得到子句:~((
x)(
y)Q(x,y))∨ANS(x) S~B:~Q(x,y)∨ANS(x)则得到的相应的子句集为:{SA1,SA2,S~B}96中南大学智能系统与智能软件研究所2.3.4归结推理
归结方法,1965年Robinson提出归结方法的基本思想命题逻辑归结原理谓词逻辑归结原理97中南大学智能系统与智能软件研究所2.3.4什么是归结原理在定理证明系统中,已知一公式集F1,F2,…,Fn,要证明一个公式W(定理)是否成立,即要证明W是公式集的逻辑推论时,一种证明法就是要证明F1∧F2∧…∧Fn→W为永真式。反证法:证明F=F1∧F2∧…∧Fn∧┐W为永假,这等价于证明F对应的子句集S=S0∪{┐W}为不可满足的。98中南大学智能系统与智能软件研究所思路:设法检验扩充的子句集Si是否含有空子句,若S集中存在空子句,则S不可满足。若没有空子句,则就进一步用归结法从S导出S1。然后再检验S1是否有空子句。用归结法导出的扩大子句集S1,其不可满足性是不变的,所以若S1中有空子句,也就证得了S的不可满足性。通过归结过程演绎出S的不可满足性来,从而使定理得到证明。99中南大学智能系统与智能软件研究所2.3.4谓词逻辑的归结原理在谓词逻辑中,要考虑变量的约束问题,在应用归结法时,要对公式作变量置换和合一等处理,才能得到互补的基本式,以使进行归结。归结过程:·若S中两子句间有相同互补文字的谓词,但它们的项不同,则必须找出对应的不一致项;
·进行变量置换,使它们的对应项一致;
·求归结式看能否导出空子句。100中南大学智能系统与智能软件研究所2.3.4谓词逻辑的归结原理归结原理就是从子句集S出发,应用归结推理规则导出子句集S1。再从S1出发导出S2,依此类推,直到某一个子句集Sn出现空子句为止。根据不可满足性等价原理,已知若Sn为不可满足的,则可逆向依次推得S必为不可满足的。用归结法,过程比较单钝,只涉及归结推理规则的应用问题,因而便于实现机器证明。101中南大学智能系统与智能软件研究所归结原理的归结过程归结的过程写出谓词关系公式→用反演法写出谓词表达式→SKOLEM标准形→子句集S→对S中可归结的子句做归结→归结式仍放入S中,反复归结过程→得到空子句
▯得证102中南大学智能系统与智能软件研究所谓词逻辑的归结过程设C1和C2为不具有完全相同变元的两个子句,子句中的变量已标准化。采用文字集的形式来表示子句(即文字之间理解为析取关系),则有
C1={C1i},(i=1,2,…,n),
C2={C2j},(j=l,2,…,m)103中南大学智能系统与智能软件研究所设{L1k}和{L2k}分别为C1和C2的两个子集。若{L1k}和{┐L2k}的并集存在一个mgus,则两个子句的归结式为
C={{C1i}-{L1k}}s∪{{C2j}-{L2k}}s由于有多种方式选取{L1k}和{L2k},因此归结式不是唯一的。104中南大学智能系统与智能软件研究所例:Cl=P(x,f(A))∨P(x,f(y))∨Q(y)C2=┐P(z,f(A))∨┐Q(z)(1)取L11=P(x,f(A)),L21=┐P(z,f(A))
则s={z/x}使L11和┐L21合一,归结式为
P(z,f(y))∨Q(y)∨┐Q(z)(2)取L11=P(x,f(y)),L21=┐P(z,f(A))
则s={z/x,A/y},归结式为Q(A)∨┐Q(z)(3)取L11=Q(y),L21=┐Q(z),则s={y/z},归结式为P(x,f(A))∨P(x,f(y))∨P(y,f(A))105中南大学智能系统与智能软件研究所选择不同文字对做归结时可得到不同的归结式,但由于都是用最一般的合一者作置换,因此这些归结式仍是最一般的归结式。如果对某个文字不是用mgu来合一,那么得到的归结式比最一般的归结式则有较多的限制。总是希望用最一般的归结式,以增加归结过程的灵活性。106中南大学智能系统与智能软件研究所例:已知:(1)会朗读的人是识字的,(2)海豚都不识字,(3)有些海豚是很机灵的。证明:有些很机灵的东西不会朗读。解:把问题用谓词逻辑描述如下,已知:(1)(
x)(R(x)→L(x))(2)(
x)(D(x)→┐L(x))(3)(
x)(D(x)∧I(x))
求证:(
x(I(x)∧┐R(x))
107中南大学智能系统与智能软件研究所前提化简,待证结论取反并化成子句形,求得子句集:(1)┐R(x)∨L(x)(2)┐D(y)∨┐L(y)(3a)D(A)(3b)I(A)(4)┐I(z)∨R(z)一个可行的证明过程:(5)R(A)(3b)和(4)的归结式
(6)L(A)(5)和(1)的归结式
(7)┐D(A)(6)和(2)的归结式
(8)NIL(7)和(3a)的归结式108中南大学智能系统与智能软件研究所例题“快乐学生”问题假设任何通过计算机考试并获奖的人都是快乐的,任何肯学习或幸运的人都可以通过所有的考试,张不肯学习但他是幸运的,任何幸运的人都能获奖。求证:张是快乐的。解:先将问题用谓词表示如下:R1:“任何通过计算机考试并获奖的人都是快乐的”
(
x)((Pass(x,computer)∧Win(x,prize))→Happy(x))R2:“任何肯学习或幸运的人都可以通过所有考试”
(
x)(
y)(Study(x)∨Lucky(x)→Pass(x,y))R3:“张不肯学习但他是幸运的” ~Study(zhang)∧Lucky(zhang)R4:“任何幸运的人都能获奖”
(
x)(Luck(x)→Win(x,prize))结论:“张是快乐的”的否定~Happy(zhang)109中南大学智能系统与智能软件研究所例题“快乐学生”问题由R1及逻辑转换公式:P∧W→H=~(P∧W)∨H,可得
(1)~Pass(x,computer)∨~Win(x,prize)∨Happy(x)由R2:(2)~Study(y)∨Pass(y,z)(3)~Lucky(u)∨Pass(u,v)由R3:(4)~Study(zhang)(5)Lucky(zhang)由R4:(6)~Lucky(w)∨Win(w,prize)由结论:(7)~Happy(zhang) (结论的否定)(8)~Pass(w,computer)∨Happy(w)∨~Luck(w)
(1)(6),{w/x}(9)~Pass(zhang,computer)∨~Lucky(zhang)
(8)(7),{zhang/w}(10)
~Pass(zhang,computer)(9)(5)(11)
~Lucky(zhang)(10)(3),{zhang/u,computer/v}
(12)
ɓ
(11)(5)
110中南大学智能系统与智能软件研究所2.3.5归结反演(Refutation)归结反演系统是用反演(反驳)或矛盾的证明法,使用归结推理规则建立的定理证明系统。这种证明系统是基于归结的反证法,故称归结反演系统。可用在信息检索、常识性推理和自动程序设计等。111中南大学智能系统与智能软件研究所l·归结反演的基本算法
综合数据库:子句集规则集合:IFcx(∈Si)和cy(∈Si)有归结式rxyTHENSi+1=Si∪{rxy}
目标条件:Sn中出现空子句112中南大学智能系统与智能软件研究所过程RESOLUTION(1)CLAUSES:=S;S为初始的基本子句集。(2)untilNIL是CLAUSES的元素,do:(3)begin(4)在CLAUSES中选两个不同的可归结的子句ci、cj;ci、cj称母子句。(5)求ci、cj的归结式rxy;(6)CLAUSES:={rxy}∪CLAUSES;(7)end;??113中南大学智能系统与智能软件研究所2·搜索策略选哪两个子句做归结?对哪一个文字做归结?114中南大学智能系统与智能软件研究所S={┐I(z)∨R(z),I(A),┐R(x)∨L(x),┐D(y)∨┐L(y),D(A)}归结过程用归结反演树表示比较简单。搜索策略的目标就是要找到一棵归结反演树。一个反演系统当存在一个矛盾时,如果使用的一种策略,最终都将找到一棵反演树,则这种策略是完备的。
归结反演树115中南大学智能系统与智能软件研究所提高策略效率——只归结含有互补对的文字;及时删去出现的重言式和被其他子句所包含的子句;每次归结都取与目标公式否定式有关的子句作为母子句之一进行归结等等。
(1)宽度优先策略(完备,效率低)宽度优先策略首先归结出基本集S中可能生成的所有归结式,称第一级归结式,然后生成第二级归结式等等,直到出现空子句。116中南大学智能系统与智能软件研究所(2)支持集策略(完备)归结时,其母子句中至少有一个是与目标公式否定式有关的子句。117中南大学智能系统与智能软件研究所(3)单元子句优先策略每次归结时优先选取单文字的子句(称单元子句)为母子句进行归结,显然归结式的文字数会比其他情况归结的结果要少,这有利于向空子句的方向搜索,实际上会提高效率。118中南大学智能系统与智能软件研究所(4)线性输入形策略每次归结时,至少有一个母子句是从基本集中挑选。该策略可限制生成归结式的数目,具有简单和效率高的优点。119中南大学智能系统与智能软件研究所它不是一个完备的策略,反例:S={Q(u)∨P(A),┑Q(w)∨P(w),
┑Q(x)∨┑P(x),Q(y)∨┑P(y)},从S出发很容易找到一棵反演树,但不存在一个线性输入形策略的反演树。120中南大学智能系统与智能软件研究所(5)祖先过滤策略
(完备)
祖先过滤策略的搜索过程121中南大学智能系统与智能软件研究所2.3.6谓词演算归结反演的合理性和完备性归结原理是反演完备的,即如果一个子句集合是不可满足的,则归结将会推导出矛盾。归结不能用于产生某子句集合的所有结论,但是它可以用于说明某个给定的句子是该子句集合所蕴涵的。因此,使用前面介绍的否定目标的方法,它可以发现所有的答案。122中南大学智能系统与智能软件研
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 2026年新疆维吾尔自治区乌鲁木齐市中小学教师招聘笔试参考题库及答案详解
- 2026年湖北省随州市法检系统书记员招聘考试模拟试题及答案详解
- 2025年武汉市汉阳区街道办人员招聘考试试题及答案详解
- 2026年铁岭市银州区中小学教师招聘考试备考题库及答案详解
- 2026年湖北省荆门市街道办人员招聘笔试备考试题及答案详解
- 2026年云南省玉溪市街道办人员招聘笔试备考题库及答案详解
- 2025年天津市西青区街道办人员招聘考试试题及答案详解
- 2026年海南省海口市法检系统书记员招聘考试参考试题及答案详解
- 初升高完美衔接教材 英语教学 句子成分与结构
- 2026年百色市右江区街道办人员招聘笔试备考试题及答案详解
- 2026年景洪市教育体育局公开选调教师(31人)参考题库及参考答案详解(新)
- 湖南省湘潭市2025-2026学年高一下学期期末考试物理自编试卷(人教版)(解析版)
- 2026江苏南通市通州区消防救援局第二批招聘镇(街道)基层消防网格员2人备考题库带答案详解
- 中国白塞病诊疗指南(2025版)
- 2026棉花大幅增殖技术创新遗传育种研究报告规划
- (HJ 166-2026)《土壤环境监测技术规范》培训课件
- 护理:护理安全管理与应急预案
- 2026中国碳捕集技术发展现状及未来应用前景分析报告
- 2026年消防设施操作员(中级维保)真题题库附完整答案详解(全优)
- 2025共识声明:维生素D在代谢健康中的作用课件
- DB36-T 1406-2021 杉木人工林近自然更新造林技术规程
评论
0/150
提交评论