人工智能之确定性推理课件

上传人:94****0 文档编号:183194402 上传时间:2023-01-29 格式:PPT 页数:93 大小:4.18MB
返回 下载 相关 举报
人工智能之确定性推理课件_第1页
第1页 / 共93页
人工智能之确定性推理课件_第2页
第2页 / 共93页
人工智能之确定性推理课件_第3页
第3页 / 共93页
点击查看更多>>
资源描述
第三章第三章 确定性推理确定性推理n3.1 基本概念基本概念n3.3 自然演绎推理自然演绎推理n3.4 归结演绎推理归结演绎推理n3.5 基于规则的演绎推理(与基于规则的演绎推理(与/或形演绎推理)或形演绎推理)3.1 基本概念基本概念n为使计算机具有智能,仅仅使它拥有知识还不够,更重要地,为使计算机具有智能,仅仅使它拥有知识还不够,更重要地,还必须使它具有思维能力,即能运用知识进行还必须使它具有思维能力,即能运用知识进行推理推理、求解问题、求解问题的能力。的能力。n知识表示(知识库)知识表示(知识库)求解过程(推理)求解过程(推理)n经典推理是根据经典逻辑(命题逻辑和一阶谓词逻辑)的经典推理是根据经典逻辑(命题逻辑和一阶谓词逻辑)的逻逻辑规则辑规则进行的一种推理,又称机械进行的一种推理,又称机械-自动定理证明。自动定理证明。n主要推理方法有:自然演绎推理、归结演绎推理、基于规则主要推理方法有:自然演绎推理、归结演绎推理、基于规则的演绎推理(与的演绎推理(与/或形演绎推理)。或形演绎推理)。基本概念基本概念推理是按推理是按某种策略某种策略由已知判断推出另一种判断的过程。在由已知判断推出另一种判断的过程。在AI系统中,推理是由程序来实现的,称为系统中,推理是由程序来实现的,称为推理机推理机。n不同的控制策略不同的控制策略 默认推理归纳推理演绎推理从新判断推出的途径)1(演绎推理演绎推理n由一般(全称判断)到个别(特称判断)的推理方法。由一般(全称判断)到个别(特称判断)的推理方法。n核心是核心是三段论三段论,通常由一个大前提、一个小前提和一个结,通常由一个大前提、一个小前提和一个结论三部分组成的。论三部分组成的。n例:例:阿凡提的故事阿凡提的故事-两头驴的故事两头驴的故事 我肩上驮的是两头驴的东西我肩上驮的是两头驴的东西(大前提)(大前提)国王和大臣的衣衫是我肩上驮的(小前提)国王和大臣的衣衫是我肩上驮的(小前提)国王和大臣的衣衫是两头驴的东西(结论)国王和大臣的衣衫是两头驴的东西(结论)归纳推理归纳推理n从个别到一般从个别到一般n归纳结论不具备逻辑必然性归纳结论不具备逻辑必然性n莫里斯莫里斯科恩科恩 逻辑学著作包括两部分,第一部分是演绎,其功能是解释谬逻辑学著作包括两部分,第一部分是演绎,其功能是解释谬误;第二部分是归纳,其功能是生成谬误误;第二部分是归纳,其功能是生成谬误 我们获得关于这个实在世界的一般性事我们获得关于这个实在世界的一般性事实的唯一方法!实的唯一方法!n演绎推理所得出的结论蕴含在一般性知识的前提演绎推理所得出的结论蕴含在一般性知识的前提中,演绎推理只不过是将已有事实揭示出来,因此中,演绎推理只不过是将已有事实揭示出来,因此它不能增殖新知识。它不能增殖新知识。n在归纳推理中,所推出的结论是没有包含在前提在归纳推理中,所推出的结论是没有包含在前提内容中的。这种由个别事物或现象推出一般性知识内容中的。这种由个别事物或现象推出一般性知识的过程,是增殖新知识的过程。的过程,是增殖新知识的过程。默认推理默认推理n默认推理是在知识不完全的情况下默认推理是在知识不完全的情况下假设某些条件已经具备假设某些条件已经具备所进行的推理,也称为所进行的推理,也称为缺省推理缺省推理。在推理过程中,如果发现。在推理过程中,如果发现原先的假设不正确,就撤消原来的假设以及由此假设所推出原先的假设不正确,就撤消原来的假设以及由此假设所推出的所有结论,重新按新情况进行推理。由于默认推理允许在的所有结论,重新按新情况进行推理。由于默认推理允许在推理过程中假设某些条件是成立的,因此解决了在一个不完推理过程中假设某些条件是成立的,因此解决了在一个不完备的知识集中进行推理的问题。备的知识集中进行推理的问题。n封闭世界假设:如果没有足够的证据证明某命题不成立,封闭世界假设:如果没有足够的证据证明某命题不成立,就假定该命题成立就假定该命题成立 不确定性推理确定性推理从知识的确定性)2(非单调性推理单调性推理从结论的单调性)3(非启发式推理启发式推理从启发性知识是否运用)4(直觉推理统计推理基于知识的推理从方法论的角度)5(推理过程涉及到推理过程涉及到求解方法求解方法和和求解策略求解策略。求解方法包括求解方法包括匹配方法匹配方法、不确定性的传递方法不确定性的传递方法求解策略包括求解策略包括推理方向推理方向、求解策略求解策略、限制策略限制策略等。等。指推理是求一个指推理是求一个解、所有解,还解、所有解,还是最优解。是最优解。为防止无穷的推理过为防止无穷的推理过程,以及由此带来的程,以及由此带来的时间和空间复杂性,时间和空间复杂性,限制策略是对推理的限制策略是对推理的深度、宽度、时间、深度、宽度、时间、空间等进行限制。空间等进行限制。推理方向分为推理方向分为正向推理、逆向推理、混合推理、双向推理正向推理、逆向推理、混合推理、双向推理四四种。种。无论哪一种推理,系统都具有无论哪一种推理,系统都具有知识库知识库、数据库数据库和和推理机推理机。正向推理需要解决的问题:正向推理需要解决的问题:1、确定匹配的方法、确定匹配的方法2、确定搜索策略、确定搜索策略3、消解冲突、消解冲突正向推理的缺点:盲目,效率低正向推理的缺点:盲目,效率低逆向推理的优点:逆向推理的优点:1、目标性强、目标性强2、有利于向用户提供解释、有利于向用户提供解释逆向推理的缺点:逆向推理的缺点:初始目标的选择有盲目性初始目标的选择有盲目性 开始开始提出假设提出假设该假设在数据库中?该假设在数据库中?该假设是证据?该假设是证据?在知识库中找出所有能导出该假设在知识库中找出所有能导出该假设的知识,形成适用知识集的知识,形成适用知识集KS从从KS中选出一条知识,并将该知识中选出一条知识,并将该知识的每一个的每一个运用条件都运用条件都作为作为新的假设新的假设目标目标退出退出有此事实?有此事实?询问用户询问用户NNNYYY该假设成立该假设成立该假设成立,并将此事实该假设成立,并将此事实存入数据库存入数据库还有假设?还有假设?NYY开始开始把初始已知事实送入把初始已知事实送入DBDB中包含问题的解中包含问题的解KB中有可适用的知识中有可适用的知识把把KB中所有的适用知识都选出送入中所有的适用知识都选出送入KSKS空?空?按冲突消解策略从按冲突消解策略从KS中选出一条知识进行推理中选出一条知识进行推理推出的是推出的是新知识新知识?将该新知识加入将该新知识加入DB成功,退出成功,退出失败,退出失败,退出用户补充新知识?用户补充新知识?把用户提供的新事实加入把用户提供的新事实加入DBNNNYYYYNYN逆向推理逆向推理-例例n有关知识有关知识规则规则1 1:IF IF 你丢了自行车钥匙,并且车胎没气你丢了自行车钥匙,并且车胎没气 THEN THEN 自行车不能骑自行车不能骑规则规则2 2:IF IF 自行车不能骑,并且你只有走路去自行车不能骑,并且你只有走路去 THEN THEN 你听课会迟到你听课会迟到事实事实1 1:你丢了自行车钥匙:你丢了自行车钥匙事实事实2 2:车胎没气:车胎没气n问题问题 “你听课会迟到?你听课会迟到?”逆向推理逆向推理-例例1.1.首先查找知识库,知该假设不是已有事实,但可由规则首先查找知识库,知该假设不是已有事实,但可由规则2 2导出,导出,于是将规则于是将规则2 2放入可用知识集,并将其两个前提条件放入可用知识集,并将其两个前提条件“自行车不自行车不能骑能骑”和和“你只有走路去你只有走路去”都作为新的假设放入假设集。都作为新的假设放入假设集。2.2.从假设集中取出假设从假设集中取出假设“自行车不能骑自行车不能骑”,它不是已有事实,但可,它不是已有事实,但可由规则由规则1 1导出,于是规则导出,于是规则1 1被放入可用知识集,并将其两个前提条被放入可用知识集,并将其两个前提条件件“你丢了自行车钥匙你丢了自行车钥匙”和和“车胎没气车胎没气”也作为新的假设放入假也作为新的假设放入假设集。设集。3.3.从假设集中取出假设从假设集中取出假设“你只有走路去你只有走路去”,此假设既不是已有事实,此假设既不是已有事实,也不能被任何一条规则导出,询问用户也不能被任何一条规则导出,询问用户“你只有走路去吗?你只有走路去吗?”,若用户回答若用户回答“是是”,则该假设成立,并被放入已有事实集。,则该假设成立,并被放入已有事实集。4.4.假设集中还有两个假设假设集中还有两个假设“你丢了自行车钥匙你丢了自行车钥匙”和和“车胎没气车胎没气”,它们都是已有事实,均为真。继续推理,它们都是已有事实,均为真。继续推理,假设集为空假设集为空,推理过程,推理过程结束,结束,“你听课会迟到你听课会迟到”得证。得证。混合推理是把正向推理和逆向推理结合起来,混合推理是把正向推理和逆向推理结合起来,吸取两种推理的优点。它通常适用以下吸取两种推理的优点。它通常适用以下3种情况:种情况:(1)已知事实不充分)已知事实不充分(2)由正向推理推出的可信度不高)由正向推理推出的可信度不高(3)希望得到更多的结论)希望得到更多的结论混合推理有两种方式:混合推理有两种方式:先正后逆先正后逆和和先逆后正先逆后正双向推理是指正向推理和逆向推理同时进行,在推理过双向推理是指正向推理和逆向推理同时进行,在推理过程的某步碰头。程的某步碰头。基本思想基本思想双向推理的难点是双向推理的难点是碰头碰头的判定。的判定。开始开始进行正向推理进行正向推理需要逆向推理?需要逆向推理?以正向推理所得的结以正向推理所得的结果作为假设进行逆向果作为假设进行逆向推理推理还需要正向推理?还需要正向推理?输出结果输出结果开始开始YYNN开始开始进行逆向推理进行逆向推理需要正向推理?需要正向推理?进行正向推理进行正向推理还需要逆向推理?还需要逆向推理?输出结果输出结果开始开始YYNN模式匹配是指对两个知识模式(如两个谓词公式、框模式匹配是指对两个知识模式(如两个谓词公式、框架或语义片段等)的比较与藕合,即检查这两个知识模式架或语义片段等)的比较与藕合,即检查这两个知识模式是否完全一致或近似一致。是否完全一致或近似一致。按匹配的近似程度划分,可分为按匹配的近似程度划分,可分为确定性匹配确定性匹配和和不确定不确定性匹配。性匹配。确定性匹配是指两个知识模式完全一致,或经确定性匹配是指两个知识模式完全一致,或经过变量代换后变得完全一致。例如:过变量代换后变得完全一致。例如:)(),(:)(),(:21ymanandyxfatherPLixiaosimanandLixiaosiLisifatherP不确定性匹配是指两个知识不确定性匹配是指两个知识模式不完全一致,但总体上模式不完全一致,但总体上它们的相似度在一定的限度它们的相似度在一定的限度内。内。定义定义3.1 置换(代换)置换(代换)代换是形如代换是形如 的有限集合。其中的有限集合。其中 是项是项 是是互不相同互不相同的变元;的变元;表示表示用用 代换代换 ,不允许不允许 与与 相同相同,也不允许变元也不允许变元 循环循环地地出现在另一个出现在另一个 中中。nnxtxtxt/,/,/2211nttt21,nxxx21,iixt/itixitjtixix根据定义根据定义 /,/)(,/zwybfxa/)(,/)(yxfxyg/)(,/)(yxfxag是代换是代换不是代换不是代换是代换是代换/)(,/)(yagfxag设有代换设有代换a/x,f(b)/y,u/z则对公式则对公式 EP(x,y,z)有有 EP(a,f(b),u)对公式对公式E运用代换运用代换s,记作,记作Es。Es称作公式称作公式E在代换在代换s下的下的例例(例示),它是(例示),它是E的的逻辑结论逻辑结论。设设是两个代换,则此两个代换的复合也是一个是两个代换,则此两个代换的复合也是一个代换代换,它是从,它是从删除以下两种元素删除以下两种元素后剩下的元素所构成的集合,记作后剩下的元素所构成的集合,记作 nnnnyuyuyuxtxtxt/,/,/,/,/22112211 niiiiiixxxyyuxtxti,/21 当当 nnnnyuyuyuxtxtxt/,/,/,/22112211 定义定义3.2 代换的复合代换的复合例如:例如:则则 zyybxayzxyf/,/,/,/)(zyybxbf/,/,/)(解释:解释:zyybxayzxyf/,/,/,/,/)(zyybxaybxbf/,/,/,/,/)(/,/,/)(/,/,/)(/,/,/,/,/,/)(/,/)(zbybxbfzyybxbfzbybxazyybxayzxzfyzxyf就是对一个公式就是对一个公式先运用先运用代换代换,然后,然后再运用再运用代换代换.!注意:即:)()(PP大家验证一下!大家验证一下!设有公式集设有公式集 ,若存在一个代换,若存在一个代换 使得使得则称则称 是公式集是公式集 的一个的一个合一合一,且称,且称 是是可合可合一的一的。NFFFF21,NFFF21,NFFF 21F一个公式集的合一一般来说一个公式集的合一一般来说不是唯一的不是唯一的例如公式集例如公式集有合一有合一),(,(),),(,(bbfzPbyfxPF ybxz/,/1ybzx/,/2zaybxa/,/,/3设设 是公式集是公式集 的一个合一,如果对的一个合一,如果对任一个任一个合一合一 都都存在一个代换存在一个代换 ,使得,使得则称则称 是公式集是公式集 的一个的一个最一般合一最一般合一。FF如前面提到的公式集如前面提到的公式集 是最一般合一,而是最一般合一,而 则不是最则不是最一般合一。一般合一。按照最一般合一的定义,有:按照最一般合一的定义,有:),(,(),),(,(bbfzPbyfxPF ybxz/,/1zaybxa/,/,/3/13za),(,(,),(,(31bbfaPFbbfzPF因此,对于一个公式集来说,如果存在多个合一,则其中因此,对于一个公式集来说,如果存在多个合一,则其中代代换数最少、限制最少、产生的例最具一般性的代换换数最少、限制最少、产生的例最具一般性的代换称为最一称为最一般合一。如:般合一。如:ybzx/,/2一般来说,一般来说,最一般合一也不是唯一的最一般合一也不是唯一的,同样同样是该公式集的一个最一般合一。是该公式集的一个最一般合一。差异集差异集:)(,)(,21bhzDafyD )(),(,(:),(:21bhafxPFzyxPF 求最一般合一算法:求最一般合一算法:(1)令)令 。这里,。这里,是欲求最一般是欲求最一般合一的公式集,合一的公式集,是空代换,它表示不做代换。是空代换,它表示不做代换。(2)若)若 只含一个表达式,则算法停止,只含一个表达式,则算法停止,就是最一就是最一般合一。般合一。(3)找出)找出 的的差异集差异集 。(4)若)若 中存在元素中存在元素 和和 ,其中,其中 是是变元变元,是项,是项,且且 不在不在 中出现,则置:中出现,则置:然后转向(然后转向(2)。)。(5)算法终止,)算法终止,的最一般合一不存在。的最一般合一不存在。kkFFk,0kFFkkFkDkDkxktkxktkt 1/11 kkxtFFxtkkkkkkkkkxF举例:求举例:求的最一般合一。的最一般合一。)(),(,(),(,(ufzfzPygfxaPF 11)(),(,(),(,(/,)1(0101000 kkufafaPygfxaPFzazazaDFFk令 21)(),(,(),(),(,(/)(,/)()(,)2(2121 kkufafaPygfafaPFxafzaxafafxD 31)(),(,()(),(,(),(),(,(/)(,/)(,/)(),()3(3232kkygfafaPygfafaPygfafaPFuygxafzauyguygD 在推理过程中,系统要不断地用当前已知事实与知识库中的知识进行在推理过程中,系统要不断地用当前已知事实与知识库中的知识进行匹配,此时可能发生以下三种情况:匹配,此时可能发生以下三种情况:(1)已知事实不能与知识库中的任何知识匹配)已知事实不能与知识库中的任何知识匹配(2)已知事实恰好与知识库中的一条知识匹配)已知事实恰好与知识库中的一条知识匹配(3)已知事实可与知识库中的多条知识匹配,或者多组已知事实可与知)已知事实可与知识库中的多条知识匹配,或者多组已知事实可与知识库中的某一条知识匹配,或者多组已知事实可与知识库中的多条知识匹识库中的某一条知识匹配,或者多组已知事实可与知识库中的多条知识匹配。配。处于第三种情况时,就发生处于第三种情况时,就发生冲突冲突。此时需要按一定的。此时需要按一定的消解策略消解策略解决冲解决冲突。突。冲突:多个知识都匹配成功。冲突:多个知识都匹配成功。冲突消解的基本思想都是对知识进行冲突消解的基本思想都是对知识进行排序排序。对于产生式系统,若出现以下情况就认为发生冲突:对于产生式系统,若出现以下情况就认为发生冲突:(1)对正向推理而言,如果有多条产生式规则的前件都和)对正向推理而言,如果有多条产生式规则的前件都和已知事实匹配,或者有多组已知事实都与同一条产生式规则的已知事实匹配,或者有多组已知事实都与同一条产生式规则的前件匹配;或者以上两种情况同时出现。前件匹配;或者以上两种情况同时出现。(2)对逆向推理而言,如果有多条产生式规则的后件都和)对逆向推理而言,如果有多条产生式规则的后件都和同一假设匹配,或者有多条产生式规则的后件可与多个假设匹同一假设匹配,或者有多条产生式规则的后件可与多个假设匹配。配。1、按针对性排序、按针对性排序 设有如下两条产生式规则:设有如下两条产生式规则:22121211:HthenBandandBandBifrHthenAandandAandAifrnn如果存在最一般合一,使得如果存在最一般合一,使得r1中的每个中的每个Ai都可以变成相都可以变成相应的应的Bi,如,如Ai=P(x,y),Bi=P(a,z)则称则称r2比比r1有更大的针对性,有更大的针对性,r1比比r2有更大的通用性。有更大的通用性。该策略选用针对性较强的产生式规则。该策略选用针对性较强的产生式规则。2、按已知事实的新鲜性排序、按已知事实的新鲜性排序 把数据库中后生成的事实称为新鲜的事实,该策略要求把数据库中后生成的事实称为新鲜的事实,该策略要求具有最大新鲜性的事实总是排在前面。具有最大新鲜性的事实总是排在前面。设规则设规则r1可与事实组可与事实组A匹配成功,规则匹配成功,规则r2可与事实组可与事实组B匹配成功,则匹配成功,则A和和B哪一组中的事实更新鲜,与它匹配的规哪一组中的事实更新鲜,与它匹配的规则就先被利用。则就先被利用。如何衡量如何衡量A和和B哪一组中的事实更新鲜呢?哪一组中的事实更新鲜呢?3、按匹配度排序、按匹配度排序4、根据领域问题的特点排序、根据领域问题的特点排序 先验知识、启发式知识先验知识、启发式知识5、按上下文限制排序、按上下文限制排序 把规则按照下上文分组,并只能选取组中的规则。把规则按照下上文分组,并只能选取组中的规则。6、按冗余限制排序、按冗余限制排序 冗余知识少的规则先推。冗余知识少的规则先推。7、按条件个数排序、按条件个数排序 条件少的规则先推。条件少的规则先推。尽量减少冲突的发生,使推理具有较高的效率尽量减少冲突的发生,使推理具有较高的效率3.3 自然演绎推理自然演绎推理自然演绎推理就是从一组已知为真的事实出发,自然演绎推理就是从一组已知为真的事实出发,直接直接运用运用经经典逻辑的推理规则典逻辑的推理规则推出结论的过程。推出结论的过程。推理规则包括:推理规则包括:1、假言推理、假言推理2、拒取式推理、拒取式推理3、P规则:在推理的任何步骤都可引入规则:在推理的任何步骤都可引入前提前提4、T规则:推理时,如果前面步骤有一个或多个公式规则:推理时,如果前面步骤有一个或多个公式永真蕴永真蕴含含公式公式S(逻辑结论逻辑结论),则可把公式),则可把公式S引入推理过程中。引入推理过程中。QQPP,PQQP ,例例3.1 已知下述事实:已知下述事实:A,B,AC,BC D,D Q 求证:求证:Q为真为真证明:证明:A,A C C P规则及假言推理规则及假言推理 B,C BC 合取合取 BC,BCD D T规则及假言推理规则及假言推理 D,DQ Q T规则及假言推理规则及假言推理思考题:思考题:所有人都是必死的;所有人都是必死的;苏格拉底是人;苏格拉底是人;求证:苏格拉底是必死的。求证:苏格拉底是必死的。自然演绎推理的优点:自然演绎推理的优点:表达定理证明过程表达定理证明过程自然自然,容易理解,而且拥有,容易理解,而且拥有丰富的推丰富的推理规则理规则,推理过程,推理过程灵活灵活,便于在它的推理规则中嵌入,便于在它的推理规则中嵌入领域领域启发式知识启发式知识。自然演绎推理的缺点:自然演绎推理的缺点:容易产生容易产生组合爆炸组合爆炸中间结论呈指数级增长。中间结论呈指数级增长。3.4 归结演绎推理归结演绎推理 要证明要证明PQ永真,需要证明它在任何个体域上所永真,需要证明它在任何个体域上所有可能的解释都是永真的,这是难以实现的。采用有可能的解释都是永真的,这是难以实现的。采用反反证法证法的思想,只要证明的思想,只要证明P Q永假(不可满足)永假(不可满足)即即可。可。这是因为:这是因为:PQ PQ(PQ)P Q海伯伦(海伯伦(HerbrandHerbrand)和)和鲁宾逊鲁宾逊(RobinsonRobinson)在这)在这个方向上先后作了卓越的研究工作。首先,由海伯个方向上先后作了卓越的研究工作。首先,由海伯伦提出的伦提出的H H域(海伯伦域)和海伯伦定理,为自动定域(海伯伦域)和海伯伦定理,为自动定理证明奠定了理论基础;然后,由鲁宾逊提出的理证明奠定了理论基础;然后,由鲁宾逊提出的归归结原理(消解原理)结原理(消解原理)则使机器定理证明成为可能。则使机器定理证明成为可能。在谓词公式中,把原子谓词公式及其否定统称为在谓词公式中,把原子谓词公式及其否定统称为文字文字。例如:例如:P(x,y)和和 Q(x)都是文字。都是文字。定义定义 任何文字的任何文字的析取式析取式称为子句。称为子句。例如:例如:P(x,y)Q(x)是子句;是子句;P(x,y)(Q(x)R(y)不是子句。不是子句。定义定义 不包含任何文字的子句称为空子句,简记为不包含任何文字的子句称为空子句,简记为NIL。空子句是永假的,是不可满足的空子句是永假的,是不可满足的。子句的集合称为子句的集合称为子句集子句集。在谓词逻辑中,谓词公式可以通过等价关系及推理规在谓词逻辑中,谓词公式可以通过等价关系及推理规则化成相应的子句集。则化成相应的子句集。把谓词公式转化为子句集的步骤:把谓词公式转化为子句集的步骤:(1)(1)消去蕴涵符号消去蕴涵符号(2)(2)内移否定符号内移否定符号 (3)(3)对变元更名:使对变元更名:使不同量词约束的不同量词约束的变元变元不同名不同名(4)(4)消去存在量词:个体常量、消去存在量词:个体常量、SkolemSkolem函数代换函数代换 (5)(5)全称量词前束化全称量词前束化 (6)(6)化为化为SkolemSkolem标准型:合取范式标准型:合取范式(7)(7)消去全称量词消去全称量词 (8)(8)对变元更名:使对变元更名:使不同子句中的不同子句中的变元不同名变元不同名(9)(9)消去合取词:消去合取词:子句集子句集例如:例如:(x)(y)P(x,y)(y)(Q(x,y)R(x,y)(x)(y)P(x,y)(y)(Q(x,y)R(x,y)(2)(x)(y)P(x,y)(y)(Q(x,y)R(x,y)(3)(x)(y)P(x,y)(z)(Q(x,z)R(x,z)(4)(x)(P(x,f(x)(Q(x,g(x)R(x,g(x)(5)全称量词已经前束化全称量词已经前束化(6)(x)(P(x,f(x)Q(x,g(x)(P(x,f(x)R(x,g(x)(7)(P(x,f(x)Q(x,g(x)(P(x,f(x)R(x,g(x)(8)(P(x,f(x)(Q(x,g(x)(P(y,f(y)R(y,g(y)(1)(9)P(x,f(x)Q(x,g(x),P(y,f(y)R(y,g(y)例例1:求谓词公式:求谓词公式G=x y z(P(x,y)R(x,y,z)(Q(x,z)R(x,y,z)的子句集。的子句集。解:已经是前束范式,并且不含连接词解:已经是前束范式,并且不含连接词 。由于存在量词。由于存在量词y,z都在全称量词都在全称量词x的辖域中,所以将的辖域中,所以将y,z分别用分别用Skolem函数函数f(x)、g(x)代替。代替。x(P(x,f(x)R(x,f(x),g(x)(Q(x,g(x)R(x,f(x),g(x)该谓词公式已经是该谓词公式已经是合取范式合取范式了,消去全称量词、对变元更名了,消去全称量词、对变元更名、消去合取词,得到谓词公式、消去合取词,得到谓词公式G的的子句集子句集是是 P(x,f(x)R(x,f(x),g(x),Q(y,g(y)R(y,f(y),g(y)例例2:求谓词公式的子句集:求谓词公式的子句集:x(yP(x,y)y(Q(x,y)R(x,y)解:解:x(yP(x,y)y(Q(x,y)R(x,y)=x(yP(x,y)y(Q(x,y)R(x,y)=x(y P(x,y)y(Q(x,y)R(x,y)=x(y P(x,y)z(Q(x,z)R(x,z)=x(P(x,f(x)(Q(x,g(x)R(x,g(x)=x(P(x,f(x)Q(x,g(x)(P(x,f(x)R(x,g(x)从而该谓词公式的子句集是从而该谓词公式的子句集是 P(x,f(x)(Q(x,g(x),P(y,f(y)R(y,g(y)转化要点:转化要点:1、第一步应先消去蕴涵符号,再内移否定符号等其它工作;、第一步应先消去蕴涵符号,再内移否定符号等其它工作;2、先内移否定符号,再消去量词;、先内移否定符号,再消去量词;3、先消存在量词,再消全称量词。、先消存在量词,再消全称量词。定理定理3.1 设有谓词公式设有谓词公式F,其标准形的子句集为,其标准形的子句集为S,则,则F不不可满足可满足的的充要条件充要条件是是S不可满足不可满足。(注意:。(注意:F和和S并不等并不等价!价!存在量词消去、变元更名)存在量词消去、变元更名)因此,要想证明因此,要想证明F不可满足,只需证明不可满足,只需证明S不可满足即可,鲁不可满足即可,鲁滨逊提出的归结原理就是用来解决这一问题的。滨逊提出的归结原理就是用来解决这一问题的。为提高判定子句集不可满足的有效性,鲁宾逊于为提高判定子句集不可满足的有效性,鲁宾逊于1965年年提出了归结提出了归结(Resolution)原理,也称为原理,也称为消解原理消解原理。由谓词转化子句集的过程可以看出,在子句集中各子句由谓词转化子句集的过程可以看出,在子句集中各子句之间是之间是合取合取关系,其中只要有一个子句不可满足,则子句集关系,其中只要有一个子句不可满足,则子句集就不可满足。空子句是不可满足的,就不可满足。空子句是不可满足的,若一个子句集含有一个若一个子句集含有一个空子句(该子句集中有矛盾),子句集一定是不可满足的空子句(该子句集中有矛盾),子句集一定是不可满足的。鲁宾逊归结原理的基本是:检查子句集鲁宾逊归结原理的基本是:检查子句集S是否包含空子句,是否包含空子句,若包含,则若包含,则S不可满足;若不包含,就在子句集中选择合适的不可满足;若不包含,就在子句集中选择合适的子句进行归结,一旦通过子句进行归结,一旦通过归结归结推出推出空子句空子句,就说明子句集,就说明子句集S是是不可满足的。不可满足的。定义定义3.18 若若P是原子谓词公式,则称是原子谓词公式,则称P和和 P为为互补文字互补文字。设设C1C1和和C2C2是子句集中任意二个子句,如果是子句集中任意二个子句,如果C1C1中的文字中的文字L1L1和和C2C2中的文字中的文字L2L2互补,那么从互补,那么从C1C1和和C2C2中分别消去中分别消去L1L1和和L2L2,并对并对C1C1和和C2C2的剩余部分析取,构成一个新的子句的剩余部分析取,构成一个新的子句C12C12,则称,则称这一过程为这一过程为归结归结,称,称C12C12为为C1C1和和C2C2的的归结式归结式,C1C1和和C2C2是是C12C12的的亲本子句亲本子句。例:例:C1=C1=PQPQ,C2=C2=QRQR,C3=PC3=P C12=C12=PRPR,C123=RC123=R PQPQ QRQR PRPRP PR 归结树归结树定理定理3.2 归结式归结式C12是其亲本子句是其亲本子句C1和和C2的的逻辑结论逻辑结论,即:,即:C1C2 C12如何证明?如何证明?推论推论1:设:设C1和和C2是子句集是子句集S中的两个子句,中的两个子句,C12是它们的是它们的归结式,若用归结式,若用C12代替代替C1和和C2后得到新子句集后得到新子句集S1,则,则 S1的不可满足性的不可满足性 S的不可满足性的不可满足性推论推论2:设:设C1和和C2是子句集是子句集S中的两个子句,中的两个子句,C12是它们的是它们的归结式,若用归结式,若用C12加入加入S中后,得到新子句集中后,得到新子句集S1,则,则 S1的不可满足性的不可满足性 S的不可满足性的不可满足性谓词逻辑中的归结原理谓词逻辑中的归结原理在谓词逻辑情况下,由于子句中含有变量,不能像命在谓词逻辑情况下,由于子句中含有变量,不能像命题逻辑那样直接发现和消去互补文字,往往需对题逻辑那样直接发现和消去互补文字,往往需对潜在的潜在的互补文字互补文字先作先作变量代换和合一变量代换和合一处理,才能用于归结。处理,才能用于归结。例如有如下两个子句:例如有如下两个子句:C1=P(x)Q(x)C1=P(x)Q(x)C2=C2=P(a)R(y)P(a)R(y)用用最一般合一最一般合一 =a/x=a/x对两个子句分别进行代换:对两个子句分别进行代换:C1C1 =P(a)=P(a)Q(a)Q(a)C2 C2 =P(a)R(y)P(a)R(y)可得归结式:可得归结式:Q(a)Q(a)R(y)R(y)若若C2=C2=P(a)R(P(a)R(x x)又该如何?又该如何?定义定义3.20 设设C1和和C2是两个没有相同变元的子句,是两个没有相同变元的子句,L1和和L2分别是分别是C1和和C2中的文字,若中的文字,若 是是L1L1和和 L2L2的的最一般合一最一般合一,则称则称 C12=(C1C12=(C1-L1-L1)(C2)(C2-L2-L2)是是C1C1和和C2C2的二元归结式,的二元归结式,L1L1和和L2L2称为归结式上的文字。称为归结式上的文字。如果在参加归结的如果在参加归结的子句内部子句内部含有可合一的文字,则在进含有可合一的文字,则在进行归结前应对这些文字先进行行归结前应对这些文字先进行合一合一。例如:例如:C1=P(x)P(f(a)Q(x)C1=P(x)P(f(a)Q(x)C2=C2=P(y)R(b)P(y)R(b)C1C1中中P(x)P(x)和和P(f(a)P(f(a)可合一,用其最一般合一可合一,用其最一般合一=f(a)/x=f(a)/x进进行代换,得:行代换,得:C1C1=P(f(a)Q(f(a)=P(f(a)Q(f(a)C1C1 和和C2C2归结得归结得C12=Q(f(a)R(b)C12=Q(f(a)R(b)注意注意:这样多做了一次代换,相当于对:这样多做了一次代换,相当于对C1C1做了更严格的限制,做了更严格的限制,有可能存在归结不出结果的可能性。有可能存在归结不出结果的可能性。一般来说:若子句一般来说:若子句C中有两个或两个以上的文字中有两个或两个以上的文字具有最一般的合一具有最一般的合一,则称,则称C C 为子句为子句C C的的因子因子。如果如果C C 是一个单文字,则称为单因子。是一个单文字,则称为单因子。定义定义3.21 子句子句C1和和C2的归结式是下列二元归结式的归结式是下列二元归结式之一:之一:(1)C1和和C2的二元归结式;的二元归结式;(2)C1和和C2的的因子因子C2C2 2 2的的二元归结式;二元归结式;(3)C1的的因子因子C1C1 1 1和和C2的的二元归结式;二元归结式;(4)C1的的因子因子C1C1 1 1和和C2的的因子因子C2C2 2 2的的二元归结二元归结式。式。对于谓词逻辑,定理对于谓词逻辑,定理3.2仍然适用。仍然适用。归结演绎的完备性归结演绎的完备性从从不可满足不可满足的意义上说,基于归结的演绎方法是的意义上说,基于归结的演绎方法是完备的,即若子句集完备的,即若子句集S S不可满足,就必定存在一个从不可满足,就必定存在一个从S S到空子句的归结演绎;反之,若存在一个从到空子句的归结演绎;反之,若存在一个从S S到空子到空子句的归结演绎,则句的归结演绎,则S S必定是不可满足的。关于归结演必定是不可满足的。关于归结演绎的完备性可用海伯伦定理进行证明,因此从这个意绎的完备性可用海伯伦定理进行证明,因此从这个意义上讲,归结原理是建立在海伯伦定理之上的。不过义上讲,归结原理是建立在海伯伦定理之上的。不过归结原理并不能用于解决子句集不可满足性的不可判归结原理并不能用于解决子句集不可满足性的不可判定问题定问题,即对于,即对于永真永真和和可满足可满足的子句集,判定过程将的子句集,判定过程将无休止地进行下去,得不到任何结果。无休止地进行下去,得不到任何结果。证明证明Q是是P1,P2Pn的逻辑结论,的逻辑结论,即:即:P1P2 PnQ只需证明只需证明(P1P2 Pn Q)是不可满足是不可满足的。的。因为因为 (P1P2 Pn Q)(P1P2 Pn)Q)(P1P2 Pn)Q只需证明只需证明子句集子句集P1,P2,Pn,Q是不是不可满足的。可满足的。对子句集中的子句相互归结,直到归结出对子句集中的子句相互归结,直到归结出空子句空子句,这个过程就是这个过程就是归结反演归结反演。设设F为已知前提的公式集,为已知前提的公式集,Q为目标公式,用归结反演证明为目标公式,用归结反演证明Q为真的步骤:为真的步骤:(1)否定否定Q,得到,得到 Q;(2)把)把 Q并入到公式集并入到公式集F中,得到中,得到F,Q;(3)把公式集)把公式集F,Q化为子句集化为子句集S(P126127););(4)应用归结原理对子句集)应用归结原理对子句集S中的子句进行归结,并把每次中的子句进行归结,并把每次得到的归结式放入得到的归结式放入S中。如此反复,若出现中。如此反复,若出现空子句空子句,就停止归,就停止归结,此时就证明了结,此时就证明了Q为真。为真。例例1:求证求证:G是是A1和和A2的逻辑结论的逻辑结论 A1:x(P(x)(Q(x)R(x)A2:x(P(x)S(x)G:x(S(x)R(x)证证:P(x)Q(x).从从A1变换变换 P(y)R(y).从从A1变换变换 P(a).从从A2变换变换 S(a).从从A2变换变换 S(z)R(z).结论的否定结论的否定 R(a).归结归结a/y R(a).归结归结a/z NIL.归结归结 得证得证.例例2:设已知设已知:(1)能阅读者是识字的能阅读者是识字的;(2)海豚不识字海豚不识字;(3)有些海豚是聪明的有些海豚是聪明的;求证求证:有些聪明者并不能阅读有些聪明者并不能阅读.证证:定义如下命题定义如下命题:R(x):x能阅读能阅读;L(x):x识字识字;I(x):x是聪明的是聪明的;D(x):x是海豚是海豚;把已知条件及求证结论翻译成谓词公式为把已知条件及求证结论翻译成谓词公式为 x(R(x)L(x).已知已知 x(D(x)L(x).已知已知 x(D(x)I(x).已知已知 x(I(x)R(x).求证结论求证结论 将将已知条件已知条件,求证结论的反求证结论的反化成子句集化成子句集 R(x)L(x)D(y)L(y)D(a)I(a)I(z)R(z)L(a).2,3归结归结a/y R(a).1,6归结归结a/x R(a).4,5归结归结a/z NIL.7,8归结归结 得证得证.例例3.17“快乐学生快乐学生”问题问题 假设:任何通过计算机考试并获奖的人都是快假设:任何通过计算机考试并获奖的人都是快乐的,任何肯学习或幸运的人都可以通过所有考试,乐的,任何肯学习或幸运的人都可以通过所有考试,张不肯学习但他是幸运的,任何幸运的人都能获奖。张不肯学习但他是幸运的,任何幸运的人都能获奖。求证:张是快乐的。求证:张是快乐的。解:先定义谓词:解:先定义谓词:Pass(x,y)x可以通过可以通过y考试考试 Win(x,prize)x能获得奖励能获得奖励 Study(x)x肯学习肯学习 Happy(x)x是快乐的是快乐的 Lucky(x)x是幸运的是幸运的再将问题用谓词表示如下:再将问题用谓词表示如下:“任何通过计算机考试并奖的人都是快乐的任何通过计算机考试并奖的人都是快乐的”(x)(Pass(x,computer)Win(x,prize)Happy(x)“任何肯学习或幸运的人都可以通过所有考试任何肯学习或幸运的人都可以通过所有考试”(x)(y)(Study(x)Lucky(x)Pass(x,y)“张不肯学习但他是幸运的张不肯学习但他是幸运的”Study(zhang)Lucky(zhang)“任何幸运的人都能获奖任何幸运的人都能获奖”(x)(Lucky(x)Win(x,prize)结论结论“张是快乐的张是快乐的”的否定的否定 Happy(zhang)将上述谓词公式转化为子句集如下:将上述谓词公式转化为子句集如下:(1)Pass(x,computer)Win(x,prize)Happy(x)(2)Study(y)Pass(y,z)(3)Lucky(u)Pass(u,v)(4)Study(zhang)(5)Lucky(zhang)(6)Lucky(w)Win(w,prize)(7)Happy(zhang)(结论的否定结论的否定)Pass(x,computer)Win(x,prize)Happy(x)Lucky(w)Win(w,prize)Pass(w,Computer)Happy(w)Lucky(w)Happy(zhang)Lucky(zhang)Pass(zhang,Computer)Lucky(zhang)Pass(zhang,Computer)Lucky(u)Pass(u,v)Lucky(zhang)Lucky(zhang)NILw/xzhang/wzhang/u,computer/v 例例3.18“激动人心的生活激动人心的生活”问题问题 假设:所有不贫穷并且聪明的人都是快乐的,假设:所有不贫穷并且聪明的人都是快乐的,那些看书的人是聪明的。李明能看书且不贫穷,快那些看书的人是聪明的。李明能看书且不贫穷,快乐的人过着激动人心的生活。乐的人过着激动人心的生活。求证:李明过着激动人心的生活。求证:李明过着激动人心的生活。解:先定义谓词:解:先定义谓词:Poor(x)x是贫穷的是贫穷的 Smart(x)x是聪明的是聪明的 Happy(x)x是快乐的是快乐的 Read(x)x能看书能看书 Exciting(x)x过着激动人心的生活过着激动人心的生活 再将问题用谓词表示如下:再将问题用谓词表示如下:“所有不贫穷并且聪明的人都是快乐的所有不贫穷并且聪明的人都是快乐的”(x)(Poor(x)Smart(x)Happy(x)“那些看书的人是聪明的那些看书的人是聪明的”(y)(Read(y)Smart(y)“李明能看书且不贫穷李明能看书且不贫穷”Read(Liming)Poor(Liming)“快乐的人过着激动人心的生活快乐的人过着激动人心的生活”(z)(Happy(z)Exciting(z)目标目标“李明过着激动人心的生活李明过着激动人心的生活”的否定的否定 Exciting(Liming)将上述谓词公式转化为子句集如下:将上述谓词公式转化为子句集如下:(1)Poor(x)Smart(x)Happy(x)(2)Read(y)Smart(y)(3)Read(Liming)(4)Poor(Liming)(5)Happy(z)Exciting(z)(6)Exciting(Liming)(结论的否定结论的否定)Exciting(Liming)Happy(z)Exciting(z)Happy(Liming)Happy(x)Smart(x)Happy(x)Poor(Liming)Smart(Liming)Read(y)Smart(y)Poor(Liming)Read(Liming)Poor(Liming)Read(Liming)Read(Liming)NILLiming/zLiming/xLiming/y求问题的答案与定理证明类似,其步骤为:求问题的答案与定理证明类似,其步骤为:(1)用谓词公式表示已知前提,并化为子句集)用谓词公式表示已知前提,并化为子句集S;(2)用谓词公式表示待求解,并将其)用谓词公式表示待求解,并将其否定否定与谓词与谓词ANSWER构构成成析取式析取式(同一个子句);(同一个子句);ANSWER是一个为求解而设定的谓是一个为求解而设定的谓词,词,其变元必须与问题公式的变元一致其变元必须与问题公式的变元一致;(用;(用重言式重言式也可)也可)(3)把此析取式化为子句集,并把该子句集假如到子句集)把此析取式化为子句集,并把该子句集假如到子句集S中,得到子句集中,得到子句集S;(4)对对S应用归结原理进行归结;应用归结原理进行归结;(5)若得到归结式)若得到归结式ANSWER,则答案就在,则答案就在ANSWER中。中。例例 设设A,B,C三人中有人从不说真话,也有人从不三人中有人从不说真话,也有人从不说假话。某人向这三人分别提出同一个问题:谁说假话。某人向这三人分别提出同一个问题:谁是说谎者?是说谎者?A答:答:“B和和C都是说谎者都是说谎者”;B答:答:“A和和C都是说谎者都是说谎者”;C答:答:“A和和B中至少有中至少有一个是说谎者一个是说谎者”。求谁是老实人,谁是说谎者?。求谁是老实人,谁是说谎者?解:设用解:设用T(x)表示表示x说真话。说真话。如果如果A说的是真话,则说的是真话,则T(A)T(B)T(C)如果如果A说的是假话,则说的是假话,则T(A)T(B)T(C)对对B和和C说的话作相同处理,可得:说的话作相同处理,可得:T(B)T(A)T(C)T(B)T(A)T(C)T(C)T(A)T(B)T(C)T(A)T(B)把上述公式化成子句集,得到把上述公式化成子句集,得到S:(1)T(A)T(B)(2)T(A)T(C)(3)T(C)T(A)T(B)(4)T(B)T(C)(5)T(C)T(A)T(B)(6)T(A)T(C)(7)T(B)T(C)下面先求谁是老实人。把下面先求谁是老实人。把T(x)Answer(x)并入并入S得到得到S1。即多。即多一个子句:一个子句:(8)T(x)Answer(x)应用归结原理对应用归结原理对S1进行归结:进行归结:(9)T(A)T(C)(1)和和(7)归结归结(10)T(C)(6)和和(9)归结归结(11)Answer(C)(8)和和(10)归结归结所以所以C是老实人,即是老实人,即C从不说假话。从不说假话。下面证下面证A和和B不是老实人。不是老实人。设设A不是老实人,则有不是老实人,则有T(A),把它否定并入,把它否定并入S中,得到中,得到子句集子句集S2,即,即S2比比S多如下子句:多如下子句:(8)(T(A),即即T(A)应用归结原理对应用归结原理对S2进行归结:进行归结:(9)T(A)T(C)(1)和和(7)归结归结(10)T(A)(2)和和(9)归结归结(11)NIL(8)和和(10)归结归结所以所以A不是老实人。不是老实人。同理,可证明同理,可证明B也不是老实人。也不是老实人。n归结时,并不要求把子句集中所有的子句都用到。归结时,并不要求把子句集中所有的子句都用到。n在归结过程中,一个子句可以多次被用来进行归结。在归结过程中,一个子句可以多次被用来进行归结。例例3.24 已知:已知:“张和李是同班同学,如果张和李是同班同学,如果x和和y是同班同学,则是同班同学,则x的教室也是的教室也是y的教室,现在张在的教室,现在张在302教室上课。教室上课。”问:问:“现在李在哪个教室上课?现在李在哪个教室上课?”解:首先定义谓词:解:首先定义谓词:C(x,y)x和和y是同班同学;是同班同学;At(x,u)x在在u教室上课。教室上课。把已知前提用谓词公式表示如下:把已知前提用谓词公式表示如下:C(zhang,li)(x)(y)(u)(C(x,y)At(x,u)At(y,u)At(zhang,302)把目标的否定用谓词公式表示如下:把目标的否定用谓词公式表示如下:(v)At(li,v)把上述公式化为子句集:把上述公式化为子句集:C(zhang,li)C(x,y)At(x,u)At(y,u)At(zhang,302)把目标的否定化成子句式,并用重言式把目标的否定化成子句式,并用重言式 At(li,v)At(li,v)代替之。代替之。把此重言式加入前提子句集中,得到一个新的子句集,把此重言式加入前提子句集中,得到一个新的子句集,对这个新的子句集,应用归结原理求出其证明树。其求解过对这个新的子句集,应用归结原理求出其证明树。其求解过程如下图所示。程如下图所示。该证明树的根子句就是所求的答案,即该证明树的根子句就是所求的答案,即“李明在李明在302教室教室”。At(li,v)At(li,v)C(x,y)At(x,u)At(y,u)At(li,v)C(x,li)At(x,v)C(zhang,li)At(zhang,v)At(li,v)At(zhang,302)At(li,302)li/y,v/uZhang/x302/v1、计算机进行归结的一般过程、计算机进行归结的一般过程设子句集设子句集S=C1,C2,C3,C4,计算机对此子句集进行归,计算机对此子句集进行归结的一般过程是:结的一般过程是:(1)从子句)从子句C1开始,逐个与开始,逐个与C2,C3,C4进行比较,若能归进行比较,若能归结,就求出归结式。然后用结,就求出归结式。然后用C2与与C3、C4进行归结,最后进行归结,最后C3和和C4进行归结。经过这一轮的比较和归结后,就得到一组归结式,进行归结。经过这一轮的比较和归结后,就得到一组归结式,称为称为第一级归结式第一级归结式。(2)再从)再从C1开始,用开始,用S中的子句中的子句分别与第一级归结式中的子分别与第一级归结式中的子句逐个地比较、归结,这样又会得到一组归结式,称为句逐个地比较、归结,这样又会得到一组归结式,称为第二级第二级归结式归结式。(3)仍然从)仍然从C1开始,用开始,用S中的子句及第一级归结式中的子句中的子句及第一级归结式中的子句分别与第二级归结式中的子句逐个地比较、归结,得到第三级分别与第二级归结式中的子句逐个地比较、归结,得到第三级归结式。归结式。如此继续,直到出现空子句或者不能再继续归结为止。如此继续,直到出现空子句或者不能再继续归结为止。例例 设有子句集:设有子句集:S=P,R,P Q,Q R归结过程:归结过程:S:(1)P (2)R (3)P Q (4)Q RS1:(5)Q (6)Q (7)P RS2:(8)R (9)P (10)P (11)RS3:(12)NIL事实上,事实上,(5)(6)归结就可以得到归结就可以得到NIL2、归结策略、归结策略 为了尽量避免造成时空浪费,提高归结的效率,需要对归为了尽量避免造成时空浪费,提高归结的效率,需要对归结过程进行适当的控制。结过程进行适当的控制。归结策略分为两大类:归结策略分为两大类:删除策略删除策略:删除某些无用子句,缩小归结的范围:删除某些无用子句,缩小归结的范围 限制策略限制策略:对参加归结的子句进行限制,减小归结的:对参加归结的子句进行限制,减小归结的 盲目性盲目性2、删除策略、删除策略删除策略是指在归结过程中把子句集的无用的子句删除掉这删除策略是指在归结过程中把子句集的无用的子句删除掉这样就会样就会缩小寻找范围,
展开阅读全文
相关资源
正为您匹配相似的精品文档
相关搜索

最新文档


当前位置:首页 > 办公文档 > 教学培训


copyright@ 2023-2025  zhuangpeitu.com 装配图网版权所有   联系电话:18123376007

备案号:ICP2024067431-1 川公网安备51140202000466号


本站为文档C2C交易模式,即用户上传的文档直接被用户下载,本站只是中间服务平台,本站所有文档下载所得的收益归上传人(含作者)所有。装配图网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私,请立即通知装配图网,我们立即给予删除!