{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:32:51Z","timestamp":1742920371613,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_12","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"181-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers"],"prefix":"10.1007","author":[{"given":"Grant Olney","family":"Passmore","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comp. Logic vol. 9(1), Article No. 2 (2007)","DOI":"10.1145\/1297658.1297660"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2006.10.005","volume":"370","author":"J Avigad","year":"2007","unstructured":"Avigad, J., Yin, Y.: Quantifier elimination for the reals with a predicate for the powers of two. Theor. Comput. Sci. 370, 1\u20133 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer, Secaucus (2006)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Collins, G.E., Akritas, A.G.: Polynomial real root isolation using Descarte\u2019s rule of signs. In: ACM Symposium on Symbolic and Algebraic computation. ACM (1976)","DOI":"10.1145\/800205.806346"},{"issue":"1\u20132","key":"12_CR5","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF01171706","volume":"54","author":"L van den Dries","year":"1985","unstructured":"van den Dries, L.: The field of reals with a predicate for the powers of two. Manuscr. Math. 54(1\u20132), 187\u2013195 (1985)","journal-title":"Manuscr. Math."},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1016\/j.jnt.2009.08.009","volume":"130","author":"M Hirvensalo","year":"2010","unstructured":"Hirvensalo, M., Karhum\u00e4ki, J., Rabinovich, A.: Computing partial information out of intractable: powers of algebraic numbers as an example. J. Number Theor. 130(2), 232\u2013253 (2010)","journal-title":"J. Number Theor."},{"issue":"2","key":"12_CR7","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0022-314X(01)92763-5","volume":"95","author":"M van Hoeij","year":"2002","unstructured":"van Hoeij, M.: Factoring polynomials and the knapsack problem. J. Number Theor. 95(2), 167\u2013189 (2002)","journal-title":"J. Number Theor."},{"issue":"4","key":"12_CR8","doi-asserted-by":"crossref","first-page":"329","DOI":"10.4064\/aa-45-4-329-335","volume":"45","author":"H Hollmann","year":"1986","unstructured":"Hollmann, H.: Factorisation of $$x^n - q$$ over Q. Acta Arith. 45(4), 329\u2013335 (1986)","journal-title":"Acta Arith."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Koenigsmann, J.: Defining $$\\mathbb{Z}$$ in $$\\mathbb{Q}$$. Annals of Mathematics, To appear (2015)","DOI":"10.4007\/annals.2016.183.1.2"},{"key":"12_CR10","unstructured":"Koenigsmann, J.: Personal communication (2015)"},{"key":"12_CR11","volume-title":"Hilbert\u2019s Tenth Problem","author":"Y Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.: Hilbert\u2019s Tenth Problem. MIT Press, Cambridge (1993)"},{"key":"12_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4344-1","volume-title":"Algorithmic Algebra","author":"B Mishra","year":"1993","unstructured":"Mishra, B.: Algorithmic Algebra. Springer, New York (1993)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-38574-2_12","volume-title":"Automated Deduction \u2013 CADE-24","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 178\u2013192. Springer, Heidelberg (2013)"},{"key":"12_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover, vol. 828. Springer, New York (1994)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32347-8_1","volume-title":"Interactive Theorem Proving","author":"LC Paulson","year":"2012","unstructured":"Paulson, L.C.: MetiTarski: past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1\u201310. Springer, Heidelberg (2012)"},{"issue":"3","key":"12_CR16","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1353\/ajm.0.0057","volume":"131","author":"B Poonen","year":"2009","unstructured":"Poonen, B.: Characterizing integers among rational numbers with a universal-existential formula. Am. J. Math. 131(3), 675\u2013682 (2009)","journal-title":"Am. J. Math."},{"issue":"3\u20134","key":"12_CR17","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1016\/S0747-7171(03)00093-2","volume":"36","author":"R Rioboo","year":"2003","unstructured":"Rioboo, R.: Towards faster real algebraic numbers. J. Sym. Comp. 36(3\u20134), 513\u2013533 (2003)","journal-title":"J. Sym. Comp."},{"key":"12_CR18","unstructured":"Robinson, J.: Definability and Decision Problems in Arithmetic. Ph.D. thesis, University of California, Berkeley (1948)"},{"key":"12_CR19","volume-title":"Theory of Equations","author":"JV Uspensky","year":"1948","unstructured":"Uspensky, J.V.: Theory of Equations. McGraw-Hill, New York (1948)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC 1999, New York, NY, USA (1999)","DOI":"10.1145\/309831.309888"},{"key":"12_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/11542384","volume-title":"The Seventeen Provers of the World","author":"F Wiedijk","year":"2006","unstructured":"Wiedijk, F.: The Seventeen Provers of the World. Springer, New York (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T13:33:03Z","timestamp":1674567183000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}