{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,27]],"date-time":"2025-07-27T07:15:48Z","timestamp":1753600548528},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642406621"},{"type":"electronic","value":"9783642406638"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40663-8_18","type":"book-chapter","created":{"date-parts":[[2013,8,20]],"date-time":"2013-08-20T01:03:57Z","timestamp":1376960637000},"page":"186-198","source":"Crossref","is-referenced-by-count":8,"title":["On Gr\u00f6bner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Junges","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Loup","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Corzilius","sequence":"additional","affiliation":[]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Becker, T., Weispfenning, V., Kredel, H.: Gr\u00f6bner bases: a computational approach to commutative algebra. Graduate texts in mathematics. Springer (1993)","DOI":"10.1007\/978-1-4612-0913-3"},{"key":"18_CR2","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"18_CR3","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, University of Innsbruck (1965)"},{"key":"18_CR4","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 real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-642-31612-8_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"F. Corzilius","year":"2012","unstructured":"Corzilius, F., Loup, U., Junges, S., \u00c1brah\u00e1m, E.: SMT-RAT: An SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 442\u2013448. Springer, Heidelberg (2012)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"de Moura, L., Passmore, G.O.: On locally minimal Nullstellensatz proofs. In: Proc. of SMT 2009, pp. 35\u201342 (2009)","DOI":"10.1145\/1670412.1670418"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1006\/jsco.1997.0123","volume":"24","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Simplification of quantifier-free formulas over ordered fields. Journal of Symbolic Computation\u00a024, 209\u2013231 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"18_CR9","unstructured":"Gao, S., Ganai, M.K., Ivancic, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In: Proc. of FMCAD 2010, pp. 81\u201389. IEEE (2010)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Junges, S., Loup, U., Corzilius, F., \u00c1brah\u00e1m, E.: On Gr\u00f6bner bases in the context of satisfiability-modulo-theories solving over the real numbers. Technical Report AIB-2013-08, RWTH Aachen University (May 2013)","DOI":"10.1007\/978-3-642-40663-8_18"},{"key":"18_CR11","unstructured":"Passmore, G.O.: Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex. PhD thesis, University of Edinburgh (2011)"},{"key":"18_CR12","unstructured":"Passmore, G.O., de Moura, L., Jackson, P.B.: Gr\u00f6bner basis construction algorithms based on theorem proving saturation loops. In: Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proc., vol.\u00a010161 (2010)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-02959-2_35","volume-title":"Automated Deduction \u2013 CADE-22","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 485\u2013501. Springer, Heidelberg (2009)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Roune, B.H., Stillman, M.: Practical Gr\u00f6bner basis computation. In: Proc. of ISSAC 2012, pp. 203\u2013210. ACM (2012)","DOI":"10.1145\/2442829.2442860"},{"issue":"2","key":"18_CR15","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. AAECC\u00a08(2), 85\u2013101 (1997)","journal-title":"AAECC"}],"container-title":["Lecture Notes in Computer Science","Algebraic Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40663-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T18:39:26Z","timestamp":1558031966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40663-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642406621","9783642406638"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40663-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}