{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:53:47Z","timestamp":1725515627597},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_24","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"358-370","source":"Crossref","is-referenced-by-count":8,"title":["Real Algebraic Strategies for MetiTarski Proofs"],"prefix":"10.1007","author":[{"given":"Grant Olney","family":"Passmore","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"24_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.: MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. Journal of Automated Reasoning\u00a044(3), 175\u2013205 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/980175.980185","volume":"38","author":"C.W. Brown","year":"2004","unstructured":"Brown, C.W.: QEPCAD-B: A System for Computing with Semi-algebraic Sets via Cylindrical Algebraic Decomposition. SIGSAM Bull.\u00a038, 23\u201324 (2004)","journal-title":"SIGSAM Bull."},{"key":"24_CR3","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. J. Symb. Comput.\u00a05, 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L. Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: RealPaver: An Interval Solver using Constraint Satisfaction Techniques. ACM Trans. on Mathematical Software\u00a032, 138\u2013156 (2006)","journal-title":"ACM Trans. on Mathematical Software"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-Based Approach for Analysis of Hybrid Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 190\u2013203. Springer, Heidelberg (2008)"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Jovanovic\u0300, D., de Moura, L.: Solving Nonlinear Arithmetic. In: IJCAR 2012 (2012)","DOI":"10.1007\/978-3-642-31365-3_27"},{"issue":"3","key":"24_CR8","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1006\/jsco.1999.0327","volume":"29","author":"A. Strzebonski","year":"2000","unstructured":"Strzebonski, A.: Solving Systems of Strict Polynomial Inequalities. Journal of Symbolic Computation\u00a029(3), 471\u2013480 (2000)","journal-title":"Journal of Symbolic Computation"},{"issue":"9","key":"24_CR9","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1016\/j.jsc.2006.06.004","volume":"41","author":"A. Strzebonski","year":"2006","unstructured":"Strzebonski, A.: Cylindrical Algebraic Decomposition using Validated Numerics. Journal of Symbolic Computation\u00a041(9), 1021\u20131038 (2006)","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/1576702.1576749","volume-title":"Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC 2009","author":"A. Strzebonski","year":"2009","unstructured":"Strzebonski, A.: Real Root Isolation for Tame Elementary Functions. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, pp. 341\u2013350. ACM, New York (2009)"}],"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-31374-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:22:23Z","timestamp":1556889743000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}