{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:17:07Z","timestamp":1772043427525,"version":"3.50.1"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030294359","type":"print"},{"value":"9783030294366","type":"electronic"}],"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-29436-6_11","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"178-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["NIL: Learning Nonlinear Interpolants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8840-5605","authenticated-orcid":false,"given":"Jian","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9260-9697","authenticated-orcid":false,"given":"Jie","family":"An","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5377-9351","authenticated-orcid":false,"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2464-2895","authenticated-orcid":false,"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"11_CR1","unstructured":"Bennett, K.P., Bredensteiner, E.J.: Duality and geometry in SVM classifiers. In: ICML 2000, pp. 57\u201364 (2000)"},{"key":"11_CR2","first-page":"326","volume-title":"Pattern Recognition and Machine Learning","author":"CM Bishop","year":"2006","unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning, pp. 326\u2013328. Springer, New York (2006)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Boser, B.E., Guyon, I., Vapnik, V.: A training algorithm for optimal margin classifiers. In: COLT 1992, pp. 144\u2013152 (1992)","DOI":"10.1145\/130385.130401"},{"key":"11_CR4","series-title":"Elements of Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61715-7","volume-title":"Topological Vector Spaces","author":"N Bourbaki","year":"1987","unstructured":"Bourbaki, N.: Topological Vector Spaces. Elements of Mathematics. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/978-3-642-61715-7"},{"issue":"3","key":"11_CR5","first-page":"27:1","volume":"2","author":"C Chang","year":"2011","unstructured":"Chang, C., Lin, C.: LIBSVM: a library for support vector machines. ACM TIST 2(3), 27:1\u201327:27 (2011)","journal-title":"ACM TIST"},{"key":"11_CR6","unstructured":"Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N.: NIL: learning nonlinear interpolants (full version). http:\/\/lcs.ios.ac.cn\/~chenms\/papers\/CADE-27_FULL.pdf"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-540-78800-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2008","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397\u2013412. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_30"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"11_CR9","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"},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-39799-8_25","volume-title":"Computer Aided Verification","author":"L Dai","year":"2013","unstructured":"Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 364\u2013380. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_25"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Dathathri, S., Arechiga, N., Gao, S., Murray, R.M.: Learning-based abstractions for nonlinear constraint solving. In: IJCAI 2017, pp. 592\u2013599 (2017)","DOI":"10.24963\/ijcai.2017\/83"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-11319-2_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129\u2013145. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11319-2_12"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-40229-1_14","volume-title":"Automated Reasoning","author":"T Gan","year":"2016","unstructured":"Gan, T., Dai, L., Xia, B., Zhan, N., Kapur, D., Chen, M.: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 195\u2013212. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_14"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-662-49674-9_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Gao","year":"2016","unstructured":"Gao, S., Zufferey, D.: Interpolants in nonlinear theories over the reals. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 625\u2013641. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_41"},{"issue":"2","key":"11_CR16","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BF01362149","volume":"207","author":"S Gilbert","year":"1974","unstructured":"Gilbert, S.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87\u201397 (1974)","journal-title":"Math. Ann."},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"BS Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443\u2013458. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_33"},{"key":"11_CR19","series-title":"Springer Series in Statistics","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-84858-7","volume-title":"The Elements of Statistical Learning: Data Mining, Inference, and Prediction","author":"T Hastie","year":"2009","unstructured":"Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning: Data Mining, Inference, and Prediction. SSS, 2nd edn. Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-0-387-84858-7","edition":"2"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"issue":"7","key":"11_CR21","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1016\/j.jsc.2011.05.014","volume":"47","author":"H Hong","year":"2012","unstructured":"Hong, H., Din, M.S.E.: Variant quantifier elimination. J. Symb. Comput. 47(7), 883\u2013901 (2012)","journal-title":"J. Symb. Comput."},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE 2010, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-10575-8_15","volume-title":"Handbook of Model Checking","author":"R Jhala","year":"2018","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 447\u2013491. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_15"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-642-19835-9_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Jung","year":"2011","unstructured":"Jung, Y., Lee, W., Wang, B.-Y., Yi, K.: Predicate generation for learning-based quantifier-free loop invariant inference. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 205\u2013219. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_17"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: FSE 2006, pp. 105\u2013116 (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 199\u2013213. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_17"},{"issue":"2","key":"11_CR27","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-24310-3_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240\u2013255. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_17"},{"key":"11_CR29","volume-title":"Introduction to Diophantine Approximations: New Expanded Edition","author":"S Lang","year":"2012","unstructured":"Lang, S.: Introduction to Diophantine Approximations: New Expanded Edition. Springer, New York (2012)"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_2"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413\u2013427. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_31"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-71237-6_24","volume-title":"Programming Languages and Systems","author":"T Okudono","year":"2017","unstructured":"Okudono, T., Nishida, Y., Kojima, K., Suenaga, K., Kido, K., Hasuo, I.: Sharper and simpler nonlinear interpolants for program verification. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 491\u2013513. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_24"},{"issue":"2","key":"11_CR34","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","journal-title":"Math. Program."},{"issue":"3","key":"11_CR35","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346\u2013362. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_25"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-31424-7_11","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2012","unstructured":"Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 71\u201387. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_11"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11814771_21","volume-title":"Automated Reasoning","author":"V Sofronie-Stokkermans","year":"2006","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 235\u2013250. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_21"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-40229-1_19","volume-title":"Automated Reasoning","author":"V Sofronie-Stokkermans","year":"2016","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 273\u2013289. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_19"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI 2005, pp. 281\u2013294 (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Strzebo\u0144ski, A.W.: Real root isolation for exp-log functions. In: ISSAC 2008, pp. 303\u2013314 (2008)","DOI":"10.1145\/1390768.1390810"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Strzebo\u0144ski, A.W.: Real root isolation for tame elementary functions. In: ISSAC 2009, pp. 341\u2013350 (2009)","DOI":"10.1145\/1576702.1576749"},{"issue":"11","key":"11_CR43","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.1016\/j.jsc.2011.08.009","volume":"46","author":"AW Strzebo\u0144ski","year":"2011","unstructured":"Strzebo\u0144ski, A.W.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46(11), 1284\u20131290 (2011)","journal-title":"J. Symb. Comput."},{"key":"11_CR44","doi-asserted-by":"publisher","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)"},{"key":"11_CR45","first-page":"774","volume":"24","author":"V Vladimir","year":"1963","unstructured":"Vladimir, V.: Pattern recognition using generalized portrait method. Autom. Remote Control 24, 774\u2013780 (1963)","journal-title":"Autom. Remote Control"},{"key":"11_CR46","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Automated Deduction \u2013 CADE-20","author":"G Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353\u2013368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_26"},{"issue":"9","key":"11_CR47","doi-asserted-by":"publisher","first-page":"1361","DOI":"10.1007\/s11425-007-0092-6","volume":"50","author":"J Zhang","year":"2007","unstructured":"Zhang, J., Feng, Y.: Obtaining exact value by approximate computations. Sci. China Ser. A Math. 50(9), 1361 (2007)","journal-title":"Sci. China Ser. A Math."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:54:22Z","timestamp":1657576462000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","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":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","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":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}