Succinctness of Order-Invariant Logics on Depth-Bounded Structures

Succinctness of Order-Invariant Logics on Depth-Bounded Structures
复制标题

深度有界结构上的阶不变逻辑的简洁性

DOI:
10.1145/3152770
复制
发表时间:
2017
期刊:
ACM Transactions on Computational Logic (TOCL)
影响因子:
--
通讯作者:
F. Harwath
F. Harwath
中科院分区:
--
文献类型:
--
作者:
K. Eickmeyer;M. Elberfeld;F. Harwath

文献摘要

参考文献

被引文献

相似文献

研究了一阶逻辑和一元二阶逻辑的序不变句在有界树深结构上的表达能力和简洁性。一般来说,顺序不变是不可判定的,因此,人们努力寻找具有与顺序不变句子相同表达能力的可判定语法的逻辑。我们表明,在有界树深度的结构,顺序不变的FO具有相同的表达能力FO。我们的证明技术允许对这种翻译的简洁性进行细粒度的分析。我们证明了,对于每一个顺序不变的FO句子存在一个FO句子,其大小是小学的原始句子的大小,其数量的交替是线性的树深度。我们得到类似的结果MSO。MSO和FO的表达能力在有界树深结构上是一致的。我们提供了一个翻译MSO FO,我们表明,这种翻译基本上是最佳的公式大小。作为进一步的结果,我们表明,顺序不变的MSO具有相同的表达能力,FO与有界树深度结构上的模计数量词。
We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on structures of bounded tree-depth. Order-invariance is undecidable in general and, thus, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on structures of bounded tree-depth, order-invariant FO has the same expressive power as FO. Our proof technique allows for a fine-grained analysis of the succinctness of this translation. We show that for every order-invariant FO sentence there exists an FO sentence whose size is elementary in the size of the original sentence, and whose number of quantifier alternations is linear in the tree-depth. We obtain similar results for MSO. It is known that the expressive power of MSO and FO coincide on structures of bounded tree-depth. We provide a translation from MSO to FO and we show that this translation is essentially optimal regarding the formula size. As a further result, we show that order-invariant MSO has the same expressive power as FO with modulo-counting quantifiers on bounded tree-depth structures.
加法不变 FO 和正则性
DOI: --
发表时间: 2010
期刊: 2010 25th Annual IEEE Symposium on Logic in Computer Science
影响因子: --
作者:
Nicole Schweikardt;L. Segoufin
通讯作者: L. Segoufin
更快地确定固定高度树木的 MSO 特性以及一些后果
DOI: --
发表时间: 2012
期刊: Foundations of Software Technology and Theoretical Computer Science
影响因子: --
作者:
Jakub Gajarský;Petr Hliněný
通讯作者: Petr Hliněný
阶不变一阶逻辑的简短教程
DOI: --
发表时间: 2013
期刊: Computer Science Symposium in Russia
影响因子: --
作者:
Nicole Schweikardt
通讯作者: Nicole Schweikardt
一阶逻辑和一元二阶逻辑重合的地方
DOI: 10.1145/2946799
发表时间: 2012
期刊: 2012 27th Annual IEEE Symposium on Logic in Computer Science
影响因子: --
作者:
Michael Elberfeld;Martin Grohe;Till Tantau
通讯作者: Till Tantau