{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:13:22Z","timestamp":1743153202246,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"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_9","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"142-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Model Completeness, Covers and Superposition"],"prefix":"10.1007","author":[{"given":"Diego","family":"Calvanese","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[]},{"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Montali","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rivkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"issue":"10","key":"9_CR1","doi-asserted-by":"publisher","first-page":"1413","DOI":"10.1016\/j.ic.2005.05.009","volume":"204","author":"F Baader","year":"2006","unstructured":"Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Inf. Comput. 204(10), 1413\u20131452 (2006)","journal-title":"Inf. Comput."},{"key":"9_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"issue":"2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Inf. Comput. 121(2), 172\u2013192 (1995)","journal-title":"Inf. Comput."},{"key":"9_CR5","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":"9_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., Segoufin, L., Toru\u0144czyk, S.: Verification of database-driven systems via amalgamation. In: Proceedings of PODS, pp. 63\u201374 (2013)","DOI":"10.1145\/2463664.2465228"},{"issue":"1","key":"9_CR8","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":"9_CR9","doi-asserted-by":"crossref","unstructured":"Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data aware process analysis: a database theory perspective. In: Proceedings of PODS (2013)","DOI":"10.1145\/2463664.2467796"},{"key":"9_CR10","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Quantifier elimination for database driven verification. CoRR, abs\/1806.09686 (2018)"},{"key":"9_CR11","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes via array-based systems (extended version). Technical report arXiv:1806.11459, arXiv.org (2018)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-030-22102-7_10","volume-title":"Description Logic, Theory Combination, and All That","author":"D Calvanese","year":"2019","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: From model completeness to verification of data aware processes. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 212\u2013239. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22102-7_10"},{"key":"9_CR13","volume-title":"Model Theory","author":"C-C Chang","year":"1990","unstructured":"Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland Publishing Co., Amsterdam (1990)","edition":"3"},{"key":"9_CR14","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":"9_CR15","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proceedings of ICDT, pp. 252\u2013267 (2009)","DOI":"10.1145\/1514894.1514924"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Li, Y., Vianu, V.: Verification of hierarchical artifact systems. In: Proceedings of PODS, pp. 179\u2013194. ACM Press (2016)","DOI":"10.1145\/2902251.2902275"},{"issue":"3\u20134","key":"9_CR17","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S Ghilardi","year":"2004","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3\u20134), 221\u2013249 (2004)","journal-title":"J. Autom. Reason."},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-319-66167-4_18","volume-title":"Frontiers of Combining Systems","author":"S Ghilardi","year":"2017","unstructured":"Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 316\u2013332. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_18"},{"issue":"8","key":"9_CR19","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1016\/j.apal.2018.04.001","volume":"169","author":"S Ghilardi","year":"2018","unstructured":"Ghilardi, S., Gianola, A.: Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Log. 169(8), 731\u2013754 (2018)","journal-title":"Ann. Pure Appl. Log."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 54 p. (2008). Article no. 8","DOI":"10.1145\/1342991.1342992"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22\u201329. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_3"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., van Gool, S.J.: Monadic second order logic as the model companion of temporal logic. In: Proceedings of LICS, pp. 417\u2013426 (2016)","DOI":"10.1145\/2933575.2933609"},{"issue":"1","key":"9_CR23","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1017\/jsl.2016.70","volume":"82","author":"S Ghilardi","year":"2017","unstructured":"Ghilardi, S., van Gool, S.J.: A model-theoretic characterization of monadic second order logic on infinite words. J. Symb. Log. 82(1), 62\u201376 (2017)","journal-title":"J. Symb. Log."},{"key":"9_CR24","series-title":"Trends in Logic-Studia Logica Library","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9936-8","volume-title":"Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics","author":"S Ghilardi","year":"2002","unstructured":"Ghilardi, S., Zawadowski, M.: Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics. Trends in Logic-Studia Logica Library, vol. 14. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-78739-6_16","volume-title":"Programming Languages and Systems","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 193\u2013207. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78739-6_16"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"issue":"3","key":"9_CR27","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559\u2013587 (1991)","journal-title":"J. ACM"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23\u201337. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62950-5_59"},{"key":"9_CR29","unstructured":"Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation Co-Located with ISSAC (2017)"},{"key":"9_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"},{"issue":"3","key":"9_CR31","first-page":"283","volume":"11","author":"Y Li","year":"2017","unstructured":"Li, Y., Deutsch, A., Vianu, V.: VERIFAS: a practical verifier for artifact systems. PVLDB 11(3), 283\u2013296 (2017)","journal-title":"PVLDB"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-75560-9_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Ludwig","year":"2007","unstructured":"Ludwig, M., Waldmann, U.: An extension of the knuth-bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 348\u2013362. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_26"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-04222-5_20","volume-title":"Frontiers of Combining Systems","author":"E Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 319\u2013334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_20"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-00768-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 428\u2013442. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_35"},{"issue":"1\u20132","key":"9_CR36","doi-asserted-by":"publisher","first-page":"163","DOI":"10.3233\/FI-2010-362","volume":"105","author":"E Nicolini","year":"2010","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fundam. Inform. 105(1\u20132), 163\u2013187 (2010)","journal-title":"Fundam. Inform."},{"issue":"4","key":"9_CR37","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. J. Symb. Comput. 19(4), 321\u2013351 (1995)","journal-title":"J. Symb. Comput."},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, vol. 2, pp. 371\u2013443. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"1","key":"9_CR39","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2275175","volume":"57","author":"AM Pitts","year":"1992","unstructured":"Pitts, A.M.: On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log. 57(1), 33\u201352 (1992)","journal-title":"J. Symb. Log."},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-540-39866-0_24","volume-title":"Perspectives of System Informatics","author":"T Rybina","year":"2004","unstructured":"Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 222\u2013237. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-39866-0_24"},{"key":"9_CR41","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":"9_CR42","first-page":"1","volume":"14","author":"V Sofronie-Stokkermans","year":"2018","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3), 1\u201341 (2018)","journal-title":"Log. Methods Comput. Sci."},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proceedings of ICDT, pp. 1\u201313 (2009)","DOI":"10.1145\/1514894.1514896"},{"issue":"3\u20134","key":"9_CR44","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BF02757007","volume":"25","author":"WH Wheeler","year":"1976","unstructured":"Wheeler, W.H.: Model-companions and definability in existentially complete structures. Isr. J. Math. 25(3\u20134), 305\u2013330 (1976)","journal-title":"Isr. J. 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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:54:49Z","timestamp":1657576489000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_9","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"}}]}}