北京物流信息联盟

传统逻辑协调化、经典化和自动化的实现

2022-04-08 10:31:22

【作者单位:中国科学技术信息研究所 信息技术支持中心


摘 要:

传统逻辑主要指亚里士多德的三段论,它能否被一阶语言表达并被自动证明,长期以来是不清楚的。通过研究 证明传统逻辑经典化( 一阶语言表达和数理化) 的障碍在于它的不协调性,进而消除了传统逻辑的不协调性,建立了改进的三 段论推理的数学模型,同时改进了一阶逻辑,使之能够表达改进后的三段论。这些工作使得传统逻辑完全实现了协调化、经典化和自动化。


关键词: 三段论; 一阶逻辑; 自动推理; 格岗尼图; 部分量词; 一致性


1 问题的提出

    按照逻辑史学家的分类,一般将一阶逻辑之前的逻辑称为传统逻辑,这主要指亚里士多德三段论的逻辑。而一阶逻辑被视为是经典逻辑,在一阶逻辑建立的同时或之后,超出以名词词项、谓词、量词 为变元的逻辑( 如以时态、模态等为变元的逻辑) 称为非经典逻辑[1]。

    自一阶逻辑诞生后,传统逻辑始终面临一些问 题。首先是它与一阶逻辑的本质差异何在? 如果不 能说清楚亚里士多德三段论与一阶逻辑有本质差异,这种分类就失去了意义,但是长期以来没有充分的论证,确认二者之间何以有或没有本质差异。最 近,对传统逻辑和一阶逻辑异同的困惑的一个典型表达是2009年Intel公司的总工程师John Harrison在其专著《Handbook of Practical Logic and Automated Reasoning》中的表述[2]。作者对三段论自动推理的 研究进行了历史性的总结,他认为,有关三段论自动 推理的研究仍然有2个悬而未决的问题。

    问题1:三段论是否能够、如何以一阶语言进行表示? 或者它和一阶语言是什么关系?

    问题2: 已经实现的三段论自动推理是否是亚里士多德本意的三段论推理? 或者,我们在计算机上实现的三段论自动推理,就是亚里士多德及其后继者设想的三段论推理吗?

    问题1就是这种困惑的表达。虽然,当前的计算机实现了亚里士多德三段论的自动推理,但是,这种推理没有完全在基于一阶或高阶语言的逻辑编程语言(如 Prolog,LISP,HOL) 中实现。此外的困惑仍然存在,即问题 2——在我们实现了的亚里士多德三段论的自动推理之后,甚至不敢肯定这种实现就是亚里士多德本来意义上的三段论。这个问题体现了对传统逻辑仍然不甚清楚的研究状况。

    关于亚里士多德三段论与数理逻辑的关系也有类似的困惑。数理逻辑的教科书往往对亚里士多德三段论一笔带过甚至不讲,而哲学学科的形式逻辑对亚里士多德三段论则详加阐释,这至少造成一种印象,好像亚里士多德三段论属于哲学范畴,而非属于数理逻辑。但是,虽然亚里士多德是哲学家,而在亚里士多德时代哲学和科学在是一体化的,亚里士多德也是今天严格意义上的科学家,因此,我们不能把亚里士多德三段论仅仅列为哲学而非科学( 假如哲学和科学有本质差异的话) 。最近的一个关于数理逻辑的定义将数理逻辑定义为“逻辑中的演绎推理数学化——推理的有效性成为数理逻辑的内容之 一” [3],而三段论恰恰是典型的演绎推理,三段论理论也恰恰研究演绎推理的有效性( 它的规则和形式系统都是解决哪些三段论推理是有效的,哪些三段论推理是无效的) ,它的量词理论恰恰是使演绎推理( 严格说是构成三段论原子命题,即三段论中三 个命题中的一个) 数学化( 三段论原子命题的量词已经被集合所表示) ,这使得我们不能把三段论排斥在数理逻辑之外。还有重要的一点是,没有任何形式上的显式特征,将三段论归为所谓的哲学逻辑而非数理逻辑。那么,原子命题的量化能否构成三段论推理过程的量化,即演绎推理数学化? 如果能够,这个数学化的结果如何? 这个问题需要更为有力的证明。但是,这个证明在哪里?

    在逻辑史上,莱布尼兹首先认为包括三段论在内的逻辑演算应该完全数理化,使得哲学家与数学家讨论的逻辑完全一致,都能够成为可计算的。逻辑史研究者 Wolfgang Lenzen 这样描述莱布尼兹的思想: 在17 世纪晚期,逻辑既作为一个学科又作为一个正规的科学,基本上等同于亚里士多德三段论。 莱布尼兹的逻辑工作在相当大程度上也是关于三段论的理论,但是同时,他力图构建更有力的“广义的演算”。这一演算初步作为一个通用工具确定哪一个形式推理( 不只是三段论推理) 是逻辑有效的。更进一步,莱布尼兹寻找“通用的特征”,通过这一特征,希望能对任意命题( 科学命题) 应用逻辑运算使得命题事实上真能够用纯机械的方式被“计算出来”。这种过于乐观的思想表述在下面这段著名的 话中 : “如果可以做到这一点,矛盾一旦出现,两个哲学家不会比数学家更有必要进行争论,因为只要拿起笔坐在算盘( 西方的一种计算装置,不是中国的算盘) 旁就足够了——对对方说: 我们算一 下” [4] 。这里,我们面临一个问题,即莱布尼兹所设想的问题:如何将三段论推理可计算。如果量词将三段论的原子命题量化,那么三段论的推理是否也伴随着推理的量化,即三段论推理是否伴随着数学计算过程,亦即,是否存在三段论推理的数学模型? 如何构建这一模型? 我们在此称这个问题为问题3。

    2009 年,张寅生的专著《扩展的三段论及自动 推理》[5]( 以下简称“《扩展》” ) 一书对这3个问题给出了解答。它揭示出传统逻辑长期以来没能融入一阶逻辑的一个主要障碍是它具有不协调性( 不一致性) ;此外,一阶语言要表达传统逻辑还需要进行若干量词、演算规则的扩展。在消除了传统逻辑的 不协调性之后,经过一阶逻辑表达能力的扩展,传统逻辑与一阶逻辑的界限将会完全消除。不但一阶语言完全可以表达传统逻辑,而且可以用现代的计算机理论、方法与技术完全实现传统逻辑推理(对问题1的解答) 。至于这种自动推理是否是亚里士多德本意的三段论推理(问题2) ,研究表明,由于传统逻辑的不协调性,使得我们不可能恢复( 重建) 传统逻辑的“本来面目”,除非我们丧失协调性。对传统逻辑的不协调性的发现和证明是一个重要的结论,它终结了沿袭两千多年的传统逻辑不协调的状况,最终消除了传统逻辑融入经典逻辑体系的障碍,也 为计算机自动推理增添了新的理论和方法。传统逻辑在协调化之后,三段论推理过程将被完全数学化,即通过建立数学模型,表示( 扩展的) 三段论推理,即三段论推理过程的计算不再仅仅是符号计算,而是伴随着数学运算( 集合关系随机事件样本的合成运算) ,这使得一阶逻辑的一种量词演算建立在数学运算基础上,从而丰富了对一阶逻辑运算的理解 ( 对问题3的解答) 。

