{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:04:54Z","timestamp":1753887894365,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"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_23","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"385-405","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["On Invariant Synthesis for Parametric Systems"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Peuter","sequence":"first","affiliation":[]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10703-014-0209-9","volume":"45","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63\u2013109 (2014)","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378\u2013394. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_27"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4\u20134. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_4"},{"issue":"4\u20135","key":"23_CR5","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4\u20135), 379\u2013405 (2008)","journal-title":"Formal Asp. Comput."},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/2490253","volume":"15","author":"R Bruttomesso","year":"2014","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5:1\u20135:34 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_55"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Hosking, A.L., Eugster, P.T., Lopes, C.V., (eds.) Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, pp. 443\u2013456. ACM (2013)","DOI":"10.1145\/2509136.2509511"},{"issue":"2","key":"23_CR10","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":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-73210-5_13","volume-title":"Integrated Formal Methods","author":"J Faber","year":"2007","unstructured":"Faber, J., Jacobs, S., Sofronie-Stokkermans, V.: Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 233\u2013252. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_13"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-319-23165-5_13","volume-title":"Logic, Rewriting, and Concurrency","author":"S Falke","year":"2015","unstructured":"Falke, S., Kapur, D.: When is a formula a loop invariant? In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 264\u2013286. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23165-5_13"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-25984-8_10","volume-title":"Automated Reasoning","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with weak equality. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 168\u2013182. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_10"},{"issue":"10","key":"23_CR14","doi-asserted-by":"publisher","first-page":"1453","DOI":"10.1016\/j.ic.2005.10.002","volume":"204","author":"H Ganzinger","year":"2006","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10), 1453\u20131492 (2006)","journal-title":"Inf. Comput."},{"issue":"4","key":"23_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-6(4:10)2010","volume":"6","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods Comput. Sci. 6(4), 1\u201348 (2010)","journal-title":"Logical Methods Comput. Sci."},{"key":"23_CR16","unstructured":"Gleiss, B., Kov\u00e1cs, L., Robillard, S.: Loop analysis by quantification over iterations. In: Barthe, G., Sutcliffe, G., Veanes, M., (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, LPAR-22, pp. 381\u2013399 (2018). EasyChair"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-030-01090-4_15","volume-title":"Automated Technology for Verification and Analysis","author":"A Gurfinkel","year":"2018","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248\u2013266. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-14203-1_16","volume-title":"Automated Reasoning","author":"K Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination in Vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 188\u2013195. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_16"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-40885-4_14","volume-title":"Frontiers of Combining Systems","author":"M Horbach","year":"2013","unstructured":"Horbach, M., Sofronie-Stokkermans, V.: Obtaining finite local theory axiomatizations via saturation. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 198\u2013213. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_14"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-08587-6_14","volume-title":"Automated Reasoning","author":"M Horbach","year":"2014","unstructured":"Horbach, M., Sofronie-Stokkermans, V.: Locality transfer: From constrained axiomatizations to reachability predicates. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 192\u2013207. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_14"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-04027-6_25","volume-title":"Computer Science Logic","author":"M Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Deciding the inductive validity of $$\\forall \\exists $$* queries. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 332\u2013347. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04027-6_25"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265\u2013281. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_19"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-02959-2_9","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Ihlemann","year":"2009","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: System description: H-PILoT. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 131\u2013139. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_9"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-14203-1_4","volume-title":"Automated Reasoning","author":"C Ihlemann","year":"2010","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 30\u201345. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_4"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-18275-4_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Jacobs","year":"2011","unstructured":"Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 278\u2013293. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_20"},{"issue":"3","key":"23_CR26","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11424-006-0307-x","volume":"19","author":"D Kapur","year":"2006","unstructured":"Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. J. Syst. Sci. Complexity 19(3), 307\u2013330 (2006)","journal-title":"J. Syst. Sci. Complexity"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Young, M., Devanbu, P.T., (eds.) Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, pp. 105\u2013116. ACM (2006)","DOI":"10.1145\/1181775.1181789"},{"issue":"1","key":"23_CR28","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3022187","volume":"64","author":"A Karbyshev","year":"2017","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1), 7:1\u20137:33 (2017)","journal-title":"J. ACM"},{"key":"23_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470\u2013485. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_33"},{"key":"23_CR30","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"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Bod\u00edk, R., Majumdar, R., (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 217\u2013231. ACM (2016)","DOI":"10.1145\/2837614.2837640"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Peuter, D., Sofronie-Stokkermans, V.: On invariant synthesis for parametric systems. CoRR http:\/\/arxiv.org\/abs\/1905.12524 (2019)","DOI":"10.1007\/978-3-030-29436-6_23"},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219\u2013234. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_16"},{"key":"23_CR34","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"},{"issue":"4","key":"23_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-4(4:1)2008","volume":"4","author":"V Sofronie-Stokkermans","year":"2008","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods Comput. Sci. 4(4), 1\u201331 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"23_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14203-1_15","volume-title":"Automated Reasoning","author":"V Sofronie-Stokkermans","year":"2010","unstructured":"Sofronie-Stokkermans, V.: Hierarchical reasoning for the verification of parametric systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 171\u2013187. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_15"},{"key":"23_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-38574-2_25","volume-title":"Automated Deduction \u2013 CADE-24","author":"V Sofronie-Stokkermans","year":"2013","unstructured":"Sofronie-Stokkermans, V.: Hierarchical reasoning and model generation for the verification of parametric hybrid systems. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 360\u2013376. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_25"},{"key":"23_CR38","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"},{"issue":"3","key":"23_CR39","first-page":"1","volume":"14","author":"V Sofronie-Stokkermans","year":"2018","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Logical Methods Comput. Sci. 14(3), 1\u201341 (2018)","journal-title":"Logical Methods Comput. Sci."},{"key":"23_CR40","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"}],"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_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:56:10Z","timestamp":1657576570000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_23","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":"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"}}]}}