{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T16:24:18Z","timestamp":1790353458086,"version":"4.1.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,7,25]],"date-time":"2023-07-25T00:00:00Z","timestamp":1690243200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["446200270"],"award-info":[{"award-number":["446200270"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. However, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph problems that are commonly studied in parameterized algorithmics. By adding the atomic predicates conn<jats:sub><jats:italic>k<\/jats:italic><\/jats:sub>(<jats:italic>x,y,z_1,..., z<jats:sub>k<\/jats:sub><\/jats:italic>) that hold true in a graph if there exists a path between (the valuations of)<jats:italic>x<\/jats:italic>and<jats:italic>y<\/jats:italic>after (the valuations of)<jats:italic>z<jats:sub>1<\/jats:sub>,..., z<jats:sub>k<\/jats:sub><\/jats:italic>have been deleted, we obtain<jats:italic>separator logic<\/jats:italic>FO + conn. We show that separator logic can express many interesting problems, such as the feedback vertex set problem and elimination distance problems to first-order definable classes. Denote by FO + conn<jats:sub><jats:italic>k<\/jats:italic><\/jats:sub>the fragment of separator logic that is restricted to connectivity predicates with at most<jats:italic>k + 2<\/jats:italic>variables (that is, at most<jats:italic>k<\/jats:italic>deletions), we show that FO + conn<jats:sub><jats:italic>k + 1<\/jats:italic><\/jats:sub>is strictly more expressive than FO + conn<jats:sub><jats:italic>k<\/jats:italic><\/jats:sub>for all<jats:italic>k \u2265 0<\/jats:italic>. We then study the limitations of separator logic and prove that it cannot express planarity, and, in particular, not the disjoint paths problem. We obtain the stronger<jats:italic>disjoint-paths logic<\/jats:italic>FO + DP by adding the atomic predicates disjoint-paths<jats:sub><jats:italic>k<\/jats:italic><\/jats:sub>[(<jats:italic>x<jats:sub>1<\/jats:sub>, y<jats:sub>1<\/jats:sub><\/jats:italic>),..., (<jats:italic>x<jats:sub>k<\/jats:sub>, y<jats:sub>k<\/jats:sub><\/jats:italic>) that evaluate to true if there are internally vertex-disjoint paths between (the valuations of)<jats:italic>x<jats:sub>i<\/jats:sub><\/jats:italic>and<jats:italic>y<jats:sub>i<\/jats:sub><\/jats:italic>for all\u00a0<jats:italic>1 \u2264 i \u2264 k<\/jats:italic>. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Again, we show that the fragments FO + DP<jats:sub><jats:italic>k<\/jats:italic><\/jats:sub>that use predicates for at most<jats:italic>k<\/jats:italic>disjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitive-closure logics and monadic second-order logic.<\/jats:p>","DOI":"10.1145\/3595922","type":"journal-article","created":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T11:59:04Z","timestamp":1683547144000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["First-order Logic with Connectivity Operators"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1740-7478","authenticated-orcid":false,"given":"Nicole","family":"Schirrmacher","sequence":"first","affiliation":[{"name":"University of Bremen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6347-1198","authenticated-orcid":false,"given":"Sebastian","family":"Siebertz","sequence":"additional","affiliation":[{"name":"University of Bremen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4298-8876","authenticated-orcid":false,"given":"Alexandre","family":"Vigny","sequence":"additional","affiliation":[{"name":"University of Bremen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,7,25]]},"reference":[{"key":"e_1_3_1_2_2","volume-title":"Proceedings of the 38th International Symposium on Theoretical Aspects of Computer Science (STACS\u201921)","author":"Agrawal Akanksha","year":"2021","unstructured":"Akanksha Agrawal, Lawqueen Kanesh, Fahad Panolan, M. S. Ramanujan, and Saket Saurabh. 2021. An FPT algorithm for elimination distance to bounded degree graphs. In Proceedings of the 38th International Symposium on Theoretical Aspects of Computer Science (STACS\u201921). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik."},{"key":"e_1_3_1_3_2","first-page":"1447","volume-title":"Automorphism Groups, Isomorphism, Reconstruction","author":"Babai L\u00e1szl\u00f3","year":"1996","unstructured":"L\u00e1szl\u00f3 Babai. 1996. Automorphism Groups, Isomorphism, Reconstruction. MIT Press, Cambridge, MA, 1447\u20131540."},{"key":"e_1_3_1_4_2","unstructured":"Miko\u0142aj Boja\u0144czyk. 2021. Separator logic and star-free expressions for graphs. Retrieved from https:\/\/arXiv:2107.13953."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519935.3520037"},{"key":"e_1_3_1_6_2","volume-title":"Parameterized Complexity of Distances to Sparse Graph Classes","author":"Bulian Jannis","year":"2017","unstructured":"Jannis Bulian. 2017. Parameterized Complexity of Distances to Sparse Graph Classes. Technical Report. University of Cambridge, Computer Laboratory."},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-015-0045-3"},{"key":"e_1_3_1_8_2","first-page":"250","volume-title":"Proceedings of the International Conference on Computers and Games","author":"Buro Michael","year":"2000","unstructured":"Michael Buro. 2000. Simple Amazons endgames and their connection to Hamilton circuits in cubic subgrid graphs. In Proceedings of the International Conference on Computers and Games. Springer, 250\u2013261."},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/646255.684424"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90043-H"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s002249910009"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/2815661"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1137\/140988553"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-014-2897-6"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934552"},{"key":"e_1_3_1_17_2","volume-title":"Finite Model Theory","author":"Ebbinghaus Heinz-Dieter","year":"2005","unstructured":"Heinz-Dieter Ebbinghaus and J\u00f6rg Flum. 2005. Finite Model Theory. Springer Science & Business Media."},{"key":"e_1_3_1_18_2","first-page":"43","article-title":"Generalized first-order spectra and polynomial-time recognizable sets","volume":"7","author":"Fagin Ronald","year":"1974","unstructured":"Ronald Fagin. 1974. Generalized first-order spectra and polynomial-time recognizable sets. Complex. Comput. 7 (1974), 43\u201373.","journal-title":"Complex. Comput."},{"key":"e_1_3_1_19_2","first-page":"51:1\u201351:17","volume-title":"Proceedings of the 28th Annual European Symposium on Algorithms (ESA\u201920)","author":"Fomin Fedor V.","year":"2020","unstructured":"Fedor V. Fomin, Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. 2020. An algorithmic meta-theorem for graph modification to planarity and FOL. In Proceedings of the 28th Annual European Symposium on Algorithms (ESA\u201920). 51:1\u201351:17."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3517129"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3357713.3384318"},{"key":"e_1_3_1_22_2","first-page":"105","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Gaifman Haim","year":"1982","unstructured":"Haim Gaifman. 1982. On local and non-local properties. In Studies in Logic and the Foundations of Mathematics. Vol. 107. Elsevier, 105\u2013135."},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.07.005"},{"key":"e_1_3_1_24_2","first-page":"3684","volume-title":"Proceedings of the ACM-SIAM Symposium on Discrete Algorithms (SODA\u201923)","author":"Golovach Petr A.","year":"2023","unstructured":"Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. 2023. Model-checking for first-order logic with disjoint paths predicates in proper minor-closed graph classes. In Proceedings of the ACM-SIAM Symposium on Discrete Algorithms (SODA\u201923), Nikhil Bansal and Viswanath Nagarajan (Eds.). SIAM, 3684\u20133699."},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68804-8_3"},{"key":"e_1_3_1_26_2","first-page":"357","article-title":"Logic, graphs, and algorithms.","volume":"2","author":"Grohe Martin","year":"2008","unstructured":"Martin Grohe. 2008. Logic, graphs, and algorithms. Logic Autom. 2 (2008), 357\u2013422.","journal-title":"Logic Autom."},{"issue":"3","key":"e_1_3_1_27_2","first-page":"17","article-title":"Deciding first-order properties of nowhere dense graphs","volume":"64","author":"Grohe Martin","year":"2017","unstructured":"Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. 2017. Deciding first-order properties of nowhere dense graphs. J. ACM 64, 3 (2017), 17.","journal-title":"J. ACM"},{"key":"e_1_3_1_28_2","volume-title":"Proceedings of the International Symposium on Theoretical Aspects of Computer Science (STACS\u201920)","author":"Hols Eva-Maria C.","year":"2020","unstructured":"Eva-Maria C. Hols, Stefan Kratsch, and Astrid Pieterse. 2020. Elimination distances, blocking sets, and kernels for vertex cover. In Proceedings of the International Symposium on Theoretical Aspects of Computer Science (STACS\u201920)."},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3406325.3451068"},{"key":"e_1_3_1_30_2","first-page":"189","volume-title":"Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science","author":"Kreutzer Stephan","year":"2010","unstructured":"Stephan Kreutzer and Siamak Tazari. 2010. Lower bounds for the complexity of monadic second-order logic. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science. IEEE, 189\u2013198."},{"key":"e_1_3_1_31_2","volume-title":"Elements of Finite Model Theory","author":"Libkin Leonid","year":"2013","unstructured":"Leonid Libkin. 2013. Elements of Finite Model Theory. Springer Science & Business Media."},{"key":"e_1_3_1_32_2","first-page":"65:1\u201365:12","volume-title":"Proceedings of the 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic","author":"Lindermayr Alexander","year":"2020","unstructured":"Alexander Lindermayr, Sebastian Siebertz, and Alexandre Vigny. 2020. Elimination distance to bounded degree on planar graphs. In Proceedings of the 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic. 65:1\u201365:12."},{"key":"e_1_3_1_33_2","first-page":"102:1\u2013102:18","volume-title":"Proceedings of the 49th International Colloquium on Automata, Languages, and Programming (ICALP\u201922) (LIPIcs)","volume":"229","author":"Pilipczuk Michal","year":"2022","unstructured":"Michal Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Torunczyk, and Alexandre Vigny. 2022. Algorithms and data structures for first-order logic with connectivity under vertex failures. In Proceedings of the 49th International Colloquium on Automata, Languages, and Programming (ICALP\u201922) (LIPIcs), Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff (Eds.), Vol. 229. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 102:1\u2013102:18."},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2003.10.009"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2004.08.001"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(86)90030-4"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1006\/jctb.1995.1006"},{"key":"e_1_3_1_38_2","doi-asserted-by":"crossref","unstructured":"Nicole Schirrmacher Sebastian Siebertz Giannos Stamoulis Dimitrios M. Thilikos and Alexandre Vigny. 2023. Model checking disjoint-paths logic on topological-minor-free graph classes. Retrieved from https:\/\/arXiv:2302.07033.","DOI":"10.1145\/3661814.3662089"},{"key":"e_1_3_1_39_2","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201910)","author":"Schulz Stefan","year":"2010","unstructured":"Stefan Schulz. 2010. First-order logic with reachability predicates on infinite systems. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201910). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of Formal Languages, Volume 3: Beyond Words","author":"Thomas Wolfgang","year":"1997","unstructured":"Wolfgang Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Languages, Volume 3: Beyond Words, Grzegorz Rozenberg and Arto Salomaa (Eds.). Springer, 389\u2013455."},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01594196"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3595922","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3595922","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:35:56Z","timestamp":1750178156000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3595922"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,25]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3595922"],"URL":"https:\/\/doi.org\/10.1145\/3595922","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,25]]},"assertion":[{"value":"2022-04-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-24","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}