2 特称命题的不一致性

    一个亚里士多德三段论是形如式( 1) 的命题:

α∧β→γ 。 ( 1)

    其中, α, β, γ∈{ A, E, I, O} 。A,E,I,O分别代表4 种直言命题:全称肯定命题 ( “所有X是 Y”) ,全称否定命题 ( “所有X不是 Y”) ,特称肯定命题(ŦX是 Y” ) ,特称否定命题 ( “ŦX不是 Y” ) 。在三段论中,α,β,γ 每个命题中的项X和Y分别实例化为(M,P) ,(S,M) ,(S,P) 。Ŧ是约束前一个项X的特称量词。

    特称命题最初由亚里士多德定义,一直以来其逻辑协调性和准确性并未受到本质上的质疑、否定或纠正。但是《扩展》指出,特称量词有2种解释,相互矛盾。第1种解释是“有”,它包括所指称对象的全集;而第2种解释是“有些”,不包括全集。这就是《扩展》一书揭示的亚里士多德三段论不一致性之一。

    设X是由元素xi,i=1,2,…,n( n>0)组成的集合,设UN(X) 是集合X的全集,即UN(X) ={ xi|i=1,2,…,n},则表示UN(X)的量词是关于项X的全称量词,表示为"

    设PT(X) 是集合X的一个真子集,即PT(X) = { xi|i=1,2,…,m,m<n},亦即PT(X)ÌUN(X) ,称表示PT(X) 的量词是关于项X的部分量词,表示为〒。

    设ID(X)是集合X的一个子集,即ID(X) ={ xi|i=1,2,…,m,m≤n},亦即ID(X)ÍUN( X),称表示ID(X)的量词是关于项X的存在量词,表示为$。于是,特称命题的不一致可以表示为:

