没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记185(2007)3-15www.elsevier.com/locate/entcs压缩命题反驳Hasan Amjad剑桥大学计算机实验室摘要我们报告的初步结果缩短命题解决反驳证明。这在加速大型命题反驳的演绎重建(在定理证明器中)中有应用,例如由SAT求解器产生的那些。关键词:证明验证,命题反驳,证明压缩1引言近年来,强大的SAT求解器[6]的出现促进了命题证明在验证中的使用[4]。最近,可以提供不满意性证明的完整SAT求解器[13]允许人们通过使用SAT求解器来证明不满意性来解决有效性。完整SAT求解器的一个应用是使用它们来有效地找到大型问题的证明,然后相对便宜地在演绎环境中验证证明,例如定理证明器。从定理证明社区的角度来看,SAT求解器成为命题证明的强大预言机这个应用程序是稳步获得地面定理证明圈[7,12]。这一应用的主要障碍是,所提出的证据的篇幅往往大得令人望而却步,无法以演绎方式引入在本文中,我们提出了一些初步的结果,缩短这样的证明之前,演绎重建。SAT求解器产生的不满足性证明是一个归结反驳,通过读取求解器维护的隐式蕴涵图来创建。这种读操作是在后台完成的,以减少内存使用开销。目前大多数流行的SAT求解器都是基于DPLL算法的一些增强[5]1电子邮件:ha227@cl.cam.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2007.05.0254H. Amjad/电子笔记在理论计算机科学185(2007)3DPLL执行回溯搜索以获得满意的分配,并丢弃搜索的不成功分支。因此,由于SAT求解器的证明生成的非线性性质,最终证明可以预期包含冗余分支,并且在分支内,冗余应用解析规则。幸运的是,一个简单的反向遍历的分辨率图,即,从最后的空子句开始,再回到最初的问题子句,这样就可以发现实际使用了哪些分支。其他的可以丢弃。不那么幸运的是,分支中出现的冗余规则不那么容易被发现,因为冗余是由证明的全局方面引起的。我们表明,通过分析证明的整体结构,往往可以得到更短的证明。下一节给出了一些基本的定义。然后,我们在§ 3中给出了主要算法,然后在§ 4中给出了实验结果。最后,我们简要介绍了相关的工作和未来发展的一些想法2个房间输入问题是在合取范式(CNF),这是一个迭代的子句合取。子句是文字的迭代析取。一个字面量要么是一个原子命题(或原子),要么是一个否定的原子。原子由数字表示,文字由每个原子与布尔极性指示符配对表示。出现在初始问题中的子句将被称为初始子句。通过合取和析取的结合性和交换性,子句的顺序和子句内文字的顺序是不重要的。因此,我们可以经常把它们称为集合而不是公式。一个子句被认为包含在它自身的任何子集中。有n个元素的子句是n子句。1-子句被称为单元。决议规则是pC<$pDCD其中p是一个原子,C和D是(可能是空的)子句。 前提中的两个分句是先行分句,规则的后件分句叫做一个习得的从句,或一个预解式。被分解的原子p称为枢轴。任何同时出现在C和D中的文字都可以在预解式中安全地表示为一次出现,并且被称为合并。在前件中出现的非主元文字是它们在预解式中出现的前导祖先关系由前导关系的传递闭包表示。继承人和后代的定义类似。归结证明是一个仅由归结规则组成的推导,使得叶子中的所有先行词都是初始子句。如果空子句是在某点导出的,则证明是反驳。从视觉上看,证明看起来像一棵树。由于一个子句可能在证明中被多次使用,所以每次这样的使用都被称为子句出现,通过将子句与出现计数配对来表示。子句出现中的文字称为文字出现,通过将每个文字与子句出现配对来给出H. Amjad/电子笔记在理论计算机科学185(2007)35我们通过通常的词典结构获得子句、文字及其出现的全序由于初始子句或根子句可能被使用多次,因此证明被表示为DAG,其中子句作为节点,并且边从先行项到预解项。任何初始子句都是源。理想情况下,在反驳中,只有一个水槽,空子句。然而,由于证明搜索的性质,未使用的解式也可能作为sink出现。这样的DAG被称为分辨率图。3该算法众所周知,没有有效的确定性算法来缩短仅使用归结证明的归结证明。我们的方法依赖于对证明中的决议进行启发式重新排序,希望找到一个更短的证明,通过在所有决议都被处理之前导出3.1概述主算法有四个阶段,中间的两个阶段可以迭代:(i) 将SAT求解器证明解析为解析图。(ii) 隐式地从图中构造解析树,跟踪作为被解析的文字的祖先的任何文字之间的链接。使用一些启发式的链接排名。(iii) 将链接转换为分辨率,按照链接排名的顺序,生成新的分辨率图。每次解决后执行包容检查在派生空子句时完成(iv) 选择定理证明器中的简化证明验证。第一阶段简单地读入SAT求解器证明,并构造一个解析图的隐式表示,作为一个解析列表现在我们详细地看一下其余的每个阶段。3.2查找链接第一步是开发一个比解决方案列表更适合全局分析的证明表示。我们从连接方法文献[2,10]中借用了连接矩阵[3我们希望跟踪初始子句中的文字,这些文字的后代在原始证明中相互解决。这样的文字被称为链接。 因此,链接只是一对文字出现。为了效率,一些关于相应的解析操作的元级信息也与链接一起记录,例如枢轴,任何合并的文字等。每个链接都有一个相关联的序列号,对应于原始证明中应用其底层解析的时间。以文字出现为节点,以链接为边的图称为链接图。这个图G被构造如下:6H. Amjad/电子笔记在理论计算机科学185(2007)3C1:{-x,y}C2:{-x,-y}C3:{-x}C0:{x}假Fig. 1. §3.2示例的分辨率图(i) 从原始证明中获得归结规则应用的集合,并按照时间升序对它们进行拓扑排序(即,在原始证明中应用的顺序)。这给出了决议列表L(ii) 将每个初始子句C的出现计数#C初始化为0。(iii) 初始化每个初始子句C ={p0,.,pn},以{(p0,{(p0,(C,#C))}), . . ,(pn,{(pn,(C,#C))})}{(p,)|p∈/C}注意(C,#C)是一个子句出现,因此(p,(C,#C))是一个文字出现。因此,对于子句的每个文字,祖先集包含一组祖先文字出现。集合对于初始子句是单例的,但是对于预解子句不需要这样,因为合并。(iv) 对于每个L [i],其中0 ≤i<|L|设C和D为前件,R为预解式。然后,(a) 将发生计数#R初始化为0。(b) 计算Anc(R)={(p,pC<$pD)|(p,pC)∈Anc(C)<$(p,pD)∈Anc(D)}其中p不是枢轴。(c) 对于主元p,计算链环集pC×pD,其中(p,pC)∈Anc(C)和(p,pD)∈Anc(D),并将它们加到G上。(d) 递增#C和#D,并使用新值#C和#D更新Anc(C)和Anc(D)。在实践中,为了效率,还记录了一些其他簿记信息。例子考虑同义反复y))这对我们来说已经是CNF公式的否定了有两个原子和三个子句。设子句为C0={x},C1={<$x,y}和C2={<$x,<$y}。H. Amjad/电子笔记在理论计算机科学185(2007)37y:C1y-y:C2X x-x:C2-x:C1x:C0图二. §3.2示例的链接图图1显示了一个可能的解析图(在这个简单的例子中,只是一个树),用于派生空子句,需要两个解析。链接图(图2)中的链接是((C1,0),(C2,0))y,((C0,0),(C1,0))x和((C0,0),(C2,0))x,其中附加的枢轴移动到外部下标中以避免符号混乱。Q所有子句都使用一次,因此子句出现次数都为零。这个例子说明了这种方法的主要缺点:它可能会产生更多的链接比决议的数量。在最坏的情况下,生成的链接数量可以是子句数量的二次方。请注意,链接中只显示初始子句。通过根据序列号对链接进行排序,并按照排序顺序应用分解,我们最终得到了原始证明。然而,通过重新排序应用程序可以获得很多好处,我们将在下一节中看到。 当对应于链接的解析操作被应用时,我们说该链接已被使用。在实践中,由于预解式通常被多次使用,我们只计算第一次出现的预解式的完整祖先信息。就链接图而言,这意味着学习过的子句出现在链接中,在某种意义上证明了它们自己的派生。因此,我们失去了能够完全重新排序导致使用预解式的所有解决方案的能力,但是跟踪所有预解式出现的祖先信息的代价(即,将链接限制为只有初始子句)是拥有一个非常大的链接图。尽管有这种复杂性,但我们将证明视为一棵树是至关重要的,因为这就是它作为数学对象的意义;因此,在链接图中DAG表示对于实现目的是有用要了解原因,我们需要引入阻塞链接的概念。回想一下,链接是一对文字出现。由于合并的文字,单个文字出现可能是多重链接的,即,发生在不止一个环节。一个链接,其一个或两个文字出现是多重链接,被称为阻塞。在上面的例子中,第二个和第三个链接被阻塞,因为这两个链接都链接到子句出现(C0,0)中的文字出现x。如果是这样的话,当我们要使用这样的链接时,我们有两个选择:• 或者,我们禁止使用被阻止的链接,希望通过删除剩余的链接,最终这些链接将解除阻止,8H. Amjad/电子笔记在理论计算机科学185(2007)3• 或者,我们也为预解式复制在实践中,禁止使用被阻止的链接并不有效,因为首先考虑所有未被阻止的链接,无论它们是否需要用于证明。有了复制,即使我们复制了更多的链接,至少我们不会被迫使用它们。我们现在可以看到为什么DAG不行。假设我们通过将子句的所有出现折叠为单个出现来将树转换为DAG。那么相应的链接图不能区分子句占用,这可能会在图中创建循环。如果我们使用禁止规则来使用链接,那么一个被阻止的链接的循环永远不会被使用,失去了完整性。如果我们使用复制规则,我们可以永远在循环中创建链接的新副本,再次失去完整性。3.3使用链路一旦我们有了链接图,我们就可以对链接进行排名,并将它们用于排名或排序。我们保证找到空子句。希望是找到它在更少的决议比原来的证明。我们的算法基于以下规则:(i) 如果可能的话,避免使用涉及已学过的从句的链接(ii) 如果可能的话,避免使用被阻止的链接。(iii) 更喜欢新的链接而不是旧的链接(即,更喜欢更高的序列号)。(iv) 最大限度地使用合并的文字。(v) 在每一个机会执行包容检查。(vi) 轨道2-条款和单位。启发式规则(i)-(iv)被直接结合到用于链路的排序函数规则(v)在处理与正在使用的链接相对应的分辨率时应用,并且(vi)在每次链接使用之后应用。应该注意的是,在证明搜索中使用的通常的算法在证明压缩中不一定事实上,它们往往使情况恶化。例如,几乎每个证明搜索程序(基础或一阶)的一个共同规则不幸的是,SAT求解器大量使用单位子句的解决方案。如果我们发现的单位子句是一个学习子句,那么我们必须优化使用它的证明中的许多子树,从而导致更长的证明。在某种程度上,规则(iv)试图检查子句的大小,而不是积极寻找更小的子句。事实上,规则(i)的存在正是为了阻止使用SAT求解器学习的子句(链接图已经捕获了这些信息),因为它们的推导不太可能是最短的,而且,正如前一节所指出的,我们自己找到更短的推导的可能性更小当然,有时我们别无选择,在这种情况下,我们回到SAT求解器推导,并希望规则(v)会有所帮助。H. Amjad/电子笔记在理论计算机科学185(2007)39C1:{-x,y}C0:{x}C2:{-x,-y}C3:{y}C4:{-y}假图三. §3.3示例的分辨率图规则(ii)的原因是我们使用复制规则来使用被阻止的链接,而不是禁止它们。复制规则将新的链接引入到链接图中,这些链接必须按顺序排列并可能使用。这是最好避免的。示例图3示出了图1的证明的一个可选的、不精确的版本,其需要三个分辨率。读者可以确认,这生成的链接图与前面的示例完全相同(除了C0的子句出现次数)。然后,链接排序规则(i)-(iv)将强制首先对以y为中心的链接进行解析,之后规则(vi)中的单位子句跟踪将允许立即终止第二次解析。Q最后,我们更详细地考虑最后两个规则。3.3.1包容检查子句可被其自身的任何子集所包含。包含子句更强大,并且更接近空子句。因此,包容检查可以在两个方面对我们有用:(i) 当使用链接时,可能的预解式可以被先前使用的链接的预解式所包含。如果是这样的话,这个链接可以被丢弃而不被使用,为我们节省了一个解决方案。(ii) 联系的前提可能已经包含在现有条款中。在这种情况下,我们可以使用包含子句作为先行词,以导出更强的预解式。在这两种情况下,我们可以同时从链接图中删除其他链接。这些链接的字面占位符将不再出现在解决式中包容检查经常成功,因为由于DPLL搜索的性质,许多分支可能包含相同的解析操作序列。为了检查包容,我们维护了一个已经派生的子句的缓存。这个缓存是用initial子句初始化的。它用于扫描包含所考虑的链接的先行项或解决项的子句。添加包含检查的一个副作用是,我们经常最终这个效应必须是10H. Amjad/电子笔记在理论计算机科学185(2007)3在执行验证阶段时,请牢记这一点。缓存是作为一个trie实现的,将子句视为某种全排序下的字符串。包含子句C的子句的查找实现如下:(i) 如果找到一个包含单元子句,则立即(ii) 如果发现包含非单位子句D,(a) 计算DJ=C−D(b) 删除D的第一个(文字排序的wrt)文字以获得DJJ(c) 递归查找DJ和DJJ,选择返回值中的较小值(如果有)该算法能够在平均情况下在目标子句大小的时间线上查找最小的包含子句,在最坏情况下在二次时间内查找最小的包含子句。 不幸的是,最坏的情况是包含子句在缓存中不存在,所以它发生的频率比我们希望的要高。一般的问题被称为前向包容,SAT和一阶社区都提出了几个复杂的方案来提高包容检查性能。我们打算研究一种零抑制BDD(ZBDD)[1],作为未来工作的一部分。3.3.2跟踪2-子句和单位如果我们有包含极性相反的相同原子的单位子句,我们可以立即推导出不满足性。因此,我们跟踪到目前为止获得的单元子句,并且,每当链接使用导致单元子句时,检查我们是否完成。类似地,两个2-子句可以被解析,使得剩余的文字是一个合并的文字,允许我们导出一个单元。跟踪2-子句也是相当简单的,可以有效地检查导出单位的可能性。跟踪3-子句不太可能给我们带来任何好处,因为众所周知,从一组3-子句中得到3.3.3迭代我们在前面提到,链接查找和链接使用阶段可以迭代。 这是因为链接使用阶段会产生新的解析证明,该证明可以反馈到链接查找阶段。两个迭代结果是非常有用的。我们认为原因可能是第一个缩短的证明可能包含学习子句的SAT求解器推导(尽管规则(i),第一次迭代无法避免第二次迭代可能能够优化这些推导。目前,增加两个以上的迭代似乎最多只能提供边际价值。我们还没有想到更有用的方法来决定是否进一步扩大。时间复杂度O(n)H. Amjad/电子笔记在理论计算机科学185(2007)3113.4验证一旦我们有了一个更短的证明,证明压缩算法就完成了。然而,部分是因为这是我们的动机,部分是为了检查我们的原型实现的合理性,我们有一个最后的阶段,在这个阶段,证明是在一个可编程的定理证明器中进行演绎验证的。我们选择了HOL定理证明器[8]来完成这项任务。HOL是高阶逻辑的交互式定理证明器,具有大量的定理库和自动证明过程。术语结构是多态的简单类型λ-演算,公式语法是具有等式的高阶谓词演算。证明系统是经典的自然演绎,并为简单类型论添加了额外的规则选择HOL的主要原因是我们对该工具的熟悉。然而,HOL有两个特性使其特别适合手头的任务首先,HOL是可编程的。推理规则在标准ML中编程,可以组合成更强大的规则。这允许用户编写自己的证明程序(即反驳验证器)。其次,HOL是完全可扩展的。这意味着推理规则必须建立在八个原始规则和五个公理的小核心之上,定理只能通过推理规则推导出来。因此,只要内核是健全的,整个系统就是健全的。特别是,这允许用户编程自己的证明规则,高度保证可靠性不会受到损害。这为我们提供了一种检查原型实现的方法。在HOL中,推理规则将定理作为输入和输出定理。这不符合我们陈述解析规则的方式,其中输入和输出是子句。最简洁的解决方案是将每个子句表示为定理。这里我们不涉及细节,只是简单地说明子句{p0,...,pn}可以由定理表示p0,. ,<$pn,p0. ∨ pn► ff其中旋转栅门符号将定理的前提与结论分开。这种表示允许我们用一个cut来表示一个归结操作假设我们有两个子句,表示为v,<$p0,. ,<$pn,<$v p0. ∨ pn► ff和<$v,<$q0,. ,<$qm,v q0. q m枢轴V 然后我们解决如下:(i) 获得<$p0,.,<$pn,<$vp0. n后接否定式介绍(ii) 去掉第二个从句,p0,. ,<$pn,<$v p0. p n,<$q0,. ,<$qm,v q0. q m根据需要12H. Amjad/电子笔记在理论计算机科学185(2007)3注意,预解式隐含在定理的假设中。最后,我们能够推导出一个定理,在这个定理中,除了那些对应于子句项的假设之外,所有的假设都被去掉了,这表明子句隐含着错误。在实现这个演绎规则时,唯一需要注意的是,要使它足够健壮,以处理由于第3.3节规则(v)的原因,主元在一个或两个前件中都没有出现的情况。3.5可靠性和完备性证明可靠性很容易,因为得到的证明也是一个归结证明,并且已知归结规则是可靠的。包容检查并不排除这一点,因为即使一个或两个先行词中缺少主元,所需的操作仍然可以很容易地转换为对较弱子句的归结操作定理3.1压缩算法是合理的由于SAT求解器是完整的,为了检查完整性,它需要检查算法从相同的初始子句中返回不满足性的证明(尽管它不一定返回更短的证明)。这是很容易建立的。定理3.2压缩算法是完备的由于我们从一个有效的反驳证明开始,并将每个归结操作转换为至少一个链接,因此处理所有链接可以保证在某个点导出空子句。唯一的危险来自重新排序链接。从子句中删除文字的链接可能会在引入相同文字的链接之前处理,而在原始证明中,它们的顺序是相反的。然而,在这种情况下,只有当引入的文字是一个合并的文字时,才会发生危险,因为这样我们就有可能错过删除该文字的多个可能祖先中的任何一个。但是链接图构造为所有祖先文字的出现创建单独的链接,所以这永远不会发生。Q这个证明更精确地重申了为什么我们在构造链接图时使用DAG作为证明的底层表示时会有失去完整性的风险。我们在这里注意到,类似的论点不足以建立使用类似方法的证明搜索的完整性。这需要一个更复杂的论证[3]。4实验结果为了测试该算法,我们尝试了50个问题,从一个标准套件的propo-sitational重言式分布与HOL。每个问题都被传递到MiniSAT SAT求解器的证明生成版本,并且所得到的证明通过压缩算法的两次迭代来传递。H. Amjad/电子笔记在理论计算机科学185(2007)313问题原始压缩比puz030 1105880.16Rip02是2332180.06u53522950.16jnh2113762550.32hostint1是9047840.13ztwaalf1 be9658400.13dubois2010165960.41ssa043200311628580.26米什格贝13909370.33ztwaalf2 be142510040.29Z4 Be178215250.14x1dn是201614110.3VG2 BE219615470.3mjcg是227617690.22添加1 be295225810.13Mul03 Be323529740.08Rip06是363123440.35dk17 be381434330.1里斯克贝466742980.08sqn be573346450.18粤ICP备16017888号-168987309360.55表1原始样张和压缩样张问题集的代表性子集的结果总结在表1中,显示了原始证明和压缩证明中的解决操作的数量,按原始证明大小的升序排序。请注意,这里报告的原始大小不包括冗余分支,这些分支很容易过滤掉。结果令人鼓舞。我们能够在一个非常有效的证明搜索引擎中找到证明中的冗余。然而,应该记住,不能保证我们总是得到一个更短的证明。14H. Amjad/电子笔记在理论计算机科学185(2007)3压缩比与证明的大小无关。看看它是否与问题难度的其他度量(如相变阈值)相关,这将是有趣的。然而,这一评估有两大遗漏。首先,我们还没有在大型SAT问题上尝试过该算法(表中最大的问题只有733个子句)。第二,我们没有提出一个时间分析:这很可能是压缩开销太昂贵的情况。两个遗漏的原因是相同的我们目前只有一个原型这在很大程度上是一项正在进行的工作。此外,至少验证阶段会自动为我们可以表示的问题的大小设置上限,因为HOL的完全扩展性质必然会带来性能损失。4.1复杂性我们还没有对算法进行全面的复杂性分析,因为在有效的实现之前,我们还有很长的路要走。尽管如此,我们可以大胆地说几句。解决方案不是自动化的,即,一般来说,在给定归结证明的情况下,不可能有效地找到更短的归结证明。这就限制了我们对上述算法的期望。然而,归结是否是弱自动化的,即给定归结证明,同一公式的较短证明可以在较强的证明系统中被有效地找到这是一个可能的调查领域。这与更一般的归结的证明复杂性有关。最终,我们希望创建一个通用的平台,用于实证研究我们对基于归结的证明系统的证明复杂性的直觉。5结论证明压缩只有在证明被发现后,在更高的保证但更慢的系统中被重放或验证时才有意义。因此,证明压缩的一个领域是证明携带代码[11]。但这与我们的工作关系不大越来越多的高保证证明平台,如HOL,通过将证明搜索外包给专业引擎,然后在本地逻辑中重建证明,来利用证明验证的便利性与证明搜索的困难性[7,12]。然而,据我们所知,压缩作为一个单独的阶段并没有成为研究的重点,可能是因为,到目前为止,证明根本不够大,以保证压缩开销。在这里,我们对压缩研究进行了区分,即,缩短已经导出的证明,并研究更好的决策过程,找到比早期过程更短的证明[9]。H. Amjad/电子笔记在理论计算机科学185(2007)315我们的工作处于非常早期的阶段,许多改进正在进行中。目前的首要任务是调查各种不同的化学品的孤立影响,并改进执行情况,以便能够进行时间分析。最终,我们希望使用这个工具来调查自动化能力的问题,在一个更一般的设置。引用[1] 阿卢尔湾一、M. N. Mneimneh和K.A. Sakallah,基于ZBDD的回溯搜索SAT求解器,在:逻辑综合国际研讨会,密歇根大学,2002年。[2] 安德鲁斯,P.B.,Matings的反驳,IEEE Trans.Computers 25(1976),pp. 801-807[3] Bibel,W.,On matrices with connections,JACM 28(1981),pp. 633-645[4] Biere,A., A. Cimatti,E. M. Clarke和Y. Zhu,Symbolic model checking without BDD,in:R. Cleaveland,编辑,系统构造和分析的工具和算法,LNCS 1579(1999年)。[5] 戴维斯,M.,G. Logemann和D. Loveland,A machine program for theorem providing,Journal ofthe ACM 5(1962).[6] 恩,N。 和N. S?renss on,An extensib leSAT-s olve r,in:E. 我是一个很好的朋友。 Tacchella,editors,Theheryand Applications of Satisfiability Testing,第六届国际会议,计算机科学讲义2919(2003),pp. 502-518[7] Fontaine,P.,J. - Y. Marion,S.梅尔茨湖Nieto和A. F. Tiu,表达性+自动化+健全性:走向结合SMT求解器和交互式证明助手,在:H。赫尔曼斯和J. Palsberg,editors,TACAS,LNCS 3920(2006),pp. 167-181。[8] 戈登,M。J. C.和T. F. Melham,editors,[9] Jussila,T.,C. Sinz和A. Biere,扩展分辨率证明符号SAT解决与量化,在:第9国际。Conf. 在理论和应用的满意度测试,LNCS(2006),出现。[10] 科瓦尔斯基河一、A proof procedure using connection graphs,JACM(1975).[11] 萨卡尔,S.,B. Pientka和K. Crary,LF的小证明证人,在:M。Gabbrielli和G. Gupta,editors,ICLP,LNCS 3668(2005),pp. 387-401号。[12] Weber,T.,在LCF式定理证明器中使用SAT求解器作为命题逻辑的快速决策过程,技术报告PRG-RR-05-02,牛津大学计算实验室(2005),高阶逻辑中的定理证明-新兴趋势会议录。[13] 张 丽 和 S.Malik, Validating SAT solvers using an independent resolution-based checker : Practicalimplementations and other applications,in:Design,Automation and Test in Europe Conferenceand Exposition(Date)(2003),pp. 10880-10885
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 保险服务门店新年工作计划PPT.pptx
- 车辆安全工作计划PPT.pptx
- ipqc工作总结PPT.pptx
- 车间员工上半年工作总结PPT.pptx
- 保险公司员工的工作总结PPT.pptx
- 报价工作总结PPT.pptx
- 冲压车间实习工作总结PPT.pptx
- ktv周工作总结PPT.pptx
- 保育院总务工作计划PPT.pptx
- xx年度现代教育技术工作总结PPT.pptx
- 出纳的年终总结PPT.pptx
- 贝贝班班级工作计划PPT.pptx
- 变电值班员技术个人工作总结PPT.pptx
- 大学生读书活动策划书PPT.pptx
- 财务出纳月工作总结PPT.pptx
- 大学生“三支一扶”服务期满工作总结(2)PPT.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功