{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:17:14Z","timestamp":1770283034734,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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":[[2022,10,31]]},"abstract":"<jats:p>Axioms and inference rules form the foundation of deductive systems  \nand are crucial in the study of reasoning with logics over structures.  \nHistorically, axiomatizations have been discovered manually with much  \nexpertise and effort. In this paper we show the feasibility of using synthesis  \ntechniques to discover axiomatizations for different classes of  \nstructures, and in some contexts, automatically prove their  \ncompleteness. For evaluation, we apply our technique to find axioms  \nfor (1) classes of frames in modal logic characterized in first-order  \nlogic and (2) the class of language models with regular operations.<\/jats:p>","DOI":"10.1145\/3563348","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1697-1725","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Synthesizing axiomatizations using logic learning"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6710-9516","authenticated-orcid":false,"given":"Paul","family":"Krogmeier","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5475-5765","authenticated-orcid":false,"given":"Zhengyao","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_4_1","volume-title":"Handbook of Modal Logic","author":"Blackburn Patrick","unstructured":"Patrick Blackburn , Johan F. A. K. van Benthem , and Frank Wolter . 2006. Handbook of Modal Logic , Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc ., USA. isbn:0444516905 Patrick Blackburn, Johan F. A. K. van Benthem, and Frank Wolter. 2006. Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., USA. isbn:0444516905"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-2464(07)80002-4"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.006"},{"key":"e_1_2_1_7_1","volume-title":"Logics of Programs","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke and E. Allen Emerson . 1982. Design and synthesis of synchronization skeletons using branching time temporal logic . In Logics of Programs , Dexter Kozen (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 52\u201371. isbn:978-3-540-39047-3 Edmund M. Clarke and E. Allen Emerson. 1982. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs, Dexter Kozen (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 52\u201371. isbn:978-3-540-39047-3"},{"key":"e_1_2_1_8_1","volume-title":"Regular algebra and finite machines","author":"Conway John H.","unstructured":"John H. Conway . 1971. Regular algebra and finite machines . Chapman and Hall , London, UK . isbn:9780412106200 John H. Conway. 1971. Regular algebra and finite machines. Chapman and Hall, London, UK. isbn:9780412106200"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_4"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2022.24215"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SISY.2015.7325367"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SACI.2012.6250041"},{"key":"e_1_2_1_14_1","volume-title":"Partial Orders and the Axiomatic Theory of Shuffle (Pomsets). Ph. D. Dissertation","author":"Gischer Jay Loren","unstructured":"Jay Loren Gischer . 1985. Partial Orders and the Axiomatic Theory of Shuffle (Pomsets). Ph. D. Dissertation . Stanford University . Stanford, CA, USA. AAI8506191 Jay Loren Gischer. 1985. Partial Orders and the Axiomatic Theory of Shuffle (Pomsets). Ph. D. Dissertation. Stanford University. Stanford, CA, USA. AAI8506191"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_2_1_16_1","volume-title":"Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201921)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance , Marijn Heule , Ruben Martins , and Bryan Parno . 2021 . Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201921) . USENIX Association, Boston, MA, USA. 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201921). USENIX Association, Boston, MA, USA. 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"e_1_2_1_19_1","volume-title":"A Shorter Model Theory","author":"Hodges Wilfrid","unstructured":"Wilfrid Hodges . 1997. A Shorter Model Theory . Cambridge University Press , USA. isbn:0521587131 Wilfrid Hodges. 1997. A Shorter Model Theory. Cambridge University Press, USA. isbn:0521587131"},{"key":"e_1_2_1_20_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"2006","unstructured":"John E. Hopcroft , Rajeev Motwani , and Jeffrey D . Ullman . 2006 . Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co. , Inc., USA. isbn:0321455363 John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA. isbn:0321455363"},{"key":"e_1_2_1_21_1","volume-title":"Automated Theory Exploration for Interactive Theorem Proving","author":"Johansson Moa","unstructured":"Moa Johansson . 2017. Automated Theory Exploration for Interactive Theorem Proving :. In Interactive Theorem Proving, Mauricio Ayala-Rinc\u00f3n and C\u00e9sar A. Mu\u00f1oz (Eds.). Springer International Publishing , Cham . 1\u201311. isbn:978-3-319-66107-0 Moa Johansson. 2017. Automated Theory Exploration for Interactive Theorem Proving:. In Interactive Theorem Proving, Mauricio Ayala-Rinc\u00f3n and C\u00e9sar A. Mu\u00f1oz (Eds.). Springer International Publishing, Cham. 1\u201311. isbn:978-3-319-66107-0"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08434-3_9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_2_1_24_1","volume-title":"Representation of Events in Nerve Nets and Finite Automata","author":"Kleene S. C.","unstructured":"S. C. Kleene . 1956. Representation of Events in Nerve Nets and Finite Automata . Princeton University Press, Princeton, NJ , USA. 3\u201342. S. C. Kleene. 1956. Representation of Events in Nerve Nets and Finite Automata. Princeton University Press, Princeton, NJ, USA. 3\u201342."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_2_1_26_1","volume-title":"First-Order Theorem Proving and Vampire","author":"Kov\u00e1cs Laura","unstructured":"Laura Kov\u00e1cs and Andrei Voronkov . 2013. First-Order Theorem Proving and Vampire . In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 1\u201335. isbn:978-3-642-39799-8 Laura Kov\u00e1cs and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201335. isbn:978-3-642-39799-8"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_1_28_1","unstructured":"Paul Krogmeier Zhengyao Lin Adithya Murali and P. Madhusudan. 2022. LAS Framework Implementation. https:\/\/github.com\/zhengyao-lin\/fol-synthesis\/tree\/oopsla22 \t\t\t\t  Paul Krogmeier Zhengyao Lin Adithya Murali and P. Madhusudan. 2022. LAS Framework Implementation. https:\/\/github.com\/zhengyao-lin\/fol-synthesis\/tree\/oopsla22"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7072506"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498671"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245293"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0364-0213(81)80025-0"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_10"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_1_36_1","volume-title":"\u0141 ukasiewicz and A. Tarski","author":"J.","year":"1930","unstructured":"J. \u0141 ukasiewicz and A. Tarski . 1930 . Untersuchungen \u00fcber den Aussagenkalk\u00fcl. 23, Comptes Rendus des S\u00e9ances de la Soci\u00e9l\u00e9 des Scierices et des Lettres des Varsovie Classe III, Warsaw, Poland . J. \u0141 ukasiewicz and A. Tarski. 1930. Untersuchungen \u00fcber den Aussagenkalk\u00fcl. 23, Comptes Rendus des S\u00e9ances de la Soci\u00e9l\u00e9 des Scierices et des Lettres des Varsovie Classe III, Warsaw, Poland."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10489-017-0954-8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01233914"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-004-1902-0"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-003-1832-2"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1996.12004833"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020542009983"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881862"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700006912"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S144678870000570X"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_2_1_49_1","first-page":"120","article-title":"On defining relations for the algebra of regular events","volume":"16","author":"Redko V.N.","year":"1964","unstructured":"V.N. Redko . 1964 . On defining relations for the algebra of regular events . Ukrainian Mathematical Journal , 16 , 2 (1964), 120 \u2013 126 . In Russian V.N. Redko. 1964. On defining relations for the algebra of regular events. Ukrainian Mathematical Journal, 16, 2 (1964), 120\u2013126. In Russian","journal-title":"Ukrainian Mathematical Journal"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"e_1_2_1_51_1","volume-title":"Witness Theory: Notes on \u03bb -calculus and Logic","author":"Rezus Adrian","year":"2020","unstructured":"Adrian Rezus . 2020 . Witness Theory: Notes on \u03bb -calculus and Logic . College Publications, London , UK. isbn:ISBN 978-1-84890-326-5 Adrian Rezus. 2020. Witness Theory: Notes on \u03bb -calculus and Logic. College Publications, London, UK. isbn:ISBN 978-1-84890-326-5"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"e_1_2_1_53_1","volume-title":"Theory Exploration Powered by Deductive Synthesis","author":"Singher Eytan","unstructured":"Eytan Singher and Shachar Itzhaky . 2021. Theory Exploration Powered by Deductive Synthesis . In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing , Cham . 125\u2013148. isbn:978-3-030-81688-9 https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-81688-9_6 Eytan Singher and Shachar Itzhaky. 2021. Theory Exploration Powered by Deductive Synthesis. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham. 125\u2013148. isbn:978-3-030-81688-9 https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-81688-9_6"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106279"},{"key":"e_1_2_1_55_1","unstructured":"Peter Smith. 2010. The Galois Connection between Syntax and Semantics. https:\/\/www.logicmatters.net\/resources\/pdfs\/Galois.pdf \t\t\t\t  Peter Smith. 2010. The Galois Connection between Syntax and Semantics. https:\/\/www.logicmatters.net\/resources\/pdfs\/Galois.pdf"},{"key":"e_1_2_1_56_1","volume-title":"Program Synthesis By Sketching. Ph. D. Dissertation. EECS Department","author":"Lezama Armando Solar","unstructured":"Armando Solar Lezama . 2008. Program Synthesis By Sketching. Ph. D. Dissertation. EECS Department , University of California , Berkeley. https:\/\/dl.acm.org\/doi\/10.5555\/1714168 Armando Solar Lezama. 2008. Program Synthesis By Sketching. Ph. D. Dissertation. EECS Department, University of California, Berkeley. https:\/\/dl.acm.org\/doi\/10.5555\/1714168"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-30-1-253-256"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.72.1009"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-6259-0_4"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158144"},{"key":"e_1_2_1_61_1","volume-title":"Toward an artificial intelligence physicist for unsupervised learning.. Physical review. E, 100 3-1","author":"Wu Tailin","year":"2019","unstructured":"Tailin Wu and Max Tegmark . 2019. Toward an artificial intelligence physicist for unsupervised learning.. Physical review. E, 100 3-1 ( 2019 ), 033311. Tailin Wu and Max Tegmark. 2019. Toward an artificial intelligence physicist for unsupervised learning.. Physical review. E, 100 3-1 (2019), 033311."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563348","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563348","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:11Z","timestamp":1750178291000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563348"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":61,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563348"],"URL":"https:\/\/doi.org\/10.1145\/3563348","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}