{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T08:11:50Z","timestamp":1790842310726,"version":"4.1.0"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030221010","type":"print"},{"value":"9783030221027","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-22102-7_10","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T08:21:26Z","timestamp":1561450886000},"page":"212-239","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["From Model Completeness to Verification of Data Aware Processes"],"prefix":"10.1007","author":[{"given":"Diego","family":"Calvanese","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Montali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rivkin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Aiswarya, C., Atig, M.F., Montali, M., Rezine, O.: Recency-bounded verification of dynamic database-driven systems. In: Proceedings of the PODS, pp. 195\u2013210 (2016)","DOI":"10.1145\/2902251.2902300"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-22438-6_4","volume-title":"Automated Deduction \u2013 CADE-23","author":"F Alberti","year":"2011","unstructured":"Alberti, F., Armando, A., Ranise, S.: ASASP: automated symbolic analysis of security policies. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 26\u201333. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_4"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-642-31424-7_49","volume-title":"Computer Aided Verification","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679\u2013685. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_49"},{"issue":"1","key":"10_CR4","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":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-15763-9_36","volume-title":"Distributed Computing","author":"F Alberti","year":"2010","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol. 6343, pp. 392\u2013394. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15763-9_36"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. J. Satisfiability Boolean Model. Comput. 8(1\/2), 29\u201361 (2012)","DOI":"10.3233\/SAT190087"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-11936-6_2","volume-title":"Automated Technology for Verification and Analysis","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18\u201323. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_2"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2017-1458","volume":"150","author":"F Alberti","year":"2017","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. Fundam. Inf. 150(1), 1\u201324 (2017)","journal-title":"Fundam. Inf."},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11559306_2","volume-title":"Frontiers of Combining Systems","author":"F Baader","year":"2005","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted structures and theories through adjoint functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 31\u201347. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_2"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11532231_21","volume-title":"Automated Deduction \u2013 CADE-20","author":"F Baader","year":"2005","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted theories. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 278\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_21"},{"issue":"2","key":"10_CR11","doi-asserted-by":"publisher","first-page":"535","DOI":"10.2178\/jsl\/1185803623","volume":"72","author":"F Baader","year":"2007","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted theories. J. Symbolic Logic 72(2), 535\u2013583 (2007)","journal-title":"J. Symbolic Logic"},{"issue":"10","key":"10_CR12","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":"10_CR13","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":"2","key":"10_CR14","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1006\/inco.2001.3118","volume":"178","author":"F Baader","year":"2002","unstructured":"Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Inf. Comput. 178(2), 346\u2013390 (2002)","journal-title":"Inf. Comput."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of relational data-centric dynamic systems with external services. In: Proceedings of the PODS, pp. 163\u2013174 (2013)","DOI":"10.1145\/2463664.2465221"},{"key":"10_CR16","unstructured":"Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proceedings of the KR (2012)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., Segoufin, L., Toru\u0144czyk, S.: Verification of database-driven systems via amalgamation. In: Proceedings of the PODS, pp. 63\u201374 (2013)","DOI":"10.1145\/2463664.2465228"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-319-66845-1_26","volume-title":"Integrated Formal Methods","author":"D Bruschi","year":"2017","unstructured":"Bruschi, D., Di Pasquale, A., Ghilardi, S., Lanzi, A., Pagani, E.: Formal verification of ARP (address resolution protocol) through SMT-based model checking - a case study. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 391\u2013406. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_26"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-28891-3_28","volume-title":"NASA Formal Methods","author":"R Bruttomesso","year":"2012","unstructured":"Bruttomesso, R., Carioni, A., Ghilardi, S., Ranise, S.: Automated analysis of parametric timing-based mutual exclusion algorithms. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 279\u2013294. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_28"},{"key":"10_CR20","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 the PODS, pp. 1\u201312 (2013)","DOI":"10.1145\/2463664.2467796"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/j.ic.2017.08.007","volume":"259","author":"D Calvanese","year":"2017","unstructured":"Calvanese, D., De Giacomo, G., Montali, M., Patrizi, F.: First-order mu-calculus over generic transition systems and applications to the situation calculus. Inf. Comput. 259, 328\u2013347 (2017)","journal-title":"Inf. Comput."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness for the verification of data-aware processes. Manuscript submitted for publication (2018)","DOI":"10.1007\/978-3-030-22102-7_10"},{"key":"10_CR23","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Quantifier elimination for database driven verification. Technical report arXiv:1806.09686 , arXiv.org (2018)"},{"key":"10_CR24","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":"10_CR25","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the land of parametrized timed automata. In: Proceedings of the VERIFY. EPiC Series in Computing, vol. 3, pp. 47\u201364 (2010)"},{"key":"10_CR26","unstructured":"Chang, C.-C., Keisler, J.H.: Model Theory. North-Holland Publishing Co. (1990)"},{"key":"10_CR27","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"},{"issue":"3","key":"10_CR28","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2338626.2338628","volume":"37","author":"E Damaggio","year":"2012","unstructured":"Damaggio, E., Deutsch, A., Vianu, V.: Artifact systems with data dependencies and arithmetic. ACM TODS 37(3), 22 (2012)","journal-title":"ACM TODS"},{"issue":"4","key":"10_CR29","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1016\/j.is.2012.09.002","volume":"38","author":"E Damaggio","year":"2013","unstructured":"Damaggio, E., Hull, R., Vacul\u00edn, R.: On the equivalence of incremental and fixpoint semantics for business artifacts with Guard-Stage-Milestone lifecycles. Inf. Syst. 38(4), 561\u2013584 (2013)","journal-title":"Inf. Syst."},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Computer Science Logic","author":"G Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A., Esparza, J.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 50\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48168-0_5"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proceedings of the ICDT, pp. 252\u2013267. ACM (2009)","DOI":"10.1145\/1514894.1514924"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Li, Y., Vianu, V.: Verification of hierarchical artifact systems. In: Proceedings of the PODS, pp. 179\u2013194 (2016)","DOI":"10.1145\/2902251.2902275"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-23737-9_2","volume-title":"Advances in Databases and Information Systems","author":"M Dumas","year":"2011","unstructured":"Dumas, M.: On the convergence of data and process engineering. In: Eder, J., Bielikova, M., Tjoa, A.M. (eds.) ADBIS 2011. LNCS, vol. 6909, pp. 19\u201326. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23737-9_2"},{"key":"10_CR34","unstructured":"Dutertre, B., De Moura, L.: The YICES SMT solver. Technical report, SRI International (2006)"},{"key":"10_CR35","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of the LICS, pp. 352\u2013359. IEEE Computer Society (1999)"},{"issue":"1\u20132","key":"10_CR36","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(01)00248-1","volume":"294","author":"C Fiorentini","year":"2003","unstructured":"Fiorentini, C., Ghilardi, S.: Combining word problems through rewriting in categories with products. TCS 294(1\u20132), 103\u2013149 (2003)","journal-title":"TCS"},{"issue":"3\u20134","key":"10_CR37","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. JAR 33(3\u20134), 221\u2013249 (2004)","journal-title":"JAR"},{"key":"10_CR38","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":"10_CR39","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. Logic 169(8), 731\u2013754 (2018)","journal-title":"Ann. Pure Appl. Logic"},{"key":"10_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-71070-7_6","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67\u201382. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_6"},{"key":"10_CR41","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"10_CR42","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":"10_CR43","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 the LICS, pp. 417\u2013426. ACM (2016)","DOI":"10.1145\/2933575.2933609"},{"issue":"1","key":"10_CR44","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. Symbolic Logic 82(1), 62\u201376 (2017)","journal-title":"J. Symbolic Logic"},{"key":"10_CR45","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":"10_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1152","DOI":"10.1007\/978-3-540-88873-4_17","volume-title":"On the Move to Meaningful Internet Systems: OTM 2008","author":"R Hull","year":"2008","unstructured":"Hull, R.: Artifact-centric business process models: brief survey of research results and challenges. In: Meersman, R., Tari, Z. (eds.) OTM 2008. LNCS, vol. 5332, pp. 1152\u20131163. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88873-4_17"},{"key":"10_CR47","first-page":"210","volume":"95","author":"JB Kruskal","year":"1960","unstructured":"Kruskal, J.B.: Well-quasi-ordering, the Tree Theorem, and Vazsonyi\u2019s conjecture. Trans. Amer. Math. Soc. 95, 210\u2013225 (1960)","journal-title":"Trans. Amer. Math. Soc."},{"issue":"2","key":"10_CR48","doi-asserted-by":"publisher","first-page":"19","DOI":"10.4018\/jismd.2011040102","volume":"2","author":"V K\u00fcnzle","year":"2011","unstructured":"K\u00fcnzle, V., Weber, B., Reichert, M.: Object-aware business processes: fundamental requirements and their support in existing approaches. Int. J. Inf. Syst. Model. Des. 2(2), 19\u201346 (2011)","journal-title":"Int. J. Inf. Syst. Model. Des."},{"issue":"1","key":"10_CR49","first-page":"1","volume":"156","author":"O Kutz","year":"2004","unstructured":"Kutz, O., Lutz, C., Wolter, F., Zakharyaschev, M.: E-connections of abstract description systems. AIJ 156(1), 1\u201373 (2004)","journal-title":"AIJ"},{"issue":"3","key":"10_CR50","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"},{"issue":"2","key":"10_CR51","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"10_CR52","doi-asserted-by":"publisher","first-page":"15","DOI":"10.4064\/cm-30-1-15-25","volume":"30","author":"D Pigozzi","year":"1974","unstructured":"Pigozzi, D.: The join of equational theories. Colloq. Math. 30, 15\u201325 (1974)","journal-title":"Colloq. Math."},{"key":"10_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-33606-5_2","volume-title":"On the Move to Meaningful Internet Systems: OTM 2012","author":"M Reichert","year":"2012","unstructured":"Reichert, M.: Process and data: two sides of the same coin? In: Meersman, R., et al. (eds.) OTM 2012. LNCS, vol. 7565, pp. 2\u201319. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33606-5_2"},{"key":"10_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-15618-2_3","volume-title":"Business Process Management","author":"C Richardson","year":"2010","unstructured":"Richardson, C.: Warning: don\u2019t assume your business processes use master data. In: Hull, R., Mendling, J., Tai, S. (eds.) BPM 2010. LNCS, vol. 6336, pp. 11\u201312. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15618-2_3"},{"key":"10_CR55","unstructured":"Robinson, A.: On the Metamathematics of Algebra. North-Holland (1951)"},{"key":"10_CR56","unstructured":"Robinson, A.: Introduction to model theory and to the metamathematics of algebra. In: Studies in Logic and the Foundations of Mathematics. North-Holland (1963)"},{"key":"10_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-40184-8_2","volume-title":"CONCUR 2013","author":"S Schmitz","year":"2013","unstructured":"Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 5\u201324. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_2"},{"key":"10_CR58","unstructured":"Silver, B.: BPMN Method and Style. 2nd edn. Cody-Cassidy (2011)"},{"key":"10_CR59","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":"10_CR60","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3) (2018)"},{"key":"10_CR61","series-title":"Applied Logic Series","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems","author":"C Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.: A new correctness proof of the nelson-oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. ALS, vol. 3, pp. 103\u2013119. Springer, Dordrecht (1996). https:\/\/doi.org\/10.1007\/978-94-009-0349-4_5"},{"key":"10_CR62","doi-asserted-by":"crossref","unstructured":"Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proceedings of the ICDT, pp. 1\u201313. ACM (2009)","DOI":"10.1145\/1514894.1514896"},{"key":"10_CR63","unstructured":"Wolter, f.: Fusions of modal logics revisited. In: Advances in Modal Logic. CSLI Lecture Notes, vol. 1, pp. 361\u2013379 (1996)"}],"container-title":["Lecture Notes in Computer Science","Description Logic, Theory Combination, and All That"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22102-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,30]],"date-time":"2019-11-30T06:15:28Z","timestamp":1575094528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22102-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030221010","9783030221027"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22102-7_10","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":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}