{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:46:05Z","timestamp":1743115565707,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the calculus and show that it is a<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\delta $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03b4<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_7","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"113-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The ksmt Calculus Is a $$\\delta $$-complete Decision Procedure for Non-linear Constraints"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2386-7489","authenticated-orcid":false,"given":"Franz","family":"Brau\u00dfe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0740-621X","authenticated-orcid":false,"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2707-0231","authenticated-orcid":false,"given":"Margarita V.","family":"Korovina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3684-3029","authenticated-orcid":false,"given":"Norbert Th.","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Bard, J., Becker, H., Darulova, E.: Formally verified roundoff errors using SMTbased certificates and subdivisions. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Proceedings. LNCS, vol. 11800, pp. 38\u201344. Springer (2019)","DOI":"10.1007\/978-3-030-30942-8_4"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume\u2013guarantee verification of nonlinear hybrid systems with Ariadne. International Journal of Robust and Nonlinear Control 24(4), 699\u2013724 (2014)","DOI":"10.1002\/rnc.2914"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: Transition system and completeness. J. Autom. Reason. 64(3), 579\u2013609 (2020)","DOI":"10.1007\/s10817-018-09510-y"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Brattka, V., Hertling, P.: Topological properties of real number representations. Theor. Comput. Sci. 284(2), 241\u2013257 (2002)","DOI":"10.1016\/S0304-3975(01)00066-4"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Brattka, V., Hertling, P., Weihrauch, K.: A Tutorial on Computable Analysis, pp. 425\u2013491. Springer New York, New York, NY (2008)","DOI":"10.1007\/978-0-387-68546-5_18"},{"key":"7_CR6","unstructured":"Brau\u00dfe, F., Khasidashvili, Z., Korovin, K.: Selecting stable safe configurations for systems modelled by neural networks with ReLU activation. In: Ivrii, A., Strichman, O. (eds.) 2020 Formal Methods in Computer Aided Design, FMCAD 2020. pp. 119\u2013127. IEEE (2020)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M.V., M\u00fcller, N.T.: A CDCL-style calculus for solving non-linear constraints. In: Herzig, A., Popescu, A. (eds.) Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, Proceedings. LNCS, vol. 11715, pp. 131\u2013148. Springer (2019)","DOI":"10.1007\/978-3-030-29007-8_8"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M.V., M\u00fcller, N.T.: The ksmt calculus is a $$\\delta $$-complete decision procedure for non-linear constraints. CoRR abs\/2104.13269 (2021)","DOI":"10.1007\/978-3-030-79876-5_7"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Korovina, M.V., M\u00fcller, N.T.: Towards using exact real arithmetic for initial value problems. In: Mazzara, M., Voronkov, A. (eds.) Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Revised Selected Papers. LNCS, vol. 9609, pp. 61\u201374. Springer (2015)","DOI":"10.1007\/978-3-319-41579-6_6"},{"key":"7_CR10","unstructured":"Brau\u00dfe, F., Steinberg, F.: A minimal representation for continuous functions. CoRR abs\/1703.10044 (2017)"},{"key":"7_CR11","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3230639"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Ogawa, M., Sturm, T., Vu, X.: Subtropical satisfiability. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. LNCS, vol. 10483, pp. 189\u2013206. Springer (2017)","DOI":"10.1007\/978-3-319-66167-4_11"},{"key":"7_CR13","doi-asserted-by":"crossref","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.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Proceedings. LNCS, vol. 7364, pp. 286\u2013300. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012. pp. 305\u2013314. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.41"},{"key":"7_CR15","unstructured":"Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J.M., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. CoRR abs\/1501.02155 (2015)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4), 104\u2013105 (2012)","DOI":"10.1145\/2429135.2429155"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Ko, K.: Complexity Theory of Real Functions. Birkh\u00e4user \/ Springer (1991)","DOI":"10.1007\/978-1-4684-6802-1"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Korovin, K., Kosta, M., Sturm, T.: Towards conflict-driven learning for virtual substitution. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing - 16th International Workshop, CASC 2014, Proceedings. LNCS, vol. 8660, pp. 256\u2013270. Springer (2014)","DOI":"10.1007\/978-3-319-10515-4_19"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Proceedings. LNCS, vol. 5732, pp. 509\u2013523. Springer (2009)","DOI":"10.1007\/978-3-642-04244-7_41"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: Solving systems of linear inequalities by bound propagation. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. LNCS, vol. 6803, pp. 369\u2013383. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_28"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Kur\u00e1tko, J., Ratschan, S.: Combined global and local search for the falsification of hybrid systems. In: Legay, A., Bozga, M. (eds.) Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings. LNCS, vol. 8711, pp. 146\u2013160. Springer (2014)","DOI":"10.1007\/978-3-319-10512-3_11"},{"key":"7_CR22","unstructured":"de Moura, L.M., Jovanovic, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Proceedings. LNCS, vol. 7737, pp. 1\u201312. Springer (2013)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina, M.P. (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Proceedings. LNCS, vol. 7898, pp. 178\u2013192. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_12"},{"key":"7_CR24","unstructured":"M\u00fcller, N.T.: The iRRAM: Exact arithmetic in C++. In: Blanck, J., Brattka, V., Hertling, P. (eds.) Computability and Complexity in Analysis, 4th International Workshop, CCA 2000, Selected Papers. LNCS, vol. 2064, pp. 222\u2013252. Springer (2000)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer (2018)","DOI":"10.1007\/978-3-319-63588-0"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Pour-El, M.B., Richards, J.I.: Computability in analysis and physics. Perspectives in Mathematical Logic, Springer (1989)","DOI":"10.1007\/978-3-662-21717-7"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514\u2013520 (1968)","DOI":"10.2307\/2271358"},{"key":"7_CR28","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1996. pp. 220\u2013227. IEEE Computer Society \/ ACM (1996)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Tiwari, A., Lincoln, P.: A search-based procedure for nonlinear real arithmetic. Formal Methods Syst. Des. 48(3), 257\u2013273 (2016)","DOI":"10.1007\/s10703-016-0245-8"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Tung, V.X., Khanh, T.V., Ogawa, M.: raSAT: An SMT solver for polynomial constraints. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. LNCS, vol. 9706, pp. 228\u2013237. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_16"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Weihrauch, K.: Computable Analysis \u2013 An Introduction. Texts in Theoretical Computer Science. An EATCS Series, Springer (2000)","DOI":"10.1007\/978-3-642-56999-9"},{"key":"7_CR32","unstructured":"Willard, S.: General Topology. Addison-Wesly (1970)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:24:47Z","timestamp":1672723487000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"38% - 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","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":"5","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}