{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:21:30Z","timestamp":1770247290631,"version":"3.49.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    The\n                    <jats:italic toggle=\"yes\">Entscheidungsproblem<\/jats:italic>\n                    , or the classical decision problem, asks whether a given formula of first-order logic is satisfiable. In this work, we consider an extension of this problem to regular first-order\n                    <jats:italic toggle=\"yes\">theories<\/jats:italic>\n                    , i.e., (infinite) regular sets of formulae. Building on the elegant classification of syntactic classes as decidable or undecidable for the classical decision problem, we show that some classes (specifically, the EPR and Gurevich classes), which are decidable in the classical setting, become undecidable for regular theories. On the other hand, for each of these classes, we identify a subclass that remains decidable in our setting, leaving a complete classification as a challenge for future work. Finally, we observe that our problem generalises prior work on automata-theoretic verification of uninterpreted programs and propose a semantic class of existential formulae for which the problem is decidable.\n                  <\/jats:p>","DOI":"10.1145\/3704870","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"986-1012","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The Decision Problem for Regular First Order Theories"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3186-8307","authenticated-orcid":false,"given":"David","family":"Mestel","sequence":"additional","affiliation":[{"name":"Maastricht University, Maastricht, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7977-0080","authenticated-orcid":false,"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","volume-title":"Solvable Cases of the Decision Problem","author":"Ackermann Wilhelm","year":"1954","unstructured":"Wilhelm Ackermann . 1954. Solvable Cases of the Decision Problem. North-Holland Pub. Co., Amsterdam."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-AidedDesign. 1-8. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926454"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57259-3_20"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1133-y"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31"},{"key":"e_1_3_2_9_1","first-page":"116","article-title":"Invertibility Conditions for Floating-Point Formulas","author":"Brain Martin","year":"2019","unstructured":"Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. 2019a. Invertibility Conditions for Floating-Point Formulas. In Proceedings of the International Conference on Computer-Aided Verification. 116\u2014-136.","journal-title":"Proceedings of the International Conference on Computer-Aided Verification"},{"key":"e_1_3_2_10_1","first-page":"79","article-title":"Building Better Bit-Blasting for Floating-Point Problems","author":"Brain Martin","year":"2019","unstructured":"Martin Brain, Florian Schanda, and Youcheng Sun. 2019b. Building Better Bit-Blasting for Floating-Point Problems. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 79\u2014-98.","journal-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"e_1_3_2_11_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (OSDI\u201908). USENIX Association, USA, 209-224."},{"key":"e_1_3_2_12_1","unstructured":"Benjamin Caulfield Markus N. Rabe Sanjit A. Seshia and Stavros Tripakis. 2016. What\u2019s Decidable about Syntax-Guided Synthesis? arXiv: 1510.08393 [cs.LO]"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269326"},{"key":"e_1_3_2_14_1","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2008. Tree automata techniques and applications."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90015-A"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01696781"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"key":"e_1_3_2_19_1","first-page":"306","article-title":"Two-variable logic with counting is decidable","author":"Gr\u00e4del E.","year":"1997","unstructured":"E. Gr\u00e4del, M. Otto, and E. Rosen. 1997b. Two-variable logic with counting is decidable. In Proceedings of the IEEE Symposium on Logic in Computer Science. 306-317.","journal-title":"In Proceedings of the IEEE Symposium on Logic in Computer Science."},{"issue":"1999","key":"e_1_3_2_20_1","first-page":"313","article-title":"Undecidability results on two-variable logics","volume":"38","author":"Gr\u00e4del E.","year":"1999","unstructured":"E. Gr\u00e4del, M. Otto, and E. Rosen. 1999. Undecidability results on two-variable logics. Archive of Math. Logic 38 (1999), 313-353.","journal-title":"Archive of Math. Logic"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/2272244"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02306690"},{"key":"e_1_3_2_23_1","first-page":"680","article-title":"Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors","author":"Hadarean Liana","year":"2014","unstructured":"Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark Barrett, and Cesare Tinelli. 2014. Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. In Proceedings of the International Conference on Computer-Aided Verification. 680-695.","journal-title":"and Cesare Tinelli"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_16"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_28_1","first-page":"335","volume-title":"Computer Aided Verification","author":"Qinheping Hu","year":"2019","unstructured":"Qinheping Hu, Jason Breck, John Cyphert, Loris D\u2019Antoni, and Thomas Reps. 2019. Proving Unrealizability for Syntax- Guided Synthesis. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 335-352."},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90011-3"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.48.3.365"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563348"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498671"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586032"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_32"},{"key":"e_1_3_2_38_1","doi-asserted-by":"crossref","unstructured":"Tianyi Liang Nestan Tsiskaridze Andrew Reynolds Cesare Tinelli and Clark Barrett. 2015. A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. In Frontiers of Combining Systems Carsten Lutz and Silvio Ranise (Eds.). Springer International Publishing Cham 135-150.","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.31"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290359"},{"key":"e_1_3_2_41_1","first-page":"158","volume-title":"Tools and Algorithms for the Construction and Analysis ofSystems","author":"P. Umang Mathur","year":"2020","unstructured":"Umang Mathur, P. Madhusudan, and Mahesh Viswanathan. 2020. What\u2019s Decidable About Program Verification Modulo Axioms?. In Tools and Algorithms for the Construction and Analysis ofSystems, Armin Biere and David Parker (Eds.). Springer International Publishing, Cham, 158-177."},{"key":"e_1_3_2_42_1","unstructured":"Umang Mathur David Mestel and Mahesh Viswanathan. 2024. The Decision Problem for Regular First-Order Theories. arXiv:2410.17185 [cs.LO] https:\/\/doi.org\/https:\/\/arxiv.org\/abs\/2410.17185"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371103"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"issue":"1969","key":"e_1_3_2_47_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin Michael O.","year":"1969","unstructured":"Michael O. Rabin . 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1-35.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_2_49_1","first-page":"16","volume-title":"Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201920)","author":"Rigger Manuel","year":"2020","unstructured":"Manuel Rigger and Zhendong Su. 2020. Testing database engines via pivoted query synthesis. In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201920). USENIX Association, USA, Article 38, 16 pages."},{"key":"e_1_3_2_50_1","first-page":"480","volume-title":"Preservation theorems in finite model theoryInternational Workshop LCC\u201994","author":"Rosen Eric","year":"1995","unstructured":"Eric Rosen and Scott Weinstein. 1995. Preservation theorems in finite model theory. In Logic and Computational Complexity:International Workshop LCC\u201994 Indianapolis, IN, USA, October 13-16, 1994 Selected Papers. Springer, 480-502."},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-023-09682-2"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359570"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480915"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640389"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704870","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704870","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:00Z","timestamp":1770200280000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704870"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704870"],"URL":"https:\/\/doi.org\/10.1145\/3704870","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}