• DocumentCode
    3092771
  • Title

    Where First-Order and Monadic Second-Order Logic Coincide

  • Author

    Elberfeld, Michael ; Grohe, Martin ; Tantau, Till

  • Author_Institution
    Inst. fur Theor. Inf., Univ. zu Lubeck, Lubeck, Germany
  • fYear
    2012
  • fDate
    25-28 June 2012
  • Firstpage
    265
  • Lastpage
    274
  • Abstract
    We study on which classes of graphs first-order logic (FO) and monadic second-order logic (MSO) have the same expressive power. We show that for each class of graphs that is closed under taking subgraphs, FO and MSO have the same expressive power on the class if, and only if, it has bounded tree depth. Tree depth is a graph invariant that measures the similarity of a graph to a star in a similar way that tree width measures the similarity of a graph to a tree. For classes just closed under taking induced subgraphs, we show an analogous result for guarded second-order logic (GSO), the variant of MSO that not only allows quantification over vertex sets but also over edge sets. A key tool in our proof is a Feferman-Vaught-type theorem that is constructive and still works for unbounded partitions.
  • Keywords
    formal logic; trees (mathematics); FO; Feferman-Vaught-type theorem; GSO; MSO; bounded tree depth; first-order logic; graph invariant; guarded second-order logic; monadic second-order logic; Automata; Indexes; Semantics; Silicon; Syntactics; Vegetation; Vocabulary; first-order logic; graph classes; guarded second-order logic; monadic second-order logic; tree depth;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on
  • Conference_Location
    Dubrovnik
  • ISSN
    1043-6871
  • Print_ISBN
    978-1-4673-2263-8
  • Type

    conf

  • DOI
    10.1109/LICS.2012.37
  • Filename
    6280445