{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:22Z","timestamp":1750309522623,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Novo Nordisk Fonden","award":["NNF20OC0063462"],"award-info":[{"award-number":["NNF20OC0063462"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705882","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"171-186","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An Isabelle\/HOL Framework for Synthetic Completeness Proofs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-0804","authenticated-orcid":false,"given":"Asta Halkj\u00e6r","family":"From","sequence":"first","affiliation":[{"name":"University of Copenhagen, Copenhagen, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89391-0_25"},{"key":"e_1_3_2_2_3_1","unstructured":"Stefan Berghofer. 2007. First-Order Logic According to Fitting. Archive of Formal Proofs Aug. issn:2150-914x https:\/\/isa-afp.org\/entries\/FOL-Fitting.html"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294087"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_8"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9391-3"},{"key":"e_1_3_2_2_8_1","first-page":"49","article-title":"G\u00f6del\u2019s completeness theorem","volume":"13","author":"Braselmann Patrick","year":"2005","unstructured":"Patrick Braselmann and Peter Koepke. 2005. G\u00f6del\u2019s completeness theorem. Formalized Mathematics, 13, 1 (2005), 49\u201353.","journal-title":"Formalized Mathematics"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0002-4"},{"volume-title":"Model theory","author":"Chang Chen C.","key":"e_1_3_2_2_10_1","unstructured":"Chen C. Chang and H. Jerome Keisler. 1992. Model theory, Third Edition (Studies in logic and the foundations of mathematics, Vol. 73). North-Holland. isbn:978-0-444-88054-3"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2013.07.009"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70216-7"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_18"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2020.5"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88853-4_1"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2021.8"},{"key":"e_1_3_2_2_20_1","unstructured":"Asta Halkj\u00e6r From. 2023. Formally Correct Deduction Methods for Computational Logic. Ph. D. Dissertation. Chapter 8"},{"key":"e_1_3_2_2_21_1","unstructured":"Asta Halkj\u00e6r From. 2023. Synthetic Completeness. Archive of Formal Proofs January issn:2150-914x https:\/\/isa-afp.org\/entries\/Synthetic_Completeness.html Formal proof development. At time of writing the formalization corresponding to this paper is only available in the development version of the archive"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","unstructured":"Asta Halkj\u00e6r From. 2024. Formalization for An Isabelle\/HOL Framework for Synthetic Completeness Proofs. https:\/\/doi.org\/10.5281\/zenodo.14278854 10.5281\/zenodo.14278854","DOI":"10.5281\/zenodo.14278854"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-024-09697-3"},{"key":"e_1_3_2_2_24_1","volume-title":"Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021, Stefania Monica and Federico Bergenti (Eds.) (CEUR Workshop Proceedings","volume":"121","author":"From Asta Halkj\u00e6","year":"2021","unstructured":"Asta Halkj\u00e6 r From, Anders Schlichtkrull, and J\u00f8rgen Villadsen. 2021. A Sequent Calculus for First-Order Logic Formalized in Isabelle\/HOL. In Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021, Stefania Monica and Federico Bergenti (Eds.) (CEUR Workshop Proceedings, Vol. 3002). CEUR-WS.org, 107\u2013121. http:\/\/ceur-ws.org\/Vol-3002\/paper7.pdf"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/LOGCOM"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055135"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/421107"},{"volume-title":"Constructive Completeness Proofs and Delimited Control. (Preuves constructives de compl\u00e9tude et contr\u00f4le d\u00e9limit\u00e9 ). Ph. D. Dissertation. \u00c9cole Polytechnique","author":"Ilik Danko","key":"e_1_3_2_2_28_1","unstructured":"Danko Ilik. 2010. Constructive Completeness Proofs and Delimited Control. (Preuves constructives de compl\u00e9tude et contr\u00f4le d\u00e9limit\u00e9 ). Ph. D. Dissertation. \u00c9cole Polytechnique, Palaiseau, France. https:\/\/tel.archives-ouvertes.fr\/tel-00529021"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-022-09647-X"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2023.30"},{"key":"e_1_3_2_2_31_1","unstructured":"Jiatu Li. 2020. Formalization of PAL\u22c5 S5 in Proof Assistant. arxiv:2012.09388. arxiv:2012.09388"},{"key":"e_1_3_2_2_32_1","unstructured":"James Margetson and Tom Ridge. 2004. Completeness theorem. Archive of Formal Proofs Sept. issn:2150-914x http:\/\/isa-afp.org\/entries\/Completeness.html"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2017.5"},{"key":"e_1_3_2_2_34_1","unstructured":"Paula Neeley. 2021. Results in Modal and Dynamic Epistemic Logic: A Formalization in Lean. https:\/\/leanprover-community.github.io\/lt2021\/slides\/paula-LeanTogether2021.pdf slides."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science Vol. 2283). Springer. isbn:3-540-43376-7 https:\/\/doi.org\/10.1007\/3-540-45949-9 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science Vol. 2283). Springer. isbn:3-540-43376-7 https:\/\/doi.org\/10.1007\/3-540-45949-9 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_16"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-015-9322-8"},{"volume-title":"Constructive completeness of intuitionistic predicate logic. Licenciate thesis","author":"Persson Henrik","key":"e_1_3_2_2_39_1","unstructured":"Henrik Persson. 1996. Constructive completeness of intuitionistic predicate logic. Licenciate thesis, Chalmers University of Technology."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73859-6_28"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_26"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_19"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9447-z"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.2478\/v10037-012-0023-z"},{"volume-title":"First-Order Logic","author":"Smullyan Raymond M.","key":"e_1_3_2_2_45_1","unstructured":"Raymond M. Smullyan. 1995. First-Order Logic. Dover Publications, Mineola, New York."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704893"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705882","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705882","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705882"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":46,"alternative-id":["10.1145\/3703595.3705882","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705882","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}