Succinctness of Order-Invariant Logics on Depth-Bounded Structures

DOI10.1145/3152770zbMATH Open1407.03002arXiv1603.09055OpenAlexW2964232764WikidataQ130860772 ScholiaQ130860772MaRDI QIDQ4608722FDOQ4608722

Authors: Kord Eickmeyer, Michael Elberfeld, Frederik Harwath 

Publication date: 22 March 2018

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on structures of bounded tree-depth. Order- invariance is undecidable in general and, thus, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on structures of bounded tree-depth, order-invariant FO has the same expressive power as FO. Our proof technique allows for a fine-grained analysis of the succinctness of this translation. We show that for every order-invariant FO sentence there exists an FO sentence whose size is elementary in the size of the original sentence, and whose number of quantifier alternations is linear in the tree-depth. We obtain similar results for MSO. It is known that the expressive power of MSO and FO coincide on structures of bounded tree-depth. We provide a translation from MSO to FO and we show that this translation is essentially optimal regarding the formula size. As a further result, we show that order-invariant MSO has the same expressive power as FO with modulo-counting quantifiers on bounded tree-depth structures.

Full work available at URL: https://arxiv.org/abs/1603.09055

Recommendations

• Expressivity and succinctness of order-invariant logics on depth-bounded structures
• The succinctness of first-order logic on linear orders
• Semantics and proof-theory of depth bounded Boolean logics
• Successor-invariant first-order logic on finite structures
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Bounds for the quantifier depth in finite-variable logics: alternation hierarchy
• Decidability of order-based modal logics
• Order-Invariant First-Order Logic over Hollow Trees

zbMATH Keywords

first-order logicmonadic second-order logictree-depthexpressivitysuccinctnessorder-invariance

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25)

Cited In (10)

• Order-invariant MSO is stronger than counting MSO in the finite
• Towards a characterization of order-invariant queries over tame graphs
• Comparing the succinctness of monadic query languages over finite trees
• Computer Science Logic
• Order invariance on decomposable structures
• The succinctness of first-order logic on linear orders
• Where first-order and monadic second-order logic coincide
• Where first-order and monadic second-order logic coincide
• Expressivity and succinctness of order-invariant logics on depth-bounded structures
• Successor-invariant first-order logic on finite structures

This page was built for publication: Succinctness of Order-Invariant Logics on Depth-Bounded Structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4608722)