Ŧ=PT(X)=ID(X),(2)

    即特称量词既被表示为可包括全集,又被表示为不可包括全集,违背了逻辑同一律。这就是说,由特称命题构成的三段论是不协调的。三段论应该被纠正,使之在逻辑上协调化。

3 部分量词的增补

    由于式(2)是构成亚里士多德三段论原子命题的推论结果,因此,需要将特称量词Ŧ进行划分,即Ŧ应该划分出2个独立表示的量词概念: 部分量词〒和存在量词$

    “部分的”是自然语言知识表示中的一个非常重要的数量概念。无论从逻辑还是从数学的观点看,“部分”与“全部”具有同等重要的意义。它们是描述一个参数 ( “是全体吗” ?) 的2个变量,也可以说是以这个参数为真值的2个并列的逻辑值。在物理系统,“部分”也是不可缺少的物理状态。

    如果Ŧ划分为〒和$,三段论也将被划分,即有可能包含3个量词{〒,$"}构成的3个二元命题构成的三段论。这样我们就得到了问题2的答案。就是说,亚里士多德三段论本身就是矛盾的,不协调的,如果要保持逻辑真的推理,就必然舍弃特称命题,这就必然破坏亚里士多德三段论的“原貌”, 换言之,协调后的三段论必然不再是亚里士多德三段论本身了。质言之,如果要保持逻辑的协调性,亚里士多德三段论本身是不能被恢复的。

4 一阶逻辑的改进

    显然,如果一阶逻辑不能表示部分量词,将使一阶逻辑与传统逻辑产生鸿沟。但是,一阶语言在表示数量知识时,长期以来只表示“全部” (即全称量词) ,而不能表示“部分”。这暴露了一阶语言的历史局限性。事实上,一阶语言的表示能力并非令科学家们满意[6-7]。

    一阶逻辑以及表达它的语言(一阶语言) 自1891年被其创立者弗雷格定义以来已经有100多年的历史。在题为《函数和概念》的论文中,弗雷格对一阶函数定义如下: 正像函数和对象是根本不同的一样,其自变元是并且必然是函数这样的函数和自变元是并且只能是对象这样的函数也是不同的。 我称后者为一阶函数,称前者为二阶函数[8]。

    据此,可以对一阶命题进行如下定义:一阶命题的本质在于命题的变元( 项) 只能是对象(可数的个体) ,而不能以函数( 或谓词结构或命题) 作为变元( 项) 。关于一阶命题的逻辑应该被理解为一阶逻辑,表述一阶逻辑的语言应该被理解为一阶语言。由于弗雷格本人用一阶语言对算术知识的表示,显示了一阶逻辑及其语言自逻辑诞生以来强大的表示能力。而自20 世纪上半叶和中叶逻辑编程语言LISP和Prolog诞生以来,由于两者均以一阶语言作为其表示语言,因此,一阶逻辑语言不仅成为数学知识的通用表示语言,而且与逻辑编程语言在表达方式上 拥有广泛的一致性和同构性,这使得一阶语言成为计算机科学广为应用的形式化语言,一阶逻辑也成为计算机科学技术的一个重要的基础逻辑。值得注 意的是,弗雷格并没有对一阶语言的语法进行完整的和形式化的定义。因此,一阶逻辑和一阶语言更像是一个开放的标准,对于符合上述定义的逻辑和语言均可以视为它的家族。从这个意义上说,一阶逻辑和一阶语言不是定型的和封闭的,是逐渐地、不停地在丰富和发展着的逻辑和语言。

    事实上,广义量词理论对一阶逻辑的量词进行了大量扩展,将部分量词列入了一阶逻辑。这些工作主要是Mostovski[9],Montague[10-11]、Barwise等[12]、Hintikka[13]和Keenan[14]所做,但是在如何建 立广义量词的一阶逻辑演算问题上缺少明确而系统的解决方案。

    最近,关于亚里士多德三段论原子命题中广义量词的研究,如用模糊积分模型对量词以及一阶语言命题演算的模型化[15]。类似地,在一阶逻辑中增补部分量词的难点在于,包含部分量词的所有一阶演算的规则如何确定,以及确定的规则是否符合语言学意义(包含部分量词表达式的演算意义与运算结果与自然语言的语义是否相符) 。换言之,对于包含部分量词的二元直言命题如何进行一阶逻辑的任意逻辑运算,上述的工作没有给予解答。

    《扩展》将部分量词表示如下:

    其中: ≡表示逻辑等值, |表示“排斥或( Nand) ”,即被运算的前后两项必须一真一假。式( 3) 的直观语义是 : “‘部分’是存在的并且不是全部的;或者,‘部 分’不是‘或者全部或者不存在’”。至此,部分量词的原子命题完全可以用一阶语言表示。现在面临的问题是,是否包含部分量词的三段论原子命题能够进行逻辑运算( ®运算) 。由于式(3) 是一个逻辑公式,使得包含公式左右侧的表达式可以分别等值带入一个关于®运算,这样,关 于包含部分量词的命题的®运算公式就 可以建立。《扩展》基于此建立了包含部分量词的命题的®运算公式,这使得一阶逻辑实现了包含部分量词的命题的逻辑演算。接下来面临一个问题:如何用一阶语言表示包含部分量词的三段论命题。

5 扩展三段论命题的一阶语言表示

    对亚里士多德三段论的一阶逻辑表达最早由一阶逻辑的创始人之一罗素完成。对于式(1) ,当量词取"、谓词取肯定系辞时,罗素将其表示为一阶公式如下[16]: 

"x(f(x)®y(x))"x(y(x)®c(x))®"x(f(x)®c(x))     ( 4)

    其中fyc 表示不同的谓词。f表示“is sy表示“is mc表示“is p

    考虑到三段论的原子命题都是二元命题,所以,我们可以按照一阶语言的语法在量词取"时,式 ( 1) 可以转变为


    其中t 表示谓词(肯定系辞 ) “是”。比较式(4) 和式 (5) ,即三段论的一阶语言两种表示方法,可发现三点差异。第一,式( 4) 仅仅将每个原子命题的一个项 x 进行独立表示,项 y 不能独立表示,而是和谓词“是”在一起不独立地表示为fis s),yis m),cis p);就是说,符号fyc既表示项,也表示谓词;而在式(5)中项和谓词是独立表示的(谓词t与项smp以不同符号分开表示)。第二,对于一个原子命题,式(4)仅仅以一个变量x表示二元命题的两个项,例如,在原子命题(f(x)®y(x)中只有一个项变元x而在式(5)中每个原子命题都有两个项变元,即smmpsp)。第三,在式(4)中,每个原子命题中只有一个约束量词;而在式(5)中每个原子命题有两个约束量词

    这样,式(4) 面临一些难以解决的问题。第一,谓词和项用一个符号表示,相当于在数学中用一个符号同时表示函数符号又表示函数处理的变量(试想一下“ f(x) ”的表示方法被禁止,在需要分别表示 f 和 x 时只能用一个符号进行表示,这对于数学有多么可怕!) ,这将不能进行复杂的函数和项的表示和运算。由于一阶语言的本质特征是将项和谓词分开表示[17],因此,式( 4) 违背了一阶语言的本质特征。第二,对于二元项的命题,式(4) 用 x 表示不同的项,即未能用不同的变量表示不同的项,这将造成项的表示的困难。比如,在习惯上用不同的变量表示不同的项的一阶语言环境中,这种表示方法将造成融合的困难。第三,式(4) 没有对所有的项进行量 词约束,在一阶语言语法中,未约束的变量被理解为 自由变量,但是(4) 式中,与谓词一起表示的项变元是允许有约束量词的。例如,“所有的男人是部分人”,“部分”是对第二个项的约束,但是式(4) 未能对后一个项进行量词约束,因此,不对可约束的量词 进行约束将造成歧义。

    为克服式(4) 的上述3个表示和运算上的困难,我们需要对三段论进行形式改进。对于式(5) , 我们进行改进如下:

