{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:34Z","timestamp":1750221274462,"version":"3.41.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,10,31]],"date-time":"2017-10-31T00:00:00Z","timestamp":1509408000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3152770","type":"journal-article","created":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T13:26:47Z","timestamp":1512998807000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Succinctness of Order-Invariant Logics on Depth-Bounded Structures"],"prefix":"10.1145","volume":"18","author":[{"given":"Kord","family":"Eickmeyer","sequence":"first","affiliation":[{"name":"TU Darmstadt, Darmstadt, Germany"}]},{"given":"Michael","family":"Elberfeld","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"given":"Frederik","family":"Harwath","sequence":"additional","affiliation":[{"name":"Goethe-Universit\u00e4t Frankfurt am Main, Germany"}]}],"member":"320","published-online":{"date-parts":[[2017,12,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1231082307"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934508"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33293-7_21"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90012-5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90387-H"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00083-6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_22"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.37"},{"volume-title":"Parameterized Complexity Theory","author":"Flum Jrg","key":"e_1_2_1_9_1"},{"volume-title":"Proceedings of FSTTCS","year":"2012","author":"Gajarsk\u00fd Jakub","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","first-page":"1","volume-title":"The succinctness of first-order logic on linear orders. Logic. Methods Comput. Sci. 1(1:6)","author":"Grohe Martin","year":"2005"},{"volume-title":"An Introduction to Semigroup Theory","author":"Howie John M.","key":"e_1_2_1_12_1"},{"volume-title":"Elements of Finite Model Theory","author":"Libkin Leonid","key":"e_1_2_1_13_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07003-1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.11.002"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27875-4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38536-0_10"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.16"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152770","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3152770","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:09Z","timestamp":1750212669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152770"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,31]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3152770"],"URL":"https:\/\/doi.org\/10.1145\/3152770","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2017,10,31]]},"assertion":[{"value":"2016-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}