{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:12Z","timestamp":1750309332280,"version":"3.41.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T00:00:00Z","timestamp":1712880000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council","award":["820148"],"award-info":[{"award-number":["820148"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>\n            We extend Choiceless Polynomial Time (CPT), the currently only remaining promising candidate in the quest for a logic capturing\n            <jats:sc>Ptime<\/jats:sc>\n            , so that this extended logic has the following property: for every class of structures for which isomorphism is definable, the logic automatically captures\n            <jats:sc>Ptime<\/jats:sc>\n            .\n          <\/jats:p>\n          <jats:p>For the construction of this logic, we extend CPT by a witnessed symmetric choice operator. This operator allows for choices from definable orbits. But, to ensure polynomial-time evaluation, automorphisms have to be provided to certify that the choice set is indeed an orbit.<\/jats:p>\n          <jats:p>\n            We argue that, in this logic, definable isomorphism implies definable canonization. Thereby, our construction removes the non-trivial step of extending isomorphism definability results to canonization. This step was a part of proofs that show that CPT or other logics capture\n            <jats:sc>Ptime<\/jats:sc>\n            on a particular class of structures. The step typically required substantial extra effort.\n          <\/jats:p>","DOI":"10.1145\/3648104","type":"journal-article","created":{"date-parts":[[2024,2,13]],"date-time":"2024-02-13T13:51:15Z","timestamp":1707832275000},"page":"1-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Choiceless Polynomial Time with Witnessed Symmetric Choice"],"prefix":"10.1145","volume":"71","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5437-8074","authenticated-orcid":false,"given":"Moritz","family":"Lichter","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3585-8213","authenticated-orcid":false,"given":"Pascal","family":"Schweitzer","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,12]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_2_2","DOI":"10.1016\/S0168-0072(99)00005-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_3_2","DOI":"10.2178\/jsl\/1190150152"},{"doi-asserted-by":"publisher","key":"e_1_3_2_4_2","DOI":"10.1007\/BF01305232"},{"doi-asserted-by":"publisher","key":"e_1_3_2_5_2","DOI":"10.1016\/0022-0000(82)90012-5"},{"key":"e_1_3_2_6_2","volume-title":"Lectures on Coherent Configurations","author":"Chen Gang","year":"2019","unstructured":"Gang Chen and Ilia Ponomarenko. 2019. Lectures on Coherent Configurations. Central China Normal University Press, Wuhan. A draft is available at http:\/\/www.pdmi.ras.ru\/\u223cinp\/"},{"doi-asserted-by":"publisher","key":"e_1_3_2_7_2","DOI":"10.1109\/LICS.2009.24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_8_2","DOI":"10.1093\/logcom\/exac058"},{"doi-asserted-by":"publisher","unstructured":"Anuj Dawar and David Richerby. 2003. A fixed-point logic with symmetric choice. In Computer Science Logic. Lecture Notes in Computer Science Vol. 2803. Springer 169\u2013182. DOI:10.1007\/978-3-540-45220-1_16","key":"e_1_3_2_9_2","DOI":"10.1007\/978-3-540-45220-1_16"},{"doi-asserted-by":"publisher","key":"e_1_3_2_10_2","DOI":"10.1093\/logcom\/13.4.503"},{"doi-asserted-by":"publisher","key":"e_1_3_2_11_2","DOI":"10.1016\/j.apal.2007.11.011"},{"key":"e_1_3_2_12_2","first-page":"25","volume-title":"Model-Theoretic Logics","author":"Ebbinghaus Heinz-Dieter","year":"1985","unstructured":"Heinz-Dieter Ebbinghaus. 1985. Extended logics: The general framework. In Model-Theoretic Logics. Association for Symbolic Logic, 25\u201376."},{"unstructured":"Ronald Fagin. 1974. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation. Proceedings Vol. VII. SIAM 43\u201373.","key":"e_1_3_2_13_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_14_2","DOI":"10.1006\/inco.1998.2712"},{"doi-asserted-by":"publisher","unstructured":"Erich Gr\u00e4del and Martin Grohe. 2015. Is polynomial time choiceless? In Fields of Logic and Computation II. Lecture Notes in Computer Science Vol. 9300. Springer 193\u2013209. DOI:10.1007\/978-3-319-23534-9_11","key":"e_1_3_2_15_2","DOI":"10.1007\/978-3-319-23534-9_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_16_2","DOI":"10.1109\/LICS.2015.68"},{"doi-asserted-by":"publisher","key":"e_1_3_2_17_2","DOI":"10.1109\/LICS.2008.11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_18_2","DOI":"10.1017\/9781139028868"},{"doi-asserted-by":"publisher","key":"e_1_3_2_19_2","DOI":"10.1109\/LICS.2019.8785682"},{"doi-asserted-by":"publisher","key":"e_1_3_2_20_2","DOI":"10.1137\/1.9781611976465.154"},{"key":"e_1_3_2_21_2","first-page":"1","volume-title":"Current Trends in Theoretical Computer Science","author":"Gurevich Yuri","year":"1988","unstructured":"Yuri Gurevich. 1988. Logic and the challenge of computer science. In Current Trends in Theoretical Computer Science. Computer Science Press, 1\u201357."},{"key":"e_1_3_2_22_2","article-title":"From invariants to canonization","volume":"63","author":"Gurevich Yuri","year":"1997","unstructured":"Yuri Gurevich. 1997. From invariants to canonization. Bull. EATCS 63 (1997), 1\u20135.","journal-title":"Bull. EATCS"},{"doi-asserted-by":"publisher","key":"e_1_3_2_23_2","DOI":"10.1137\/0216051"},{"doi-asserted-by":"publisher","unstructured":"Sandra Kiefer Pascal Schweitzer and Erkal Selman. 2015. Graphs identified by logics with counting. In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science Vol. 9234. Springer 319\u2013330. DOI:10.1007\/978-3-662-48057-1_25","key":"e_1_3_2_24_2","DOI":"10.1007\/978-3-662-48057-1_25"},{"doi-asserted-by":"publisher","key":"e_1_3_2_25_2","DOI":"10.1145\/3572918"},{"doi-asserted-by":"publisher","unstructured":"Moritz Lichter. 2023. Witnessed symmetric choice and interpretations in fixed-point logic with counting. In Proceedings of the 50th International Colloquium on Automata Languages and Programming (ICALP\u201923). LIPIcs Vol. 261. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik Article 133 20 pages. DOI:10.4230\/LIPICS.ICALP.2023.133","key":"e_1_3_2_26_2","DOI":"10.4230\/LIPICS.ICALP.2023.133"},{"doi-asserted-by":"publisher","unstructured":"Moritz Lichter and Pascal Schweitzer. 2021. Canonization for bounded and dihedral color classes in choiceless polynomial time. In Proceedings of the 29th EACSL Annual Conference on Computer Science Logic (CSL\u201921). LIPIcs Vol. 183. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik Article 31 18 pages. DOI:10.4230\/LIPIcs.CSL.2021.31","key":"e_1_3_2_27_2","DOI":"10.4230\/LIPIcs.CSL.2021.31"},{"doi-asserted-by":"publisher","key":"e_1_3_2_28_2","DOI":"10.1145\/3531130.3533348"},{"doi-asserted-by":"publisher","key":"e_1_3_2_29_2","DOI":"10.1016\/0020-0190(79)90004-8"},{"doi-asserted-by":"publisher","unstructured":"Benedikt Pago. 2021. Choiceless computation and symmetry: Limitations of definability. In Proceedings of the 29th EACSL Annual Conference on Computer Science Logic (CSL\u201921). LIPIcs Vol. 183. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik 33:1\u201333:21. DOI:10.4230\/LIPIcs.CSL.2021.33","key":"e_1_3_2_30_2","DOI":"10.4230\/LIPIcs.CSL.2021.33"},{"key":"e_1_3_2_31_2","article-title":"Choiceless polynomial time, symmetric circuits and Cai-F\u00fcrer-Immerman graphs","volume":"2107","author":"Pago Benedikt","year":"2021","unstructured":"Benedikt Pago. 2021. Choiceless polynomial time, symmetric circuits and Cai-F\u00fcrer-Immerman graphs. CoRR abs\/2107.03778 (2021). https:\/\/arxiv.org\/abs\/2107.03778","journal-title":"CoRR"},{"key":"e_1_3_2_32_2","volume-title":"Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time","author":"Pakusa Wied","year":"2015","unstructured":"Wied Pakusa. 2015. Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time. Ph. D. Dissertation. RWTH Aachen University."},{"doi-asserted-by":"publisher","unstructured":"Wied Pakusa Svenja Schalth\u00f6fer and Erkal Selman. 2016. Definability of Cai-F\u00fcrer-Immerman problems in choiceless polynomial time. In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL\u201916). LIPIcs Vol. 62. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik Article 19 17 pages. DOI:10.4230\/LIPIcs.CSL.2016.19","key":"e_1_3_2_33_2","DOI":"10.4230\/LIPIcs.CSL.2016.19"},{"doi-asserted-by":"publisher","unstructured":"Benjamin Rossman. 2010. Choiceless computation and symmetry. In Fields of Logic and Computation. Lecture Notes in Computer Science Vol. 6300. Springer 565\u2013580. DOI:10.1007\/978-3-642-15025-8_28","key":"e_1_3_2_34_2","DOI":"10.1007\/978-3-642-15025-8_28"},{"doi-asserted-by":"publisher","key":"e_1_3_2_35_2","DOI":"10.1145\/3313276.3316338"},{"doi-asserted-by":"publisher","unstructured":"Faried Abu Zaid Erich Gr\u00e4del Martin Grohe and Wied Pakusa. 2014. Choiceless polynomial time on structures with small Abelian colour classes. In Mathematical Foundations of Computer Science 2014. Lecture Notes in Computer Science Vol. 8634. Springer 50\u201362. DOI:10.1007\/978-3-662-44522-8_5","key":"e_1_3_2_36_2","DOI":"10.1007\/978-3-662-44522-8_5"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3648104","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3648104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:12Z","timestamp":1750291452000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3648104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,12]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3648104"],"URL":"https:\/\/doi.org\/10.1145\/3648104","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2024,4,12]]},"assertion":[{"value":"2023-01-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-23","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-04-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}