Q1s Q2mt(s,m)∧Q3mQ4pt(m,p)®Q5sQ6pt(s,p)|Q6pQ5st(p,s)6

    式(6) 是将式(5) 中的量词"改为量词变量的结果。这里Q1,Q2,Q3,Q4,Q5,Q6 ∈{ ,",$} 。 →后面的结论由排斥或运算符“|”而选择其或前或后中的一个命题。这样,我们实现了所有的项都单独以符号表示;所有的项与谓词分开表示;所有的项都以量词进行约束; 量词中包括部分量词。我们把 式(6) 称为( 由正命题构成的) 扩展的三段论,它克服了三段论的一阶语言表示式(4) 中的局限性,也增加了部分量词,实现了一阶逻辑的改进。换言之,它即实现了亚里士多德三段论的协调化,也实现了一阶逻辑表示能力的改进。由于三段论完全实现了一阶语言的表示,而一阶逻辑被称为经典逻辑,因此,式(6) 及其允许的原子命题的否定形式实现了亚里士多德三段论的经典化,即解决了问题1。

6 扩展三段论命题的可判定性

    对于式(6) ( 假设3个原子命题的谓词t”和“t即“是”或“不是”均被允许) ,我们希望能用自动推理的方法实现有效命题(真命题) 的推导。 我们首先考虑式(6) 更为细化的形式,允许由正负命题构成的式(6) 可以实例化为4类样本。前提第1格至前提第4格,即式(6) 中的2个前提中总共的4个项会有4个排列: ( m, p, s, m,) ,( p, m, s, m) , ( m, p, m, s) ,( p, m, s, m) ( 我们用小写的字母表示被 量词约束的项) ,这 4 种不同排列实际上导致不同的原子命题,即产生不同的三段论。

