没有合适的资源?快使用搜索试试~ 我知道了~
论有约束关系代数的公理系统及其应用
204网址:http://www.elsevier.nl/locate/entcs/volume67.html14页关于有约束R.P. de Freitas1COPPE-UFRJ,里约热内卢-RJ巴西J.P. Viana2COPPE-UFRJ,Rio de Janeiro-RJ IM-UFF,Niteroi-RJBrasil摘要本文给出了一个有约束关系代数的公理系统。这是一个混合形式主义介绍x的等价问题塔斯基的关系演算。RAB并不满足塔斯基提出的要求,但正如它所表明的那样,当涉及二元关系语句的符号化时,它是一阶逻辑的一个非常有趣的替代方案RAB公理化的提出有助于它作为一种形式主义发展到关系事实的关系演算在计算机科学和自然语言研究中得到了广泛的应用,其经典理论也得到了广泛的扩展。由于RAB似乎为关系代数和混合逻辑的应用提供了新的视角,本文的工作可以被认为是对这一发展的贡献。关键词:关系代数,混合逻辑,带联结器的关系代数,完备性1关系演算和隐式排序本节回顾塔斯基的关系演算(TRC)。重要的equipollence问题,它的讨论,以及如何排序已隐含地使用与TRC。对真相与和解委员会的全面审查见[7]。1电子邮件地址:naborges@cos.ufrj.br2电子邮件地址:petrucio@cos.ufrj.br2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。205u关系演算是讨论和推理关系的适当的形式系统。关于齐次二元关系的两类有趣的关系演算由A.Tarski in [21].设一个集合fRi:i2Ig为固定的,其中的所有ym都倾向于表示二元关系.我们称之为二元关系的初等理论(Elementary Theory of Binary Relations,ETBR)的第一阶演算,是通过将具有相同类型的一阶语言定义为一组二元谓词系统而得到的扩展。 细节可以在[22]中找到。注意,在ETBR中,在某种意义上,有两种变量:个体变量和关系变量。第二种,我们称之为塔斯基关系演算(Tarski's Relational Calculus,TRC),是关系代数的方程理论的一个版本,它以fRi:i2Ig作为变量集,布尔函数[和] (并和补)和皮尔斯函数j和1(合成和转换)作为运算,Id(恒等式)作为区别元素。对于关系代数的理论,我们建议[10,15],对于TRC,参见[22]。注意,在TRC中只有一种变量。真理与和解委员会的一个重要特点是,它可以改写ETBR的句子,而不提及个人。例如,我们可以说一个关系R u u是一个双射函数,它满足方程3R1jR Id(R是泛函),RjE=E(R是总的),RjR1Idu (R是单射的),并且R 1jE=E(R是满射的)。 不幸的是不是ETBR 的 所 有 第 一 阶 句 子 都 可 以 表 示 为 TRC 的 等 式 。 1915 年 , L.LOwenheim[11]报道了Korselt的一个命题“R整环至少有四个元素”不等价于TRC的任何方程.因此,TRC在表达方式上弱于ETBR。塔斯基开始调查,如果这种不平等是他选择了错误的关系代数形式主义,即,如果有可能改变所选择的操作,以便在表达方式上与ETBR等同 他对丰富表达能力所允许的操作符的语义解释提出了非常普遍的要求。 他希望所选择的运算符在以下意义上是“逻辑的”:对集合S上的关系的运算是逻辑的,如果它在S的所有排列下都是不变的;关系演算RC的运算符号是逻辑的,如果它表示RC的所有模型中的逻辑运算。在1940年左右,塔斯基证明了下面的强否定结果[22]。定理1.1给定TRC上接有有限个对数算子的任何形式,ETBR的句子都不等价于TRC的任何方程。因此,TRC操作的选择并没有被误导:没有类似于TRC的nitary形式主义,它捕获了ETBR的全部表达能力。除了在表达方式上弱于ETBR之外,塔斯基系统的另一个缺点是它是不完整的,即,有真实的方程3注意,包含RS等价于等式R S =;。2061212111122112211222关于在TRC中无法证明的关系(涉及布尔运算和皮尔斯运算)。1950年,R.林登[12]表明,包括:RR\SS\TTR(R1S\RS1\(R1T\RT1)(T1S\TR1))R4;虽然对所有二元关系R1、R2、S1、S2、T1和T2都成立,但不能在TRC中给出。作为S. Givant在[7]中指出,有一个简单的方法可以提高TRC的可演绎能力,以获得一个关于关系的真方程完备的系统。但所涉及的公理化并不是由一套完整的公理模式给出的。事实上,R. Maddux在[14]中证明了以下强结果:定理1.2不可能从有限个模式的实例中得到完全于关于关系的真方程的TRC语句集。因此,在表达和证明方法上,就出现了扩展TRC的两个重要问题:表现力问题。寻找一个自然的、内在有趣的逻辑运算符序列来扩充TRC,从而达到与ETBR在表达方式上的等价。演绎问题。通过大量的逻辑运算符和逻辑公理模式来扩充TRC的词汇表,使得所得到的形式主义在证明方法上与ETBR等价。这些都是非常棘手的问题。部分结果已在[22]和[7]中报道。包含部分解的最新参考文献是[19]。在表达性和演绎性问题的陈述中,限制的充分性对于一个可能的解被认为是解是非常重要的[2]。但是,如果我们考虑无限多的非逻辑运算符,这两个问题都有一些有趣的解决方案事实上,如果我们把每个变量都看作是一个零元运算符,它的意义可以从一种解释变成另一种解释,那么通过在TRC中引入隐式排序,ETBR可以看作是这两个问题的退化审查更多的限制性解决方案,使用排序形式主义隐式,在这里提出。在[24]中,W. W. Wadge提出了一个自然演绎系统来推导xRy形式的公式,其中x和y是个体变量,R是关系项。Wadge证明了他的系统对于TRC的Wadge的关系演算的主要特点是使用个体变量和没有任何种类的连接或定量。在[8]中,M.C.B.亨尼西提出了一个分析tableaux反驳的for-h形式的半乳糖醛酸; i 2T,其中并表示一种关系4RS是 Rj S2207术语T。 Henessy证明了他的系统对于关系演算的所有真方程对于所有关系的齐次关系都是完备的。作为推论,他证明了他的微积分的紧凑性。Henessy的关系演算的主要特点是隐式使用变量序列和投影算子的存在。在[20]中,SchOnfeld给出了ETBR的一个版本的一个序列演算。 他证明了完整性和证明长度的上限。在[13]中,R.Maddux提出了一种用于推导包含xRy形式公式的序列的微积分,其中x和y是单独的变量,R是关系项。Maddux证明了他的系统对TRC的所有真方程是完备的,并研究了语义问题。Maddux的关系演算的主要特点是使用单个变量和没有任何种类的连接或定量。最后,在[16]中,M.马克思通过用向下箭头混合逻辑的机制扩展TRC,引入了具有绑定器的关系代数(RAB)[1,4]。马克思系统的主要特征是使用个体变量和通过向下箭头绑定算子的存在隐含地使用量化马克思用表达和证明的方法对他的体系与ETBR的等价性作了语义学的证明,并把完备性作为一个问题。由于TRC是一种代数系统,RAB被引入作为代数形式主义,即,它的形式表示是项和项之间的方程。在RAB中,方程的有效性可以归结为项的某种性质。因此,之后,我们的目标是支持RAB与一组公理和推导规则,定义一个属性的可证明性,在这样一种方式,对于任何条款,我们有'i有提到的财产。 该方法的一个重要点是,而不是减少完整性问题的一阶情况下,使用[16]的结果,它决定提出一个“直接”的证明,适应混合逻辑[6]的技术。这种选择是试图从代数和模态世界中取其精华本文的其余部分组织如下。在第二节中,给出了一个带系集的关系代数[16].在第3节和第4节中,给出了公理和规则,并证明了它们的完备性。第五部分是结论,提出了一些具体的主题和问题。第2章关系代数在本节中,描述RAB的语法和语义。文中还介绍了一些在公理陈述和完备性证明中有用的简单事实。语法的基本思想是RAB是关系代数(RA)的扩展,通过引入混合#设备。RA有一组变量范围在二元关系连同一组符号的操作表示布尔和皮尔士操作的关系。杂交2081 2 1 2xGGG(v)d(;)S=d()Sj d()S.在[16]中提出的RA语言的修改涉及到在RA语法中做两个改变。首先,取一组新的变量,并将它们视为原子项。其次,添加#,向下箭头操作符,用于绑定新变量。RAB在集合fxi:i2N g上的字母表由以下符号组成:(i) 关系变量ri:i 2N。(ii) 个体变量xi:i 2N。(iii) 布尔+和。(iv) 10.根据权利要求11所述的方法,其中:(v) 向下箭头活页夹#x,其中x是单个变量。RAB的条款定义如下::=xjr j10 j +j j;j^ j编号:关系变量的集合由RVar表示,个体变量的集合由IVar表示。在混合范式下,个体变量被认为是关系而不是个体.此外,自由和约束条件下的个别变量的出现之间的区别,并subjunctions的个别变量的个别变量的条款进行。一个项的自由个体变量的集合用free()表示。当一个人为了逻辑的目的而进行替换时,他必须防止意外的约束。再一次遵循混合范式,保持这种本质上的第一秩序背后的直觉。给定一个由个体组成的域D,每个项表示D上的一个二元关系。关系变量的表示是不受限制的,而个体变量的表示则限于D上单位元以下的原子。这是一种间接的方式来表示D本身的元素。为了处理个别变量可能被绑定的事实,它们的表示由一个单独的赋值函数以一阶逻辑中熟悉的方式一个结构是一个对S = hD; Ii,其中D是一个非空集,称为S的域,和I:RVar!2DD是一个函数,称为RVar在S中的解释. IVar在S中的赋值是一个函数g:IVar!D. 给定x2 IVar和a 2 D,g在x中的a变体是赋值(a=x)g:Ivar!D使得对于每个y 2 IVaR,如果x = y,则(a=x)g(y)= a,否则g(y)。在结构S= hD;Ii和赋值g下的项的表示,记为yd()S,由y定义:(i) d(x)S=fhg(x);g(x)i g.(ii) d(r)S=I(r).(iii) d(10)S=Id.GD(iv)d(+)S=d()S[d()S.1 2g1g2g1 2g 1g2g209GXXxXxG1G2G(vi)d()S=d()S。(vii)d(x)S=(d(x)S)1。有d()Sd()S。两项和等价,记为y,如果对于nyS和g,有d()S=d()S。G gG g(viii) d(#x)S=fha;bi2DD:ha;bi2d()Sg.g(a=x)g外延的定义确保IVar中的新变量在f(a; a)g形式的所有关系的集合上变化,其中a是2 D。此外,给定项#x,运算符#x绑定x 2IVar,存储对(a; b)的第一个坐标的值a,其中,对to进行评估。一个术语非空,如果存在S,g和a; b2 D,使得ha; bi2d()S. 我们写d()S 对于Tfd()S:2G. 一组术语非-g g g空的,如果有S,g,和a;b2Dsuchthatha;bi2d()S。一个术语是一组项的结果,表示为j=,如果对于任何S和g,G gG g以下算术性质易于验证:(i)#x0 0(ii) #x11(iii) #x10(iv) #xyy(v)#x#y#y#x(vi)#x#x#x㈦ #(#)(8)#x( + )#x +#x(ix)#x()#x#x(x)#x(; #x)#x ;#x(Xi)#(;x)#10(xii) x; x x(xiii) x; yX y(xiv) X^X以下基本命题直接成立。命题2.1(一致性引理)设S是一个结构。对于S中的所有as-1,g 1和g 2以及所有项,如果g 1和g 2在free()上一致,则d()S =d()S:命题2.2(替换引理)设S是一个结构。对于所有的指派g,所有的x,y2IVar和所有的项,如果y可替换xin,则S(g(y)=x)g=d((y=x))S:在一些混合系统中,虽然单个变量表示模型的个体,但也有一个特殊的算子,允许我们跳到由变量表示的点,并查看某些公式是否为真[4]。这些d()210G、Xx赋值g和a;b2D,ha;bi2d(1;x;;y;1)Sihg(x);g(y)i 2d()S:Xx操作符作为句法和语义之间的桥梁,在某种意义上允许满意关系的内在化。在RAB中,可以通过定义来引入这样的运算符,正如人们可以从下面的命题中看到的那样。10+10这个词 表示为y1。则d(1)S=DD,对于所有结构S和赋值g。命题2.3设x; y 2为IVar,成为一个术语。 然后,对于所有结构S,G g根据命题2.3,项1; x; ; y; 1由xy表示。3公理和法则本节介绍公理和规则。利用RA与Arrow逻辑[17,18]之间存在的对偶性来建立公理系统。在这种情况下,每个公理都可以被理解为RAB的一个项,也可以被理解为通过采用复代数的已知方法从RAB获得的扩展模态逻辑的一个公式[5]。这允许使用混合模态机器来证明完整性结果。公理系统由下列公理和规则定义。随后将进行检查。项1由0表示,(+)由+的通过,()的情况下()由,(; )的方式通过+ ,^by^j,(#^)^ by“和x;1;ybyx y。RA)RA公理[23]和代数版本的公理和规则的正常模态逻辑。Below-Id)X10。非空)11; x; 1.原子)(xy 0)+(xy)。Identi er)xyxy.版本)x^yyx.比较) Xz zyX( ;)y.Bind)x#zyx(x= z)y,i fx可被yz替换。自对偶)(#)#.Q1)#x()(#x),如果x62free()。Q2)#x(y;1)(y=x),i fy可替换xin. Q3)#x(x; 1)#x.X yy z粘贴)X( ;)z,如果y是新的。低于身份证,非空和原子公理说,个别变量必须解释为低于身份证的原子。公理Rev、Comp和Identi er说我们是在解释可表示的关系代数中的项。公理211Bind在语法上表示向下箭头运算符语义。公理自对偶说向下箭头算子是它自身的对偶。最后,公理Q1、Q2和Q3说向下箭头算子是一个quantier。 规则粘贴是混合逻辑[6]中将规则粘贴到复合运算符的一个版本一个项是一个定理,记为“,如果存在一个项序列h1; :;ni,称为的pro,使得n是,对于nyi=1; :;n,i是一个公理或i是序列中前一个的结果,通过使用一些推理规则。一个术语是从一组术语中推导出来的,表示为,如果存在一个项序列h1; :;ni,称为从的导出 ,使得n是并且,对于任何i = 1;:; n,i是定理,I2 选项卡页面上创建i是使用肯定前件的序列中先前的一个结果。定理3.1(可靠性定理)如果`,则j=。完整性定理的证明使用了续集中的结果。直接从二元箭头逻辑/关系代数继承的结果被称为RA。下列项是定理:Re(ex)x10x.Simet)x10y10x。Trans)x10yy10zx10z。聪)x10zy10wx ryzrw。 Var)x10zx10yx zy。Q4)#x#y(y=x),如果y不出现在。Q5)#x(xy)(1; y #x).Q6)“x(1; y)“x。问题7)#x,if x 62free(). Q8)“x,ifx 62 free().以下规则是派生的:Nec“)“x,其中x是任何单个变量。替换项从一个项中通过替换某些出现而获得的项在一个术语中,由一个术语表示为[=]. 因为一个人有一个正常的模态逻辑,替换引理成立。引理3.2(替换)如果`,则`[=].使用替换引理和定理Q4导出字母变体引理。引理3.3(字母变体)设x; y 2是项,且是项.存在一种字母变体0 其中:(i) free()= free(0).212(ii) 的0的情况。(iii)y可替换为x,0的情况。4完备性定理在本节中,证明了,当是由于那么,可以从第3节定义的系统中导出。混合逻辑技术被用来从一个模型存在引理导出完备性结果。证明有两个阶段。首先证明了满足某些特殊条件的所有项集都是非空的。其次,证明了所有相容项集都可以用适当语言扩充为满足特殊条件的项集。一组术语已关闭,如果有、`我二、一致,如果六英尺。是完整的,如果为任何,或。有见证人,如果对所有x;y;1;2,如果x(1;2)y,则存在某个变量z,x1z,'z2y. 项xy是当xy2 .是如果存在变量x和y使得xy是的标识符,则标识。设是一组封闭的项。 单个变量x与单个变量y模全等,记为yxy,或s i mp l yxy,i fx10y2. 根据定理Reex,Simet和Trans,是一个等价关系. 因此,IVar被划分为等价类模。给定x2 IVar,x的等价类记为yxe.与一个封闭的、一致的、完全到负的、并且具有见证项集的规范结构是具有域D=fxe的结构S :x2I Varg和i解释I:R Var! 二维D满足I (r)=fhxe;yei:xry2g,对nyr2RVar. 典型的 赋值是函数g: D使得g(x)=xe,对nyx2I Var. 定理Cong保证了S的良好定义。引理4.1(真值引理)如果是封闭的,一致的,完全为负的,且有见证人,则对于allx;y,hx;yi2d()S ix y2。eeG证据通过对结构的归纳,利用替换引理(SL)、字母变式引理(AV)、替换引理(RL)、公理Rev、Comp、Bind和定理Var.情况z)hx;yi2d(z)S ig(z)=x=y(defd)eeeeG伊泽埃 =xe =ye(def(g)ix10z;x10y2(def)ixzy2(Var)情况r)hx;yi2d(r)S ihx;yi2I(r)(defd)eeeeGixry2(def S)案例10)hx;yi2d(10)S ix=y(defd)eeeeG213(xe=z)g(g(x)=z)gzn2Nn2Nfx i(i; i)z i:1我ngn时0,矛盾。ixy(defxe)ix10y2(def)情况^)hx;yi2d(^)S ihy;xi2d()S(def d)eeeeG gCase;)hx;yi2d(;)S我yx 2(I.H.)i x^y 2(Rev)ihx;zi2d()S,hz;yi2d()Seeeeeeg g g我x z; z y 2(I.H.)我x(;)y 2(Comp,has witn.)病例编号)hx;yi2d(#)S ihx;yi2d()S(def d)eeeez zg(xe=z)gihxe;yei2d(0)Sihxe;yei2d(0)Sihx;yi2d((x=z)0)S(AV)(def(g)(SL)eeG我x(x=z)0y 2(I.H.)我x编号0y 2(绑定)我x #zy2(RL)2下一个引理的证明严格遵循一阶逻辑类比。引理4.2如果是封闭和一致的,那么就有一些是封闭的,一致的,完备的。引理4.3如果相容,则r是某个集合IVar0 的个别变量和一些项的集合上的I V一个r0,这样,I V一个r0 I VAR,,并且是封闭的,一致的,并且有证人。证据通过以下规则同时定义ne hIVarn:n2Ni和hn:n2Ni(i) IVar 1= IVaR,int n= nums();(ii) IVar n+1= IVar n[ fz :2 n;] 的 形 式 为 x ( 1; 2 ) yg , n+1 =Cn(n[ fx1z;z2 y:2 n;]的形式为x(1; 2)yg)。注意到IVarn+1和n+1是由IVarn和n构造的,通过考虑形式x(1;2)y的n中的每个项,并取不在IVarn中的新的个体变量z和项x1z和z2 y。对任意n2N,nn+1,n是闭的和相容的.事实上,1=一致。 如果n是一致的,n+1不是,则存在项x11 y1,y11 z1;:,xnn yn,ynn zn 2n+1 nn使得:n; x11年1;年11z1;:; xnnyn; ynnzn`0.通过粘贴,由于yi是新的,我们有01 - 02- 03张晓波(1个;1)z1;:; x n(n;n)zn`0。以来现在,说我的话 =SIVarn 和 =S. 然后Ivar0Ivar,,是封闭的,一致的,并与证人:如果`x(1;2)y,则有2141Nx1n x1nyx1n yx1n12n2n2n2N(iii)2n+2是将引理4.3应用于2n+1的结果。G一些n2N满足n`x(1;2)y。由于n 是闭的,x(1;2)y2n。因此,x1z;z2y2n+1。2引理4.4如果是相容的,则r是某个集合IVar0 的个别变量和一些项的集合上的IVar0,这样,和是identi ed和一致的。是的。De neIVar0 =I Var[fx;y g,其中x;y62I Var且x6 =y。De ne=[fx yg. 一个是IVAR0 我是一个,,其实如果0,则由RA,xy() ,与**二、1n1n由Nec #,`#(xy())。 截至 第 5 季 度,`1; y#()的。 由Nec“,`“(1; y#())。2 0 1 6 -0 6-2 20 0 : 0 0 : 00())。 通过Q7和Q8,由于x和y不出现在,`()。0,这是一个矛盾。2现在我们把引理4.2、4.3和4.4放在一起,就可以得到关于相容集扩张的理想结果。定理4.5如果是一致的,那么使得是已识别,封闭,一致,完整到负数,并有证人。证据已知,应用引理4.4,取0一致性和一致性。然后de nehn:n2Ni通过以下规则:(一)= Cn(0)。(二)2n+1是将引理4.2应用于2n.现在带=S氮n. 一个是封闭的,组成,和com-全减。 事实上,让是这样一个术语,6`. 因此,62 .给定n2N,62. 以来完全为负数,2. 那么,2和2. 最后,“。 更重要的是,有目击者。事实上,设x; y; 1;2是这样的:“x(1;2)y。因此,存在某个n 2N使得2n+1`x(1;2)y。由于 2n+1有见证人,因此存在某个个体变量 z,使得2n+1`x1z和2n+1`z2y.因此,我们认为,x1z,'z 2y.2推论4.6(模型存在定理)如果是相容的,则是非空的。证据设是一个可识别的、一致的、封闭的、完全到负数的、有见证人的项集,包括。设xy是的标识符。设为.然后二、因此,根据公理Identier,xy2,因此,利用Truth引理,(xe;ye)2d()S.2最后,它遵循完备性定理。推论4.7(完备性)如果 j=,则 “的意思。2155透视具有绑定器的关系代数(RAB)是经典关系代数语言的扩展,具有向下箭头混合绑定器的机制这种扩展增加了语言的表达能力和证明能力。在[16]证明了二元关系的任何一阶性质都可以用扩展语言表示。本文提供了一个完备性结果,表明任何这样的性质是有效的,也可以证明。其目的不是利用[16]的结果将完备性问题简化为一阶逻辑的完备性问题,而是提出一个“直接”证明,采用著名的规范模型方法。事实上,这里提出的公理非常简单,使系统成为一个非常优雅的公式。 中讨论的示例[16] 为关系代数和混合逻辑提供了新的视角本文的工作是一种尝试,以促进这一发展。本文提出了RAB的一些具体的主题和问题,并对RAB的发展前景进行了展望.本文提出的公理最直接的问题是是关于他们的独立性有多少公理和规则可以删除而不损失证明力?作为表达性结果的推论,它遵循RAB的Craig插值定理的一个版本。一个未来的任务是定义的RAB的微积分,以获得一个建设性的证明这个插值定理。RAB的一个重要特征是没有公式,即,RAB是一个术语系统,在表达和证明上与ETBR是等价的。在[9]中引入了一个等价于一阶逻辑的项系。一个非常有趣的研究主题可能是RAB和该系统之间的关系。确认感谢M。马克思提出了许多富有启发性的讨论和许多改进的建议。引用[1] 阿雷斯角,Blackburn,P.,和马克思,M.,混合逻辑:特征化,插值和复杂性,符号逻辑杂志,66(2001)977{ 1010。[2] Bir o,B.,代数逻辑中的非有限公理化结果,符号逻辑杂志,57(1992)832{843。[3] 布林克角,卡尔,W.,Schmidt,G.(编辑),《计算机科学中的关系方法》,Springer,纽约,1997年。216[4] Blackburn,P.,表示,推理和关系结构:混合逻辑宣言,逻辑杂志的IGPL,8(2000)339{365。[5] Blackburn,P.,de Rijke,M.,和Venema,Y.,《模态逻辑》,剑桥大学出版社,2001年。[6] Blackburn, P. ,和 Tzakova, M., 混合 完备 性,逻 辑学报, 6(1998 )625{650。[7] Givant,S.,塔斯基的发展逻辑和数学的基础上演算的关系在安德烈·埃卡,H.,蒙克,J.D.,和Nemeti,I.(编辑),《代数逻辑》,《数学学会学术讨论会》,54,北荷兰,阿姆斯特丹,1991,189{215.[8] Henessy,M.C.B.,一阶关系演算的证明系统,计算机与系统科学杂志,20(1980)96{110。[9] Hermes,H.,“带选择算子的项逻辑”,《数学讲义》,第6期,柏林,1970年。[10] J onsson , B. , Varieties of relation algebras , Algebra Universalis , 15(1982)273{ 298.[11] L或温海姆湖,447{470.UberM在Relativkalku中的oglichkeiten我,数学。安,第七十六条(一九一五年)[12] 林登河关系代数的表示,数学年鉴,51(1950)707{729。[13] Maddux,R. D.,一个关系代数的微积分,纯逻辑与应用逻辑年鉴,25(1983)73{101。[14] Maddux,R. D.,圆柱代数和关系代数的非有限公理化结果,符号逻辑杂志,54(1989)951{974。[15] Maddux,R. D.,关系代数In C.Brink,W.Kahl和G.Schmidt(eds.),计算机科学中的关系方法”,Springer,Wien,1997,22{38.[16] 马克思,M.,具有绑定器的关系代数,逻辑与计算杂志,11(2001)691{700。[17] 马克思,M.,波罗斯湖,和Masuch,M.(编辑),《Arrow Logic andMulti-Modal Logic》,CSLI,Stanford,1996。[18] 马克思,M.,和Venema,Y.,《多维模态逻辑》,应用逻辑丛书第4期,Kluwer学术出版社,1997。[19] 塞恩岛关于一阶逻辑的可初始化代数化的研究,逻辑学报,8(2000)497{591。[20] SCHOnfeld,W.,关系方程的序列演算中的前向搜索的上界。F. Logik undGrundlagen d.数学、28(1982)239{246.217[21] 塔斯基,A.,关于关系演算,《符号逻辑杂志》,6(1941)73{89。[22] 塔 斯 基 , A. , 和 Givant , S.R. , \A formalization of set theory withoutvariables” , Colloquium Publications , 41 , American MathematicalSociety,Providence,R.I.,1987.[23] 维内马,Y.,箭逻辑速成班。在[17],3{34。[24] Wadge,W. W.,《关系演算的一个完全自然演绎系统》,计算理论报告第5号,华威大学,1975年。
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功