Expressiveness and succinctness of first-order logic on finite words
Expressiveness and succinctness of first-order logic on finite words
复制标题
有限词上的一阶逻辑的表达性和简洁性
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Philipp Weis
中科院分区：
文献类型：
--
作者：
N. Immerman;Philipp Weis
表现力以及最近的简洁性是有限模型理论和描述复杂性理论的两个核心关注点。简洁性特别有趣，因为它与平行时间和硬件量之间的复杂性理论权衡密切相关。我们在有限单词上使用两个变量的一阶逻辑的表现力和简洁性开发了新的界限，对此逻辑的满意度问题的复杂性呈现了相关结果，并探索了从该逻辑中获得的可满足性问题逻辑表达的观点。
我们给出了有限词的两个变量的一阶逻辑的表达能力的完整表征。我们进行调查的主要工具是古典Ehrenfeucht-Fraisse游戏。使用我们的新特征，我们证明了该逻辑的量词交替层次结构是严格的，解决了有关此逻辑表现力的主要剩余问题。
关于一阶逻辑的第二个重要问题，其中有两个变量有限词，这是关于此逻辑的可满足性问题的复杂性。以前只知道这个问题是NP-HARD和NEXP。我们证明了该逻辑的多项式化小型模型属性，导致NP算法，因此证明了该逻辑的满足性问题是NP完整的。
最后，我们调查了形式语言理论中最令人困惑的开放问题之一：广义的星际高度问题。截至今天，我们甚至都不知道是否存在普通语言大于1的常规语言。可以用受限的传递闭合操作员将此问题作为一阶逻辑的表达性问题，从而使我们允许我们使用有限模型理论的既定工具来攻击广义的星际高度问题。除了我们以纯粹逻辑形式形式化这个问题的贡献外，我们还开发了几种示例语言，作为至少2个普通的《星际高度》语言的候选人。虽然其中一些仍然是有前途的候选人，而对于另一些人来说，我们提出了新的结果，这些结果证明了这些结果他们只有广义的星级高度1。
Expressiveness, and more recently, succinctness, are two central concerns of finite model theory and descriptive complexity theory. Succinctness is particularly interesting because it is closely related to the complexity-theoretic trade-off between parallel time and the amount of hardware. We develop new bounds on the expressiveness and succinctness of first-order logic with two variables on finite words, present a related result about the complexity of the satisfiability problem for this logic, and explore a new approach to the generalized star-height problem from the perspective of logical expressiveness.
We give a complete characterization of the expressive power of first-order logic with two variables on finite words. Our main tool for this investigation is the classical Ehrenfeucht-Fraisse game. Using our new characterization, we prove that the quantifier alternation hierarchy for this logic is strict, settling the main remaining open question about the expressiveness of this logic.
A second important question about first-order logic with two variables on finite words is about the complexity of the satisfiability problem for this logic. Previously it was only known that this problem is NP-hard and in NEXP. We prove a polynomialsize small-model property for this logic, leading to an NP algorithm and thus proving that the satisfiability problem for this logic is NP-complete.
Finally, we investigate one of the most baffling open problems in formal language theory: the generalized star-height problem. As of today, we do not even know whether there exists a regular language that has generalized star-height larger than 1. This problem can be phrased as an expressiveness question for first-order logic with a restricted transitive closure operator, and thus allows us to use established tools from finite model theory to attack the generalized star-height problem. Besides our contribution to formalize this problem in a purely logical form, we have developed several example languages as candidates for languages of generalized star-height at least 2. While some of them still stand as promising candidates, for others we present new results that prove that they only have generalized star-height 1.