我们用F表示这4个排列。类似地,结论的两 个项也有( s,p) ,( p, s) 2 个排列,我们称之为结论 格,用F’表示这2 个排列。谓词用⊙( 加下标) 表示 ( 它相当于式( 6) 中的 τ 的肯定或否定,为直观起见,位置放置在项的中间) ,实例化为正负( 表示 “是”和“不是” ) 。表1 列出了式( 6) 的各种可能形 式,其中,每个前提格中的2个前提及其对应的一个 结论( 结论第 1 格或结论第 2 格) 构成一个扩展三段论。

    这样,考虑量词的取值、谓词的取值、前提格和结论格的不同,扩展的三段论所有可能的方案( 三段论的变量导致的不同样本) 是:

Q××Q×Q××Q×Q××Q×F×F′

其中:QÎ{〒,"$},⊙Î{+,—}

FÎ{(mpsm)(pmsm)(mpms)(pmms)}F’Î{(ps)(sp)}。其方案总数是:3×2×3×3×2×3×3×2×3×4×2=46656

在46656个扩展的三段论中,如何自动地证明其中的某1个样本的真假, 是扩展的三段论的判定问题。这个判定需要解 (7)、(8) 和(9) 3 个函数,即量词、谓词、格从前提到结论的映射:

Q4®Q2               (7)

2®             (8)

F®F′                    (9)

《扩展》一书证明,函数( 7) 、 ( 8) 、 ( 9) 是可解 的,并给出了这 3 个函数的求解答案。结果表明, 46656个扩展的三段论是可判定的,其中 504 个是有效命题,其余均为假命题。

7 扩展的三段论推理的数学模型

    求解函数(7)、(8)、(9)的模型以及决定量词的 模型就是改进的三段论( 扩展的三段论) 推理所依 据的数学模型,它使得问题 3 得以解答。基本方法 是应用格岗尼图的合成方法。格岗尼用两个欧拉圈的拓扑关系表示二元直言命题中两个项X和Y的关系,即全异关系、全同关系、交叉关系、包含关系和被包含关系,见表2[18],即: G={║,,¤, É, Ì}。其中每个元素( 表示一个关系) 称之为一个格岗尼图。

    显然,格岗尼空间包括且仅包括这5个关系。至于用哪个关系或者关系组合表示某个二元直言命 题,欧拉给出的解答是: Ì表示A表示E;¤既表示I也表示O欧拉的局限性在于:某些直言命题可能多于欧拉所说的单一关系,如●也可以表示A的一个方案。由此产生一个问题 : “欧拉作为一个 大数学家为什么会犯此错误”[19] 。《扩展》给出的 解答是由于三段论中的直言命题的不一致性使然, 即欧拉只考虑了特称命题不一致性中的一个方面, 即认为Ŧ=PT(X) ,且后项 Y 没有像 X一样考虑多个方案。但是,如果扩展的直言命题(表1中的任何一个原子命题) 都用格岗尼空间中的元素组合来表示,一个扩展的三段论就构成了3 组格岗尼图的 再组合,其组合方案是庞大的。如何根据这些格岗尼图的组合与再组合方案求解式(7)、(8)、(9),当前的法国学者Stenning和Lambagen认为无法求解[19]。但是,《扩展》一书发现了求解的方法,实现了(7)、(8)、(9) 的求解。这使得问题3得以解答, 进一步地使得扩展的三段论推理成为可计算的。因此扩展的三段论也是用机器可进行数值计算的,即实现了改进的三段论推理的自动化。

8 结 论

    《扩展》的研究表明,传统逻辑需要并且能够协调化,其主要方法是将特称量词进行部分量词和存在量词的划分,并使直言命题的后项允许量词约束。传统逻辑经过协调化,一阶逻辑经过改进,能够使传统逻辑实现一阶语言表示,即实现了经典化。通过数学模型的建立, 想,被机器演算。而实际上,改进的三段论( 扩展的 三段论) 推理的核心是基于数值计算,它可以在数值计算的机械(如电子计算机)上实现,这相当于扩展的三段论作为改进了的传统逻辑在原理上完全实 现了自动化。
参考文献:
[1] 苏珊·哈克. 逻辑哲学[M] . 北京:商务印书馆,2003:12 -13. 

[2] HARRISON J. Handbook of practical logic and automated reason

ing[M]. Cambridge: Cambridge University Press,2009:320.

[3] 顾红方,白鹏,肖奚安,等. 数理逻辑之研究对象、学科归属、定 义及研究领域[ J] . 自然杂志,2000, 22( 5) :294 -299.

[4] GABBAY D M. Handbook of the history of logic[M]. Amsterdam

Boston Heidelberg London New York Oxford Paris San Diego San Francisco Singapre Sydney Tokyo. Elsveier Press,2004.

[5] 张寅生. 扩展的三段论及自动推理[M] . 北京: 科学技术文献 出版社,2009:88 -117.

[6] 史忠植. 高级人工智能[M] . 北京:科学出版社,1998:18.

[7] BARWISE J,COOPER R. Generalized quantifiers and natural language[ J]. Linguistics and Philosophy,1981, 4:159 -219.

[8] 弗雷格. 弗雷格哲学论著选辑[M] . 北京: 商务印书馆,2001: 72.

[9] MOSTOWSKI A. On a generalization of quantifiers[ J]. Fundement a Mathematicae,1957, 44:17 -36.

[10] MONTAGUE R. The proper treatment of quantification in ordinary english[M]. Oxford: Blackwell Publishing,1974:17 -34.

[11] PARTEE B H. The structure of meaning Lecture 13: noun phrases and quantification[EB/OL] . ( 2012 -08 -22) [2014 -12 -22] http: / /www. docin. com/p -466958032. html.

[12] BARWISE J,ROBIN C. Generalized quantifiers and natural language[ J]. Linguistics and Philosophy,1981, 4:159 -219.

[13] HINTIKKA J,SANDU G. What is a quantifier? [J]. Synthese, 1994, 98:113 -129.

[14] KEENAN E. Some properties of natural language quantifiers,generalized quantifier theory[J]. Linguistics and Philosophy,2002, 25:627 -654.

[15] YIN M S. Linguistic quantifiers modeled by sugeno integrals[ J] . Artificial Intelligence,2006,170:581 -606.

[16] RUSSEL B. Principia mathematica[M]. Cambridge: Cambridge University Press,1957:138.

[17] 肯尼·安东尼. 牛津西方哲学史[M] . 北京: 中国人民大学出 版社,2008:316.

[18] 涅尔·威廉,涅尔·玛莎. 逻辑学的发展[M] . 北京: 商务印 书馆,1985:450.

[19] STENNING K,LAMBALGEN M V. Human reasoning and cognitive science[M]. Cambridge: The MIT Press,2008:303.

友情链接

Copyright © 2023 All Rights Reserved 版权所有 北京物流信息联盟