重叠逻辑的不可判定性及离散线性序：理论计算机科学电子笔记

理论计算机科学电子笔记262（2010）65-81www.elsevier.com/locate/entcs重叠逻辑的不可判定性离散线性序达维德·布雷索林1意大利维罗纳大学Dario Della Monica2意大利乌迪内乌迪内大学Valentin Goranko瓦伦丁·戈兰科3，6丹麦技术大学，Lyngby，丹麦Angelo Montanari4意大利乌迪内乌迪内大学Guido Sciavicco Guido Sciavicco5，6西班牙穆尔西亚穆尔西亚大学摘要大多数命题区间时态逻辑的有效性/可满足性问题是（高度）不可判定的，在对它们被解释的区间结构类的非常弱的假设下。这一点尤其适用于Halpern和Shoham的区间模态逻辑HS的大多数片段。尽管如此，可判定性是规则的片段HS只有一个模态算子，基于艾伦的关系。在本文中，我们表明，逻辑O的重叠关系，在离散线性序解释时，是一个例外。证明是基于减少从不可判定的八分区平铺问题。这是HS片段的最尖锐的不可判定性结果之一关键词：区间时序逻辑，重叠关系，不可判定性，八分块镶嵌问题1电子邮件：davide. univr.it2电邮地址：dario. dimi.uniud.it3电子邮件：vfgo@imm.dtu.dk4电子邮件：angelo. dimi.uniud.it5电子邮件：guido@um.es6这些作者得到了西班牙-南非项目n的部分支持。HS 2008 -00061571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.04.00666D. Bresolin等人/理论计算机科学电子笔记262（2010）651引言线性时态逻辑是模态逻辑，其框架是线性有序结构。大多数线性时态逻辑在模型中解释，其中点是原始的本体实体，并且（时态）公式的真实性在时间点上进行评估。时间域的不同选择（离散、密集、戴德金完备等）对于时态算子（F，P，Next，Until，etc.）导致不同基于点的线性时间逻辑。然而，表示和推理时间间隔的能力在各种计算机科学领域都是需要的，包括自然语言处理，约束满足问题，行为和变化理论，时态数据库，并发和实时系统的规范和验证[8，12]。与基于点的时态逻辑不同，区间时态逻辑假设时间区间为其原始本体实体，并且所有公式都相对于区间而不是点进行评估。线性序上区间之间各种关系的系统描述首先由Allen [1]在代数环境中讨论艾伦区间代数的模态逻辑对应物因为HS的每个公式都被解释为二元关系，而不是一组点，HS的有效性/可满足性问题在非常弱的假设下是高度不可判定的。特别是，当在任何一类线性有序结构上解释时，HS是不可判定的，这些结构包含至少一个具有无限上升或下降链的线性有序，因此包括N， Z， Q和R[9]。HS的不良计算行为激发了对其片段家族的系统分析，以寻找足够表达但可判定的片段，并且更普遍地，在区间逻辑领域中，寻求确定可判定性和不可判定性在这个方向上的第一个主要步骤是由Halpern和Shoham自己在他们的原始论文中采取的，他们在论文中表明，即使将逻辑限制在其ABE片段中，HS的不可判定性结果也是成立的（我们使用以下符号：“XY ...... Z '是HS的片段，仅涉及对应于关系X，Y，.的模态，Z），并建议研究较弱或不可比的有意义的片段，如BE和DD。Lodaya在近十年后证明了BE在稠密线性序上的不可判定性[10]，而DD在Q上的可判定性才刚刚建立[11]。最近对HS的重要可判定片段的识别，例如各类线性序上的区间邻域AA的逻辑[6，7]和稠密序上的子区间关系D的逻辑[5，13]，为HS片段的研究带来了新的兴趣。关于可判定性/不可判定性的HS片段的部分分类，反映了最新的技术水平，可以在[3]中找到。此后在[4]中获得了进一步的不可判定性结果。虽然不可判定性在HS片段的完整集合中占主导地位，但判定-D. Bresolin等人/理论计算机科学电子笔记262（2010）6567∈⟨⟩∈≤⟨ ⟩ ¬⟨ ⟩¬¬ ∨AP能力通常是涉及仅一种模态的HS片段的情况，这使得该片段集合特别有趣。 B，B，E，E的可判定性可以很容易地通过简化为基于点的逻辑来显示。 A，A的可判定性，以及L，L（分别用A，A定义）的可判定性已经建立在[6，7]中，通过不同的模型理论参数，每个参数都意味着这些逻辑的小（非标准）模型属性;同样对于D在稠密线性序上的可判定性（证明也可以适用于D的情况）。 D的可判定性然而，在一般的、有限的或离散的线性排序上，仍然是开放的。在这项工作中，我们表明，O（因此O，这是对称的）是迄今为止唯一被证明的例外，从可判定性的趋势，尽管它的简单性和有限的表达能力。 本文的主要结论是，O（相应地，O），在离散线性序上解释，是不可判定的。这个结果加强了在[4]中得到的那些，当语义被限制为离散线性序时，对于O的许多扩展。[2]），这是确定给定的有限组瓦片类型是否可以平铺整数平面的第二个八分圆的问题，考虑垂直或水平相邻的瓦片对之间的颜色约束。本文的结构如下。在第2节中，我们介绍了片段O的语法和语义，在离散线性排序上解释。在第三节中，我们简要地说明了不可判定性证明的结构。在第四节中，我们给出了详细的说明。结论提供了工作的评估和未来的研究方向。第二章重叠O的逻辑：语义和语义设D=D，是离散线性序集。 D上的区间是一个有序对[a，b]，其中a，b为D和a b，因此不包括端点重合的区间（严格语义）。对于任何区间[a，b]，我们定义[a，b]的长度，记为len（[a，b]），作为集合{a，...，b}减1，例如， 三点间隔的长度是2。作为替代，可以将D上的区间定义为一对[a，b]，其中a，bd和b（非严格语义）。 从今以后，我们限制我们注意严格的语义;然而，所有的证明都可以很容易地适应非严格的情况（如果允许或不允许点间隔，它没有区别，因为O-公式只能谈论当前的间隔或长度大于或等于2的间隔）。逻辑O的特点是命题字母的无限集合，经典连接词，（其余的被认为是缩写），和一元模态算子O（对偶算子[O]通常被定义为O）。合式公式，记为，，。. . ，通过以下抽象语法获得：：= p |¬ ϕ |ϕ ∨ ϕ|你好。O的一个模型是一个形式为M=I（D），V（D）的结构，其中I（D）是D上所有区间的集合，V：AP <$→ 2I（D）给每个p∈ AP分配一个区间68D. Bresolin等人/理论计算机科学电子笔记262（2010）65O××∗T {} O ∈ T×OV（p），它在其上保持。模型M中给定区间[a，b]上公式的真值由公式的结构归纳法定义• M，[a，b]Dpi<$[a，b] ∈V（p），对所有p∈ AP;• M，[a，b]D<$i，则M，[a，b]D<$i不是这样的情况;• M，[a，b]DiM，[a，b]D或M，[a，b]D;• M，[a，b]D<$O<$$>i <$存在一个区间[c，d]使得a c b d，并且M，[c，d]D.像往常一样，我们有一个O-公式是满足的，如果它在某个区间上为真， 如果它在每个模型中的每个区间上都为真，则它是有效3关于不可判定性证明的直观说明在这一节中，我们给出了不可判定性证明的结构的直观说明。我们已经从整数平面的第二个八分圆的平铺问题中利用了一个简化来证明各种HS片段的不可判定性[3，4]。然而，逻辑O所具有的重叠模态的性质在很大程度上限制了归约的技术性3.1整数平面第二个八分圆O的镶嵌问题设O={（i，j）：i，j∈ N <$0≤ i ≤ j}为整数平面的第二个八分圆ZZ的平铺问题是确定给定的瓦片类型的有限集合是否=t1，.，tk可以平铺。 对于每个瓦片类型t，，让 右（ti）、左（ti）、上（ti）和下（ti）是ti的对应边的颜色。为了解决这个问题，我们必须找到一个函数f：O → T，使得right（f（n，m））=left（f（n+1，m）），其中n m，并且up（f（n，m））=down（f（n，m+1））。利用柯尼希第一种是不确定性，第二种是不确定性，第三种是不确定性。3.2O的平铺问题的编码从平铺问题到满足性问题给定区间时态逻辑利用了一些特殊的命题字母，即u，Id，tile，，uprel，t1，t2，.，t k。附加的（不同的）命题字母引入不同的逻辑。对于每一个命题字母p，p-区间指的是一个满足p的区间。约简由三个主要步骤组成：（i）通过合适的间隔链（称为“单位”间隔（简称u -间隔））对八分区进行编码在第一步中，我们通过强制存在唯一的无限链来设置框架线性序上的u-区间（简称u-链）。 使用u-区间作为细胞来排列平铺。接下来，我们定义一个Id-区间链（Id-链，D. Bresolin等人/理论计算机科学电子笔记262（2010）6569∗OTT{}⟨ ⟩每一个都代表一行八分圆。 任何Id-间隔都由以下各项组成一个u-区间序列;每个u-区间用来表示平面的一部分或分隔两个Id-区间。在前一种情况下，它被标记为命题字母瓦片，在后一种情况下，它被标记为命题字母. 然后，我们定义两个关系，分别将每个图块与八分圆中的上邻居和右邻居（如果有的话）连接起来。利用这些关系，我们强制第j个Id区间恰好包含j个tile区间.最后，我们引入一组命题字母T= {t1，t2，...，t k}对应于图块类型的集合=t1，t2，...，tk我们定义了一个公式Φ T，当且仅当存在一个适当的平铺，通过，也就是，一种满足于对垂直和水平相邻图块的颜色约束3.3逻辑O与 u-链的构造在处理逻辑O时，我们必须解决的主要问题是构造u-链：我们必须指定如何从给定的u-区间仅使用运算符O到达下一个u -区间。我们通过利用线性序的离散性来解决这个问题：我们建立一个相邻u-区间的链，每个区间的长度为2。为此，我们使用一组附加的命题字母，即u1，u2，u，k1，k2，k，beginu1，beginu2，begink1，begink2。更准确地说，为了限制u-区间的长度，我们首先强制每个u-区间的每个内部点都是无限多个开始u-区间的起点，然后我们约束每个开始u-区间不与任何其他开始u-区间重叠。通过这种方式，我们将每个u-区间约束为恰好有一个内点（图1）。此外，为了使连续的u-区间对相邻，我们利用k-区间的辅助链，每个k-区间的长度也是2，使得每个k-区间的端点是两个连续u-区间的（唯一的）内点（图2）。2）。4离散线性序上逻辑O的不可判定性在本节中，我们正式证明了逻辑O，在离散线性序上解释，是不可判定的。a B a BC def图1.一个不一致的情况是u区间[a，b]的长度大于2，并且存在两个开始于它内部的u区间，它们重叠（左），另一个正确的情况是u区间[a，b]的长度等于2，并且所有开始于它内部的u区间都不重叠（右）。CDeF70D. Bresolin等人/理论计算机科学电子笔记262（2010）65≥G≥Gu u u u u u u u uk k k k k k k k图2.u-区间是相邻的，并且每对连续的u-区间由k-区间连接4.1u链的定义u链的构造可以形式化如下。对于任意区间[a，b]，len（[a，b]） 2、让[a，b]是包含区间[a，b]所有的区间[c，d]，len（[c，d]）2，开始于a之后，结束于b之后。此外，让[G]（总是在未来）是下面的导出运算符：[G] p p [O] p [O][O] p.不难证明[G]p在区间[a，b]上成立，其中len（[a，b]）≥2，当且仅当p在[a，b]中的每个区间上成立。 设[a，b]是我们计算公式的区间（技术上讲，是u链开始的右边的区间）。我曾以自己为榜样，以自己为榜样。区间组）属于（分别，包含在）G[a，b]中。为了定义u链，我们使用以下公式：[G]（（kParticlek1<$k2）<$（uParticleu1<$u2）<$（k1→ <$k2）<$（u1→< $u2））（1）[G]（k1→ <$O<$u1）<$（u1→ <$O <$k2）<$（k2→ <$O <$u2）<$（u2→ <$O<$k1））（2）<$u<$k[O]<$u[O]<$k2 Ok1（3）公式（1）-（3）强制存在一个无限的重叠区间链，其中k-和u-区间以规则的方式交替。更准确地说，u-间隔（分别为，k-区间）被划分为u1-区间和u2-区间（分别，k1-和k2-区间）（公式（1））。每个k1-区间（分别，u1-，k2-，u2-间隔）与至少u1-间隔（分别，k2-，u2-，k1-区间）（公式（2））。 链的第一个区间是k1-区间（公式（3））。 正如我们将进一步展示的那样，下一个公式约束 u- 和k-区间的长度都等于2：[G]（（u1→ [O]beginu1）<$（u2→ [O]beginu2）<$<$（k1→ [O]begink1）<$（k2→ [O]begink2））[G]（u2k1k2）→ <$$>Obeginu1）<$（（u1k1k2）→<$$>Obeginu2）<$<$（（k2<$u1<$u2）→ <$$>O<$begink1）<$（（k1<$u1<$u2）→<$$> O <$begink2））[G]（（beginu1 <$$> O <$beginu2→<$$> O <$beginu1）<$（beginu2 → <$Obeginu2）（begink1 → <$Obegink1）（begink2 → <$Obegink2））（四）（五）（六）（1）无. （6）（7）D. Bresolin等人/理论计算机科学电子笔记262（2010）6571公式（4）-（6）迫使第一个k1-区间从初始区间[a，b]的最后一个内点开始，并且每个k1-区间（分别，ui-区间）满足k3−i-区间72D. Bresolin等人/理论计算机科学电子笔记262（2010）65/∈ G≥⟨ ⟩（分别地，u3−i-interval），紧随其后。引理4.1如果M，[a，b] D（7），则存在无穷多点序列c1 ci（分别地，c > ci，c > bi，c > bi）对于每个i > 0。证明语句1-3的证明是通过指数i和j上的互感来实现的序列c1c2<<。. . 和b12。 这意味着至少有一个点bJ使得c bJ 0，c > bi（对于u2，k1和k2也是一样）。通过矛盾，假设存在这样一个区间[c，d]。从（1）和（3）可以直接得出，[a，b]既不满足u1，也不与满足u1的区间重叠，因此c b。给出了u-链和k-链的性质，以下三种情况：• 如果对于某个奇数i，c = bi，则d >bi+1。由于[ci+1，ci+2]是一个k2-区间，对任意e > d，区间[bi+1，e]是一个与u1-区间[c，d]重叠的开始k2-区间，与（5）的第四个合取式• 如果对于某个偶数i，c=bi，那么，通过（1）的最后一个合取，d >bi+1;我们应用于前一种情况的完全相同的论点产生矛盾;• 如果对于某个奇数（分别地，even）i，则d≥ci+1，并且对于任何e > d，区间[bi，e]是开始k1-区间（分别地，begink2-interval）与u1-interval [c，d]重叠，与第三个（分别，第四，（5）。同样的论证可以应用于u2-、k1-和k2-区间的情况（事实上，在k1-区间的情况下，我们必须考虑到，通过（3），[a，b]与序列的第一个k1-区间重叠;然而，证明本质上仍然是相同的）。Q推 论 4.2 若 M ， [a ， b] D （ 7 ） ， 则 存 在 无 穷 点 列 c1 b1（分别地， c> ci）对于每个i> 0。我们通过引入算子Xu来结束这一节，它允许从一个u-区间步进到下一个：如果在初始区间[a，b]上或在u-区间上求值，当且仅当p在下一个u-区间上成立时，Xup其正式定义如下：Xu74D. Bresolin等人/理论计算机科学电子笔记262（2010）651111J∗∗∗∗j+1j+1j+1JJj+11j+1JJJJj+1J JJJ J4.2Id链的定义为了定义Id链，我们利用以下公式集（8）第一章：Xu[G]（Id→O（k）O（k））（12）[G]（k→< $O）（13）[G]（u= 0）[G]（O→OId）（15）（8）无... （15）第16章：一个人的世界引理4.3设M，[a，b] D（7）≠（16）且设c0 1，kl> 2，没有其他区间[c，d] ∈ G [a，b]满足（ 分别为， tile，Id），除非对于每个i，j> 0。证明a）首先，由于（9），（11）和（12），观察到存在一个无穷区间序列。让我们用[b0，b1]，[b0，b1]，.，[b0，b1]，. 这样的1122jj顺序通过（10）的第一个合取式，我们可以假设不存在任何时间间隔在[b0，b1]和[b0，b1 ]之间，对于每个j>0。j j j+1j+1b) 由于通过（10），每个满足或tile的区间都是u-区间，并且每个u-区间满足或tile，任何两个-区间之间的u-区间（如果有的话）必须是tile-区间。c) 通过（11），对于每个k-区间[b0，b1]，存在从c1开始的Id-区间，并且在某个点结束，比如说cJ。 我们想证明cJ= b0，也就是Id-区间[b0，b1]在下一个区间的开始点结束，间歇。 假设，通过矛盾，cJ=b0，并考虑以下内容案例：• 如果cJc1，则（15）是矛盾的，因为区间[c0，c1]重叠j+1n-区间[b01j+1]和Id-区间[c1，CJ]。1j+1d) 通过（9），立即得出k1= 2，并且当l>1时kl>2最后，通过矛盾，假设存在Id-区间[c，d] ∈ G[a，b]，bD. Bresolin等人/理论计算机科学电子笔记262（2010）6575t54t42t1t3211不12t2t23t33314t4t4t453t5t52t51t5x`最后最后最后∗1∗12∗t1 t2 t2t3t3 t33 2 1∗x `X`最后t42t4 t43 4˛1t4JJJj+1JOOJ⟨ ⟩Jj+1J（a）（b）bfbfbb f b f图3. 从后向开始的上行相对间隔（分别地，前）八分圆的行不重叠。使得对于每个j > 0，[c，d]=[c1，b0]，且对于某些i，j> 0，c ≤ bi。通过（8），区间[a，b]既不满足Id，也不与满足Id的区间重叠，因此c≥b，出现下列情况之一。 1）若c=bi，其中i≥0，j > 0，则（13）矛盾。2）若c=ci，其中i≥ 0，j>0，i为1，则（14）为反驳。3）如果c=c1，对于某个j>0，那么我们已经证明了它必须d = b0。 没有其他区间[c，d] ∈ G [a，b]满足最小或最小，除非对于每个i，j> 0，c > b i可以通过类似的论证来证明。Q4.3上邻关系我们现在继续上面的邻居关系，其编码如图3所示。直观地，上方相邻关系将每个图块间隔与其在八分圆中的垂直相邻者（例如，图中的t2和t33）。如果瓦片t连接到2 2通过上邻关系，我们简单地说t上连接到tJ。为了对这样的关系建模，我们使用由up rel标记的区间，即，up rel-区间连接成对的瓦片-区间编码八分区的上方连接的瓦片对我们使用命题字母b和f区分的向后和向前行：我们用b标记每个u-区间（分别，如果它属于一个落后的（分别，向前）行（公式（17）-（18））。直观地说，属于的前向行的图块按升序编码，而属于后向行的图块按升序编码。以降序编码（以Z字形方式编码平铺）。特别地，这意味着后向级别的最左边的瓦片间隔在O中编码该行的最后一个瓦片（而不是第一个瓦片）设α，β∈ {b，f}，其中αi =β：<$Xu <$b <$[G]（（u Particib <$f）<$（b → <$f））（17）[G]（（α<$$><$$> Xu<$$> → <$Xu <$α）<$（α <$$> Xu <$$> →<$Xu <$β））（18）（17）.（18）第19集引理4.4如果M，[a，b]D（7）<$（16）<$（19），则存在类似于引理4.3中定义的点序列，使得M，[bi，bi+1]Db当且仅当j是奇数J J数和M，[bi，bi+1] D f当且仅当j是偶数。此外，我们有J J没有其他区间[c，d] ∈ G[a，b]满足b或f，除非c> bi对于每个i，j> 0。我们利用这种前后行的交替来使用操作符O来正确地编码上面的邻居关系。我们76D. Bresolin等人/理论计算机科学电子笔记262（2010）65约束每个向上的相对间隔从一个向后的（分别，前向）行不与从后向（相应地，向前）行。结构D. Bresolin等人/理论计算机科学电子笔记262（2010）657733j+1O--≥∧ ∧∧eOeOeγδγγJJJγ在图3中示出了编码的基本过程，其中从内部前向开始的上行相对间隔（分别，向后）行被放置在其他行的内部。例如，考虑图3b中的第3行和第4行。第3行的第1个区块间隔（t3）与第4行的倒数第二个区块间隔（t4）相连，第3行的第2个区块间隔（t3）与第4行的倒数第三个区块间隔（t4）相连，依此类推2 2请注意，在转发（分别）中，后行，最后一行，首先，tile-interval没有与之连接的tile-interval，以约束每行比前一行多一个tile-interval（这些tile-interval标记为last）。形式上，我们定义上面的邻居关系如下。如果[bi，bi+1]是一个图块，J J属于前向的间隔（分别，我们说：“上有上有下，下有上有下。与瓦片-i nter val[bj+2-i，bj+2-i+1]连接（分别地， [bj+2−i−1，bj+2−i]）。WE帽-j+1j+1j+1j+1通过使用上相对输入值[ci+1，cj+2-i+1]（分别，[ci+1，j j+1jcj+2−i]）。更进一步，我们区分从前向行和后向行开始的向上的相对值，以及对于这些情况中的每一种，区分从奇数和偶数瓦片间隔开始的相对值。 为此，我们使用一个新的命题字母，即up relb（resp.，up relb，up relf，up relf）标记uprel-从奇数开始的欧欧欧瓦片-向后行的间隔（分别，偶数瓦片-间隔/后向行、奇数/前向、偶数/前向）。此外，为了便于公式的阅读，我们将relb和up relbinup relb（up relbParticipup relbparticipatingup relb），对于up relf也是如此。最后，up rel恰好是up relb和up relf中的一个（up rel up relb上相对于f）。 以这样 一种方式是，我们对由上述相邻关系引起的平面的连续行的瓦片之间的对应进行设α，β∈ {b，f}和γ，δ∈ {o，e}，其中αi =β和γi =δ：[G]（（up relParticipup relbup relf）<$（up relαParticipuprel αup relα））（20）[G]（k→< $O）（21）[G]（uO uprelα → <$$> Oup relα <$Oup relβ）（22）[G]（up relα→< $Oup relα）（23）[G]（up relα→<$O（tile<$Oup relβ））（24）（20）... （24）第25章：一个人的世界引理4.5如果M，[a，b]D（7）（16）（19）（25），则存在类似于引理4.3中定义的点序列，使得对于每个i0，j > 0，以下性质成立：a) [c，d]满足rel当且仅当c=ci，d=diJ对于某个i，iJ，j，jJ>0，即，jjJ每一个上行相对间隔在u间隔内开始和结束;b) [ci，ciJ]满足up rel当且仅当它满足up relb和jjJuprelf和[ci，ciJ]满足up relb（分别为， up relf）当且仅当它完全满足jjJ一个在UPRELB和UPRELB之间（分别，在up_rel_f和up_rel_f之间）;欧欧欧c) 对于每个α，β∈ {b，f}和γ，δ ∈ {o，e}，如果[ci，ciJ]满足relα，则有78D. Bresolin等人/理论计算机科学电子笔记262（2010）65Jδγδ没有其他间隔从满足up relβ的ci开始，使得up relαi =up relβ;D. Bresolin等人/理论计算机科学电子笔记262（2010）6579∧ ∧ ∧∧JJβαd) 每个上行Relb间隔（分别，UP_RELF-间隔）不与任何其它UP_RELB-间隔（相应地，up relf-interval）;e) 如果[ci，ciJ]满足relb（特别是，uprelb，uprelf，uprelf），则[biJ−1，biJ]满足jjJ欧欧欧jJjJ瓦片并且存在上行相对间隔（分别地， 上相对f-间隔，上相对b-间隔，欧埃欧上RelB-间隔）。ejJ现在，我们约束每个图块间隔，除了代表最后一个图块的间隔之外， 为此，我们用新的命题字母last（公式（33）-（35））来标记表示八分圆的某行的最后一个瓦片的每个瓦片间隔。接下来，我们强制所有且仅那些未标记为last的瓦片区间具有与它们连接的上方瓦片区间（公式（36）-（39））：uprel[G]（tile→tiny）（27）[G]（uO uprel →tile）（28）[G]（α→ [O]（up rel→uprelα））（29）[G]（up relα→Oβ）（30）[G]（O→ <$（Oup relbOup relf））（31）[G]（tileOuprelαXutile →X u（tileO uprelα））（32）γ δ[G]（最后→瓷砖）（33）[G]（（b→X ulast）（fXu→last））（34）[G]（（lastf→Xu）（bXulast →））（ 35）[G]（f→Xu（tileO（up relO（tile Xu ）（36）[G]（lastb → O（uprelO（tileXu（tileXu ）（37）[G]（kO（tileOup relα）→ [O]（Oup rel αO（kγ γ（38）O[G]（up rel → <$O last）（39）（26）. 中国（40）引理4.6如果M，[a，b] D（7）（16）（19）（25）（40）则存在一个序列对于像引理4.3中定义的点，使得以下性质成立：a) 对于每个上Rel-interval[c，d]，存在CJ，CJ，DJ，DJ，其中cj<，cj<，<j+1，则考虑属于（j+1）的瓦片区间[ b h，b h+1]。thr ow. 根据引理4.4，我们知道[bh，bh+1]满足f（因为[bi−1，bi]j+1j+1j j满足b），通过（27）和（29），我们有一个向上的相对f-区间从ch+1在某个点chJ对于某个jJJ>j+1（由第（i）点）。考虑下一个区间[b01j+2].我们知道，[c0，c1 ]与n-区间[b0，b1 ]重叠， 上相对f-区间[ch+1，chJ]以及上Relb-间隔[Ci，Ci，J]，矛盾（31）。jjJ因此，唯一的可能性是jJ=j+1。Q引理4.7每个瓦片-区间[bi，bi+1]与恰好一个瓦片上连接-J J如果[bi，bi+1]不满足last，则恰好存在一个tile-intervalJ J与之相联系首先，我们观察到每个瓦片区间通过（27）和引理4.6项（a）与至少一个瓦片上连接。现在假设，为了矛盾，存在一个tile-interval [bi，bi+1]不满足last，使得有J J上面没有与之相连的瓦片间隔 如果[bi，bi+1]是J J第j个Id-区间不满足last（基本情况），且满足f（分别为， b），则我们有i=kj2（分别，i= kj1）和（37）（分别，（36））保证了在Ci+1处结束的上行Rel-interval的存在，从而导致矛盾。否则，如果[bi，bi+1]不是第j个Id-interval的最右边的区间，J J则应用归纳情况。 因此，我们可以假设归纳假设，存在结束于Ci+2处的上行Rel-Interval从某个点ciJ开始j−1. 我们我想说明还存在一个结束于Ci+1的上行Rel-interval。不失，b82D. Bresolin等人/理论计算机科学电子笔记262（2010）65eeJJj+1j+1Oj+1j+1j+1eJ JOeJej+1OJJJOeJOJj+1一般性地，假设[ciJ，ci+2]满足relf。 然后，根据引理4.5，项（e），j−1JO存在从Ci+2开始的上RelB-区间，并且通过严格交替性质，oj（引理4.6，项（b）），存在从ci+1开始的向上relb-区间。 我们表明eJ通过将（38）应用于k-i个整数val[ciJ-1，ciJ]，我们得到一个conntradiction。的确，Jj−1j− 1J[ci−1，ciJ]满足k O（tileOup relf），并且它与[bi−1，bi]重叠，满足j−1j− 1oj−1j下式：• CNOWUP R