{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:56:48Z","timestamp":1760079408819},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026133"},{"type":"electronic","value":"9783642026140"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02614-0_14","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T07:47:24Z","timestamp":1246520844000},"page":"122-137","source":"Crossref","is-referenced-by-count":15,"title":["Combined Decision Techniques for the Existential Theory of the Reals"],"prefix":"10.1007","author":[{"given":"Grant Olney","family":"Passmore","sequence":"first","affiliation":[]},{"given":"Paul B.","family":"Jackson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.W. Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull.\u00a037(4), 97\u2013108 (2003)","journal-title":"SIGSAM Bull."},{"issue":"2","key":"14_CR2","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1002\/cpa.3160220202","volume":"XXII","author":"P.J. Cohen","year":"1969","unstructured":"Cohen, P.J.: Decision procedures for real and p-adic fields. Comm. Pure and Applied Mathematics\u00a0XXII(2), 131\u2013151 (1969)","journal-title":"Comm. Pure and Applied Mathematics"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"issue":"1-2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. Journal of Symbolic Computing\u00a05(1-2), 29\u201335 (1988)","journal-title":"Journal of Symbolic Computing"},{"issue":"3","key":"14_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"14_CR6","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1145\/1005285.1005303","volume-title":"ISSAC 2004: Proceedings of the 2004 international symposium on Symbolic and algebraic computation","author":"A. Dolzmann","year":"2004","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: ISSAC 2004: Proceedings of the 2004 international symposium on Symbolic and algebraic computation, pp. 111\u2013118. ACM Press, New York (2004)"},{"issue":"2","key":"14_CR7","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. SIGSAM Bull.\u00a031(2), 2\u20139 (1997)","journal-title":"SIGSAM Bull."},{"key":"14_CR8","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver (2006), http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"issue":"1,2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/S0747-7171(88)80005-1","volume":"5","author":"D. Yu Grigor\u2019ev","year":"1988","unstructured":"Yu Grigor\u2019ev, D., Vorobjov Jr., N.N.: Solving systems of polynomial inequalities in subexponential time. Journal of Symbolic Computation\u00a05(1,2), 37\u201364 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Hales, T.C.: Formalizing the proof of the Kepler Conjecture. In: Theorem Proving in Higher Order Logics (TPHOLs) (2004)","DOI":"10.1007\/978-3-540-30142-4_9"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"14_CR12","unstructured":"Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Technical report, RISC Linz (1991)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Laplagne, S.: An algorithm for the computation of the radical of an ideal. In: International Symposium on Symbolic and Algebraic Computation (2006)","DOI":"10.1145\/1145768.1145802"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition. The Computer Journal\u00a036(5) (1993)","DOI":"10.1093\/comjnl\/36.5.432"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.V.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"key":"14_CR16","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals (Part I). Technical Report 853, Cornell University (1989)"},{"key":"14_CR17","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Technical report, Rand Corporation (1948)"},{"key":"14_CR18","unstructured":"Tiwari, A.: HybridSAL: Modeling and abstracting hybrid systems. Technical report, SRI International (2003)"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11538363_18","volume-title":"Computer Science Logic","author":"A. Tiwari","year":"2005","unstructured":"Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 248\u2013262. Springer, Heidelberg (2005)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"van den Dries, L.: Tame topology and o-minimal structures. London Mathematical Society (1998)","DOI":"10.1017\/CBO9780511525919"},{"issue":"2","key":"14_CR21","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2013 the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing\u00a08(2), 85\u2013101 (1997)","journal-title":"Applicable Algebra in Engineering Communication and Computing"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02614-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T17:34:24Z","timestamp":1685036064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}