{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T16:58:25Z","timestamp":1756573105595,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-16-1-0288"],"award-info":[{"award-number":["FA9550-16-1-0288"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Alexander von Humboldt Foundation","award":[""],"award-info":[{"award-number":[""]}]},{"name":"A*STAR, Singapore","award":[""],"award-info":[{"award-number":[""]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1739629,DGE1252522,DGE1745016"],"award-info":[{"award-number":["CNS-1739629,DGE1252522,DGE1745016"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575672","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"211-224","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A First Complete Algorithm for Real Quantifier Elimination in Isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Katherine","family":"Kosaian","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"KIT, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-33099-2"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90029-2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0463"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl"},{"key":"e_1_3_2_1_6_1","unstructured":"Cyril Cohen. 2012. Formalized algebraic numbers: construction and first-order theory. Ph. D. Dissertation. \u00c9cole polytechnique. https:\/\/perso.crans.org\/cohen\/papers\/thesis.pdf"},{"key":"e_1_3_2_1_7_1","unstructured":"Cyril Cohen. 2021. Formalization of a sign determination algorithm in real algebraic geometry. Preprint on webpage at https:\/\/hal.inria.fr\/hal-03274013\/document"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:2)2012"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07407-4_17"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80152-6"},{"key":"e_1_3_2_1_11_1","volume-title":"Yong Kiam Tan, and Andr\u00e9 Platzer","author":"Cordwell Katherine","year":"2021","unstructured":"Katherine Cordwell, Yong Kiam Tan, and Andr\u00e9 Platzer. 2021. The BKR Decision Procedure for Univariate Real Arithmetic. Archive of Formal Proofs, April, https:\/\/www.isa-afp.org\/entries\/BenOr_Kozen_Reif.html"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.14"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01387193"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80004-X"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_12"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1005285.1005303"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693166"},{"key":"e_1_3_2_1_18_1","unstructured":"Manuel Eberl and Ren\u00e9 Thiemann. 2021. Factorization of Polynomials with Algebraic Coefficients. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Factor_Algebraic_Polynomial.html"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl"},{"key":"e_1_3_2_1_21_1","unstructured":"Hoon Hong. 1991. Comparison of Several Decision Algorithms for the Existential Theory of the Reals. RISC. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.30.8707"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_3_2_1_23_1","volume-title":"Yong Kiam Tan, and Andr\u00e9 Platzer","author":"Kosaian Katherine","year":"2022","unstructured":"Katherine Kosaian, Yong Kiam Tan, and Andr\u00e9 Platzer. 2022. A First Complete Algorithm for Real Quantifier Elimination in Isabelle\/HOL. Archive of Formal Proofs, Dec., https:\/\/www.isa-afp.org\/entries\/Quantifier_Elimination_Hybrid.html"},{"key":"e_1_3_2_1_24_1","unstructured":"Wenda Li. 2014. The Sturm-Tarski Theorem. Archive of Formal Proofs Sept. issn:2150-914x https:\/\/isa-afp.org\/entries\/Sturm_Tarski.html"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9424-6"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854074"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600586X"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15984-3_277"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_22"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9320-x"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9183-0"},{"key":"e_1_3_2_1_33_1","volume-title":"Paulson and Jasmin Christian Blanchette","author":"Lawrence","year":"2010","unstructured":"Lawrence C. Paulson and Jasmin Christian Blanchette. 2010. Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In IWIL, Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska (Eds.) (EPiC Series in Computing, Vol. 2). EasyChair, 1\u201311."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80005-7"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_11"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Matias Scharager Katherine Cordwell Stefan Mitsch and Andr\u00e9 Platzer. 2021. Verified Quadratic Virtual Substitution for Real Arithmetic. Archive of Formal Proofs October issn:2150-914x https:\/\/isa-afp.org\/entries\/Virtual_Substitution.html","DOI":"10.1007\/978-3-030-90870-6_11"},{"key":"e_1_3_2_1_39_1","first-page":"525","article-title":"Solving algebraic inequalities","volume":"7","author":"Strzebo\u0144ski Adam","year":"2000","unstructured":"Adam Strzebo\u0144ski. 2000. Solving algebraic inequalities. The Mathematica Journal, 7, 4 (2000), 525\u2013541.","journal-title":"The Mathematica Journal"},{"volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski Alfred","key":"e_1_3_2_1_40_1","unstructured":"Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica, CA. https:\/\/www.rand.org\/pubs\/reports\/R109.html"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80003-8"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_3"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575672","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575672","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575672","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:37Z","timestamp":1750178737000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575672"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":42,"alternative-id":["10.1145\/3573105.3575672","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575672","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}