{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:14:56Z","timestamp":1759637696260},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030290061"},{"type":"electronic","value":"9783030290078"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-29007-8_8","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:10:06Z","timestamp":1566414606000},"page":"131-148","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A CDCL-Style Calculus for Solving Non-linear Constraints"],"prefix":"10.1007","author":[{"given":"Franz","family":"Brau\u00dfe","sequence":"first","affiliation":[]},{"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[]},{"given":"Margarita","family":"Korovina","sequence":"additional","affiliation":[]},{"given":"Norbert","family":"M\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Handbook of Constraint Programming, pp. 571\u2013603. Elsevier (2006)","DOI":"10.1016\/S1574-6526(06)80020-9"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-0-387-68546-5_18","volume-title":"New Computational Paradigms","author":"V Brattka","year":"2008","unstructured":"Brattka, V., Hertling, P., Weihrauch, K.: A tutorial on computable analysis. In: Cooper, S.B., L\u00f6we, B., Sorbi, A. (eds.) New Computational Paradigms, pp. 425\u2013491. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-0-387-68546-5_18"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1088216.1088219","volume":"10","author":"B Buchberger","year":"1976","unstructured":"Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bull. 10(3), 19\u201329 (1976)","journal-title":"ACM SIGSAM Bull."},{"issue":"3","key":"8_CR4","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/3230639","volume":"19","author":"A Cimatti","year":"2018","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1\u201319:52 (2018)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20\u201323, 1975","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"issue":"2","key":"8_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. ACM SIGSAM Bull. 31(2), 2\u20139 (1997)","journal-title":"ACM SIGSAM Bull."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Dragan, I., Korovin, K., Kov\u00e1cs, L., Voronkov, A.: Bound propagation for arithmetic reasoning in Vampire. In: Proceedings SYNASC 2013, pp. 169\u2013176. IEEE (2013)","DOI":"10.1109\/SYNASC.2013.30"},{"key":"8_CR9","unstructured":"Fontaine, P., Ogawa, M., Sturm, T., To, V.K., Vu, X.T.: Wrapping computer algebra is surprisingly successful for non-linear SMT. In: SC-Square 2018, Oxford, United Kingdom, July 2018"},{"issue":"3\u20134","key":"8_CR10","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. JSAT 1(3\u20134), 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$ -complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_23"},{"issue":"3\u20134","key":"8_CR12","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s11786-014-0195-8","volume":"8","author":"M Hlad\u00edk","year":"2014","unstructured":"Hlad\u00edk, M., Ratschan, S.: Efficient solution of a class of quantified constraints with quantifier prefix Exists-Forall. Math. Comput. Sci. 8(3\u20134), 329\u2013340 (2014)","journal-title":"Math. Comput. Sci."},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Kapur, D., Sun, Y., Wang, D.: A new algorithm for computing comprehensive Gr\u00f6bner systems. In: Proceedings ISSAC 2010, pp. 29\u201336. ACM, New York, USA (2010)","DOI":"10.1145\/1837934.1837946"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-319-10515-4_19","volume-title":"Computer Algebra in Scientific Computing","author":"K Korovin","year":"2014","unstructured":"Korovin, K., Kos\u0306ta, M., Sturm, T.: Towards conflict-driven learning for virtual substitution. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2014. LNCS, vol. 8660, pp. 256\u2013270. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10515-4_19"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-29709-0_31","volume-title":"Perspectives of Systems Informatics","author":"K Korovin","year":"2012","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Implementing conflict resolution. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 362\u2013376. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29709-0_31"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-04244-7_41","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K Korovin","year":"2009","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509\u2013523. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04244-7_41"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-22438-6_28","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Korovin","year":"2011","unstructured":"Korovin, K., Voronkov, A.: Solving systems of linear inequalities by bound propagation. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 369\u2013383. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_28"},{"key":"8_CR19","unstructured":"Lef\u00e9vre, V.: Moyens arithmetiques pour un calcul fiable. PhD thesis, \u00c9cole normale sup\u00e9rieure de Lyon (2000)"},{"issue":"5","key":"8_CR20","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993)","journal-title":"Comput. J."},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-662-49122-5_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Mar\u00e9chal","year":"2016","unstructured":"Mar\u00e9chal, A., Fouilh\u00e9, A., King, T., Monniaux, D., P\u00e9rin, M.: Polyhedral approximation of multivariate polynomials using Handelman\u2019s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166\u2013184. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_8"},{"issue":"5","key":"8_CR22","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462\u2013476. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_35"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-45335-0_14","volume-title":"Computability and Complexity in Analysis","author":"NT M\u00fcller","year":"2001","unstructured":"M\u00fcller, N.T.: The iRRAM: exact arithmetic in C++. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222\u2013252. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45335-0_14"},{"issue":"6","key":"8_CR25","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"8_CR26","doi-asserted-by":"crossref","DOI":"10.5948\/9781614440116","volume-title":"Irrational Numbers","author":"I Niven","year":"1956","unstructured":"Niven, I.: Irrational Numbers. Mathematical Association of America, Washington, D.C. (1956)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-31374-5_24","volume-title":"Intelligent Computer Mathematics","author":"GO Passmore","year":"2012","unstructured":"Passmore, G.O., Paulson, L.C., de Moura, L.: Real algebraic strategies for MetiTarski proofs. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 358\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_24"},{"key":"8_CR28","unstructured":"Reger, G., Bjorner, N., Suda, M., Voronkov, A.: AVATAR modulo theories. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.), 2nd Global Conference on Artificial Intelligence, EPiC Series in Computing, vol. 41, pp. 39\u201352. EasyChair (2016)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-66167-4_2","volume-title":"Frontiers of Combining Systems","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Tinelli, C., Jovanovi\u0107, D., Barrett, C.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 22\u201340. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_2"},{"issue":"4","key":"8_CR30","doi-asserted-by":"publisher","first-page":"514","DOI":"10.2307\/2271358","volume":"33","author":"D Richardson","year":"1968","unstructured":"Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514\u2013520 (1968)","journal-title":"J. Symb. Log."},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: 2nd edn. University of California (1951)","DOI":"10.1525\/9780520348097"},{"key":"8_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56999-9","volume-title":"Computable Analysis: An Introduction","author":"K Weihrauch","year":"2000","unstructured":"Weihrauch, K.: Computable Analysis: An Introduction. Springer, Secaucus (2000). https:\/\/doi.org\/10.1007\/978-3-642-56999-9"}],"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-030-29007-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,25]],"date-time":"2022-09-25T22:35:58Z","timestamp":1664145358000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29007-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290061","9783030290078"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29007-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.frocos2019.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}