Kamp定理的一个证明
A Proof of Kamp's theorem
摘要：
给出了Kamp定理的一个简单证明。
英文摘要：
We provide a simple proof of Kamp's theorem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
相关论文
单时钟ATA的Büchi-Kamp定理
Büchi-Kamp Theorems for 1-clock ATA
本文研究了1-时钟交替时间自动机（1-ATA）及其自然子类的Kamp-like和Büchi-like定理。定义了具有无环复位的1-ATA的概念。这个自动机类被证明是表达等价于时间逻辑$\regmtl$，这是$\mathsf{MTL[F_I]}$扩展与正则表达式守护模态。此外，还引入了具有k-变连通性的未来时控MSO的子类逻辑$\qkmso$ .在类似坎普的结果中，它表明，$\regmtl$是表达等价于$\qkmso$。作为我们的第二个结果，我们定义了合取-析取1-时钟ATA（$\wf$ 1-ATA）的概念。我们表明，$\wf$ 1-ATA与无环复位表示等价的子逻辑$\F\regmtl$的$\regmtl$。此外，$\F\regmtl$在表达上等同于$\qtwomso$，即$\qkmso$的两个可变连接片段。1-ATA的全类被证明是表现等价于$\regmtl$扩展与不动点算子。
cs.LO
同伦型理论中高阶归纳型的道路空间
Path Spaces of Higher Inductive Types in Homotopy Type Theory
等式类型的研究是同伦类型论的核心。描述这些类型通常很棘手，并且已经开发了各种策略，例如编码-解码方法。我们证明了一个定理的平等类型的coequalizers和pushout，让人想起一个归纳原则，没有任何限制的截断水平。这一结果使得有可能直接推理某些等式类型，并通过消除辅助结构的必要性来简化现有的证明。为了证明这一点，我们给出了一个很短的参数计算的基本群的圆（利卡塔和舒尔曼'13），并为事实，即推出保持嵌入。此外，我们的发展提出了一个更高版本的Seifert-van Kampen定理，并且集合截断算子将其映射到标准的Seifert-van Kampen定理（由于Favonia和Shulman '16）。我们提供了证明助理精益的主要技术成果的形式化。
cs.LOmath.LO
Stavi定理的一个证明
A Proof of Stavi's Theorem
本文给出了Stavi定理的一个简单证明，该定理表明带有Until、Since及Stavi模态的时态逻辑在所有线性序上与FOMLO表达等价。
cs.LO
Dilworths定理和Mirskys定理的全机械化证明
Fully Mechanized Proofs of Dilworths Theorem and Mirskys Theorem
在Coq证明助手中给出了Dilworths定理和Mirskys定理的两个完全机械化的证明。Dilworths定理指出，在任何有限偏序集（偏序集）中，最小链覆盖和最大反链的大小是相同的。Mirskys定理是Dilworths定理的一个对偶。我们用Perles [2]（对Dilworths定理）和Mirsky [5]（对对偶定理）形式化了证明。我们还提出了一个图书馆的定义和事实，可以作为一个框架，形式化其他定理的有限偏序集。
cs.DMcs.LO
