Local Normal Forms for First-Order Logic with Applications to Games and Automata
Local Normal Forms for First-Order Logic with Applications to Games and Automata
复制标题
DOI：
10.46298/dmtcs.254
复制
发表时间：
1998-02
期刊：
影响因子：
--
通讯作者：
T. Schwentick;Klaus Barthelmann
中科院分区：
文献类型：
--
作者：
T. Schwentick;Klaus Barthelmann
在Gaifman [Gai 82]的工作的基础上，证明了每个一阶公式在逻辑上等价于一个形式为x_1，...，x_l，\forall y，φ其中φ是围绕y的r-局部的，即φ中的量化被限制为离y的距离最多为r的宇宙的元素。\par从这个和相关的正规形式，一阶和存在一元二阶逻辑的Escherichfeucht博弈的变体被开发出来，限制了两个玩家之一的可能策略。这使得证明复制者（另一个玩家）的获胜策略的存在变得更容易，从而可以简化不可表达性证明。\par作为另一个应用，自动机模型被定义为，在任意类的关系结构上，分别具有一阶逻辑和存在一元二阶逻辑的表达能力。
Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata models are defined that have, on arbitrary classes of relational structures, exactly the expressive power of first-order logic and existential monadic second-order logic, respectively.