{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:39Z","timestamp":1762459299198,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_10","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"151-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Adapting Real Quantifier Elimination Methods for Conflict Set Computation"],"prefix":"10.1007","author":[{"given":"Maximilian","family":"Jaroschek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo Federico","family":"Dobal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"10_CR1","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, chapter 26, pp. 825\u2013885. IOS Press, February 2009"},{"key":"10_CR2","unstructured":"Barrett, C.W.: Checking validity of quantifier-free formulas in combinations of first-order theories. PhD thesis, Stanford University (2003)"},{"issue":"3","key":"10_CR3","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s00165-007-0027-6","volume":"19","author":"D. Barsotti","year":"2007","unstructured":"Barsotti, D., Nieto, L.P., Tiu, A.: Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Form. Asp. Comput.\u00a019(3), 321\u2013341 (2007)","journal-title":"Form. Asp. Comput."},{"key":"10_CR4","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 Bulletin\u00a037, 97\u2013108 (2003)","journal-title":"SIGSAM Bulletin"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1277548.1277557","volume-title":"Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007","author":"C.W. Brown","year":"2007","unstructured":"Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54\u201360. ACM, New York (2007)"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.jsc.2014.09.024","volume":"70","author":"C.W. Brown","year":"2015","unstructured":"Brown, C.W., Kosta, M.: Constructing a single cell in cylindrical algebraic decomposition. J. Symb. Comput.\u00a070, 14\u201348 (2015)","journal-title":"J. Symb. Comput."},{"key":"10_CR7","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-662-43799-5_17","volume-title":"Computer Mathematics","author":"C. Chen","year":"2014","unstructured":"Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W.-S., Sato, Y. (eds.) Computer Mathematics, pp. 199\u2013221. Springer, Heidelberg (2014)"},{"issue":"3","key":"10_CR8","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/1086837.1086852","volume":"8","author":"G.E. Collins","year":"1974","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition\u2013preliminary report. SIGSAM Bull.\u00a08(3), 80\u201390 (1974)","journal-title":"SIGSAM Bull."},{"issue":"3","key":"10_CR9","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G.E. Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation\u00a012(3), 299\u2013328 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR10","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)"},{"issue":"1","key":"10_CR11","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 Computation\u00a05(1), 29\u201335 (1988)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2008.04.079","volume":"198","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Model-based theory combination. Electronic Notes in Theoretical Computer Science\u00a0198(2), 37\u201349 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1016\/j.scico.2010.04.003","volume":"77","author":"D.C.B. Oliveira de","year":"2012","unstructured":"de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: Combining decision procedures by (model-)equality propagation. Science of Computer Programming\u00a077(4), 518\u2013532 (2012)","journal-title":"Science of Computer Programming"},{"key":"10_CR14","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, Hewlett Packard Laboratories, July 23, 2003"},{"key":"10_CR15","unstructured":"Dolzmann, A.: Algorithmic strategies for applicable real quantifier elimination. PhD thesis, Universit\u00e4t Passau, Innstrasse 29, 94032 Passau (2000)"},{"issue":"2","key":"10_CR16","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."},{"issue":"2","key":"10_CR17","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 formulae over ordered fields. Journal of Symbolic Computation\u00a024(2), 209\u2013231 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR18","unstructured":"Hearn, A.C., Sch\u00f6pf, R.: Reduce User\u2019s Manual, Free Version, October 2014"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D. Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"King, T., Barrett, C., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: Claessen, K., Kuncak, V. (eds.) Formal Methods In Computer-Aided Design (FMCAD), Austin, TX, October, pp. 24:139\u201324:146. FMCAD Inc. (2014)","DOI":"10.1109\/FMCAD.2014.6987606"},{"key":"10_CR21","unstructured":"Kosta, M., Sturm, T., Dolzmann, A.: Better answers to real questions. CoRR, abs\/1501.05098 (2015)"},{"issue":"2","key":"10_CR22","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Rand report. Rand Corporation, 1948. Republished as A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)","DOI":"10.1525\/9780520348097"},{"issue":"1\u20132","key":"10_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation\u00a05(1\u20132), 3\u201327 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR25","unstructured":"Weispfenning, V.: A new approach to quantifier elimination for real algebra. Technical Report MIP-9305, FMI, Universit\u00e4t Passau, Germany, July 1993"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1993","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2013 the quadratic case and beyond. AAECC\u00a08, 85\u2013101 (1993)","journal-title":"AAECC"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/190347.190425","volume-title":"Proceedings of the International Symposium on Symbolic and Algebraic Computation","author":"V. Weispfenning","year":"1994","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2013 the cubic case. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, pp. 258\u2013263. ACM, New York (1994)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,14]],"date-time":"2023-08-14T08:47:33Z","timestamp":1692002853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_10","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":"12 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}