Skip to main contentSkip to search
Episciences
Open Access Journals
Sign in(new window)
Discrete Mathematics & Theoretical Computer Science logo
Discrete Mathematics & Theoretical Computer Science
Discrete Mathematics & Theoretical Computer Science logo
Discrete Mathematics & Theoretical Computer Science
Sign in(new window)
Articles & Issues
All articlesAll accepted articlesAll volumesLast volumeSectionsSpecial issuesAuthors
About
The journalIndexing
Boards
Publish
For authorsEthical charter
Submit
Discrete Mathematics & Theoretical Computer Science logo
Contact
|
Credits
eISSN 1365-8050
|
RSS
|
Atom
Episciences
Documentation
|
Acknowledgements
|
Publishing policy
Accessibility: non-compliant
|
Legal mentions
|
Privacy statement
|
Terms of use
  1. Home > Articles & Issues >
  2. Articles >
  3. Local Normal Forms f ...
Article

Local Normal Forms for First-Order Logic with Applications to Games and Automata

Thomas Schwentick (1), Klaus Barthelmann (1)
(1) Institut für Informatik / Institute of Computer Science [Mainz]
Download article
Open on HAL
Imported on
March 26, 2015
Published on
January 1, 1999
Last modified on
March 31, 2025
Volume 3
vol. 3:3, Special Issue STACS'98
DOI
10.46298/dmtcs.254
License
https://about.hal.science/hal-authorisation-v1
Indicators
725
Views
875
Downloads

Local Normal Forms for First-Order Logic with Applications to Games and Automata

Thomas Schwentick (1), Klaus Barthelmann (1)
(1) Institut für Informatik / Institute of Computer Science [Mainz]
Abstract
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.
Keywords
  • [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM]
  • First-order logic
  • existential monadic second-order logic
  • games
  • automata
  • locality
Cited by

Source: OpenCitations

  • Descriptive Complexity, Lower Bounds and Linear Time

    Lecture notes in computer science

    Authors : Thomas Schwentick ORCID

    Journal reference : Volume , 1999, pp. 9-28

    DOI : 10.1007/10703163_2

  • Parameterized Synthesis for Fragments of First-Order Logic Over Data Words

    Lecture notes in computer science

    Authors : Béatrice Bérard ORCID, Benedikt Bollig ORCID, Mathieu Lehaut ORCID, Nathalie Sznajder ORCID

    Journal reference : Volume , 2020, pp. 97-118

    DOI : 10.1007/978-3-030-45231-5_6

  • Locality and Winning Games

    Elements of Finite Model Theory

    Authors : Leonid Libkin ORCID

    Journal reference : Volume , 2004, pp. 45-65

    DOI : 10.1007/978-3-662-07003-1_4

  • An Automaton over Data Words That Captures EMSO Logic

    arXiv (Cornell University)

    Authors : Benedikt Bollig ORCID

    Journal reference : Volume , 2011, pp. 171-186

    DOI : 10.1007/978-3-642-23217-6_12

  • Subshifts as models for MSO logic

    arXiv (Cornell University)

    Authors : Emmanuel Jeandel ORCID, Guillaume Theyssier

    Journal reference : Volume 225, 2013, pp. 1-15

    DOI : 10.1016/j.ic.2013.01.003

  • Logics Capturing Local Properties

    Lecture notes in computer science

    Authors : Leonid Libkin ORCID

    Journal reference : Volume , 2000, pp. 217-229

    DOI : 10.1007/3-540-46541-3_18

  • Locality of Queries and Transformations

    Electronic Notes in Theoretical Computer Science

    Authors : Leonid Libkin ORCID

    Journal reference : Volume 143, 2005, pp. 115-127

    DOI : 10.1016/j.entcs.2005.04.041

  • Game-Based Notions of Locality Over Finite Models

    Lecture notes in computer science

    Authors : Marcelo Arenas ORCID, Pablo Barceló ORCID, Leonid Libkin ORCID

    Journal reference : Volume , 2004, pp. 175-189

    DOI : 10.1007/978-3-540-30124-0_16

  • Logics with counting, auxiliary relations, and lower bounds for invariant queries

    Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)

    Authors : L. Libkin ORCID

    Journal reference : Volume 41, 2003, pp. 316-325

    DOI : 10.1109/lics.1999.782626

  • Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems

    Lecture notes in computer science

    Authors : Roderick Bloem ORCID, Nicolas Braud-Santoni ORCID, Swen Jacobs ORCID

    Journal reference : Volume , 2016, pp. 157-176

    DOI : 10.1007/978-3-319-41528-4_9

  • On Locality and Uniform Reduction

    20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)

    Authors : H. Niemisto

    Journal reference : Volume 99, 2006, pp. 41-50

    DOI : 10.1109/lics.2005.32

  • A hierarchy of local decision

    Authors : Laurent Feuilloley ORCID, Pierre Fraigniaud, Juho Hirvonen

    Journal reference : Volume 856, 2020, pp. 51-67

    DOI : 10.1016/j.tcs.2020.12.017
Preview
Loading PDF preview...