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

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.
Type de document :
Article dans une revue
Discrete Mathematics and Theoretical Computer Science, DMTCS, 1999, 3 (3), pp.109-124
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00958930
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : jeudi 13 mars 2014 - 16:47:52
Dernière modification le : mercredi 29 novembre 2017 - 10:26:20
Document(s) archivé(s) le : vendredi 13 juin 2014 - 12:00:26

Fichier

dm030303.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00958930, version 1

Collections

Citation

Thomas Schwentick, Klaus Barthelmann. Local Normal Forms for First-Order Logic with Applications to Games and Automata. Discrete Mathematics and Theoretical Computer Science, DMTCS, 1999, 3 (3), pp.109-124. 〈hal-00958930〉

Partager

Métriques

Consultations de la notice

93

Téléchargements de fichiers

227