{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T20:01:08Z","timestamp":1760990468985},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,5,12]],"date-time":"2022-05-12T00:00:00Z","timestamp":1652313600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,5,12]],"date-time":"2022-05-12T00:00:00Z","timestamp":1652313600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as \u201ccovers\u201d) in first-order theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that covers may not exist in the combined theories, even in case combined quantifier-free interpolants do exist. However, we exhibit a cover transfer algorithm operating also in the non-convex case for special kinds of theory combinations; these combinations (called \u2018tame combinations\u2019) concern multi-sorted theories arising in many model-checking applications (in particular, the ones oriented to verification of data-aware processes).<\/jats:p>","DOI":"10.1007\/s10817-022-09627-1","type":"journal-article","created":{"date-parts":[[2022,5,12]],"date-time":"2022-05-12T09:05:25Z","timestamp":1652346325000},"page":"409-435","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Combination of Uniform Interpolants via Beth Definability"],"prefix":"10.1007","volume":"66","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":[[2022,5,12]]},"reference":[{"issue":"1","key":"9627_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11225-007-9021-5","volume":"85","author":"M B\u00edlkov\u00e1","year":"2007","unstructured":"B\u00edlkov\u00e1, M.: Uniform interpolation and propositional quantifiers in modal logics. Stud. Logica. 85(1), 1\u201331 (2007)","journal-title":"Stud. Logica."},{"issue":"1","key":"9627_CR2","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-5:34 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"9627_CR3","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Quantifier elimination for database driven verification. Technical Report arXiv:1806.09686 (2018)"},{"key":"9627_CR4","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: Proc. of BPM 2019, LNCS 11675, 157\u2013175 (2019). Springer","DOI":"10.1007\/978-3-030-26619-6_12"},{"key":"9627_CR5","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: From model completeness to verification of data aware processes. In: Description Logic, Theory Combination, and All That, LNCS 11560, 212\u2013239 (2019). Springer","DOI":"10.1007\/978-3-030-22102-7_10"},{"key":"9627_CR6","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Proc. of CADE 2019. LNCS (LNAI) 11716, 142\u2013160 (2019). Springer","DOI":"10.1007\/978-3-030-29436-6_9"},{"key":"9627_CR7","first-page":"53","volume":"311","author":"D Calvanese","year":"2019","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes: Challenges and opportunities for automated reasoning. Proc. ARCADE 2019 311, 53\u201358 (2019). (EPTCS)","journal-title":"Proc. ARCADE 2019"},{"key":"9627_CR8","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability. In: Proc. of IJCAR 2020, LNCS (LNAI), vol. 12166, pp. 181\u2013200. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_11"},{"issue":"3","key":"9627_CR9","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1017\/S0960129520000067","volume":"30","author":"D Calvanese","year":"2020","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: SMT-based verification of data-aware processes: A model-theoretic approach. Math. Struct. Comput. Sci. 30(3), 271\u2013313 (2020)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"7","key":"9627_CR10","doi-asserted-by":"publisher","first-page":"941","DOI":"10.1007\/s10817-021-09596-x","volume":"65","author":"D Calvanese","year":"2021","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, uniform interpolants and superposition calculus. J. Autom. Reason. 65(7), 941\u2013969 (2021)","journal-title":"J. Autom. Reason."},{"key":"9627_CR11","volume-title":"Model Theory","author":"CC Chang","year":"1990","unstructured":"Chang, C.C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland Publishing Co., Amsterdam (1990)","edition":"3"},{"key":"9627_CR12","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Machine Intelligence, vol.\u00a07, pp. 91\u2013100. Edinburgh University Press (1972)"},{"issue":"1","key":"9627_CR13","doi-asserted-by":"publisher","first-page":"310","DOI":"10.2307\/2586539","volume":"65","author":"G D\u2019Agostino","year":"2000","unstructured":"D\u2019Agostino, G., Hollenberg, M.: Logical questions concerning the mu-calculus: Interpolation. Lyndon and Los-Tarski. J. Symb. Log. 65(1), 310\u2013332 (2000)","journal-title":"J. Symb. Log."},{"key":"9627_CR14","doi-asserted-by":"crossref","unstructured":"de\u00a0Leoni, M., Felli, P., Montali, M.: Strategy Synthesis for Data-Aware Dynamic Systems with Multiple Actors. In: Proc. of KR 2020, pp. 315\u2013325 (2020)","DOI":"10.24963\/kr.2020\/32"},{"key":"9627_CR15","doi-asserted-by":"crossref","unstructured":"Felli, P., de\u00a0Leoni, M., Montali, M.: Soundness verification of decision-aware process models with variable-to-variable conditions. In: Proc. of ACSD 2019, pp. 82\u201391. IEEE (2019)","DOI":"10.1109\/ACSD.2019.00013"},{"issue":"3","key":"9627_CR16","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0168-0072(93)E0084-2","volume":"71","author":"S Ghilardi","year":"1995","unstructured":"Ghilardi, S.: An algebraic theory of normal forms. Ann. Pure Appl. Logic 71(3), 189\u2013245 (1995)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3\u20134","key":"9627_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":"9627_CR18","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Proc. of FroCoS 2017, LNCS (LNAI), vol. 10483, pp. 316\u2013332. Springer (2017)","DOI":"10.1007\/978-3-319-66167-4_18"},{"issue":"8","key":"9627_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. Logic 169(8), 731\u2013754 (2018)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"4","key":"9627_CR20","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. Log. Methods Comput. Sci. 6(4), 1\u20138 (2010)","journal-title":"Log. Methods Comput. Sci."},{"key":"9627_CR21","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Proc. of IJCAR 2010, LNCS (LNAI), vol. 6173, pp. 22\u201329. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"issue":"3","key":"9627_CR22","doi-asserted-by":"publisher","first-page":"911","DOI":"10.2307\/2275765","volume":"60","author":"S Ghilardi","year":"1995","unstructured":"Ghilardi, S., Zawadowski, M.W.: A sheaf representation and duality for finitely presenting heyting algebras. J. Symb. Log. 60(3), 911\u2013939 (1995)","journal-title":"J. Symb. Log."},{"issue":"2","key":"9627_CR23","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/BF01061237","volume":"55","author":"S Ghilardi","year":"1995","unstructured":"Ghilardi, S., Zawadowski, M.W.: Undefinability of propositional quantifiers in the modal system S4. Stud. Log. 55(2), 259\u2013271 (1995)","journal-title":"Stud. Log."},{"issue":"1","key":"9627_CR24","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S0168-0072(97)00012-2","volume":"88","author":"S Ghilardi","year":"1997","unstructured":"Ghilardi, S., Zawadowski, M.W.: Model completions, r-Heyting categories. Ann. Pure Appl. Logic 88(1), 27\u201346 (1997)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9627_CR25","volume-title":"Sheaves, games, and model completions, Trends in Logic-Studia Logica Library","author":"S Ghilardi","year":"2002","unstructured":"Ghilardi, S., Zawadowski, M.: Sheaves, games, and model completions, Trends in Logic-Studia Logica Library, vol. 14. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"9627_CR26","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Compactly representing uniform interpolants for EUF using (conditional) DAGS. Technical Report arXiv:2002.09784 (2020)"},{"key":"9627_CR27","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Computing uniform interpolants for EUF via (conditional) DAG-based compact representations. In: Proc. of CILC 2020, vol. 2710, pp. 67\u201381. CEUR Workshop Proceedings (2020)"},{"key":"9627_CR28","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri nets with parameterised data - modelling and verification. In: Proc. of BPM 2020, LNCS, vol. 12168, pp. 55\u201374. Springer (2020)","DOI":"10.1007\/978-3-030-58666-9_4"},{"key":"9627_CR29","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri net-based object-centric processes with read-only data. Inf. Syst. 107 (2022)","DOI":"10.1016\/j.is.2022.102011"},{"key":"9627_CR30","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Uniform interpolants in EUF: Algorithms using DAG\u2013representations. Log. Methods Comput. Sci. 18(2) (2022)","DOI":"10.46298\/lmcs-18(2:2)2022"},{"key":"9627_CR31","unstructured":"Gianola, A.: SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications. Ph.D. thesis, Free University of Bozen-Bolzano, Bolzano, Italy (2022)"},{"key":"9627_CR32","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Proc. of ESOP 2008, Held as Part of ETAPS 2008, LNCS, vol. 4960, pp. 193\u2013207. Springer (2008)","DOI":"10.1007\/978-3-540-78739-6_16"},{"key":"9627_CR33","unstructured":"Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proc. of SC-Square 2017, co-located with ISSAC 2017, vol. 1974. CEUR Workshop Proceedings (2017)"},{"issue":"7","key":"9627_CR34","doi-asserted-by":"publisher","first-page":"825","DOI":"10.1016\/j.apal.2019.02.004","volume":"170","author":"T Kowalski","year":"2019","unstructured":"Kowalski, T., Metcalfe, G.: Uniform interpolation and coherence. Ann. Pure Appl. Log. 170(7), 825\u2013841 (2019)","journal-title":"Ann. Pure Appl. Log."},{"issue":"5","key":"9627_CR35","first-page":"556","volume":"18","author":"LL Maksimova","year":"1979","unstructured":"Maksimova, L.L.: Interpolation theorems in modal logics and amalgamable varieties of topological Boolean algebras. Algebra i Logika 18(5), 556\u2013586 (1979)","journal-title":"Algebra i Logika"},{"issue":"2","key":"9627_CR36","first-page":"194","volume":"19","author":"LL Maksimova","year":"1980","unstructured":"Maksimova, L.L.: Interpolation theorems in modal logics. Sufficient conditions. Algebra i Logika 19(2), 194\u2013213 (1980)","journal-title":"Algebra i Logika"},{"key":"9627_CR37","doi-asserted-by":"crossref","unstructured":"Metcalfe, G., Reggio, L.: Model completions for universal classes of algebras: necessary and sufficient conditions. Technical Report arXiv:2102.01426v2 (2021)","DOI":"10.1017\/jsl.2022.1"},{"issue":"2","key":"9627_CR38","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 Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9627_CR39","doi-asserted-by":"crossref","unstructured":"Peuter, D., Sofronie-Stokkermans, V.: On invariant synthesis for parametric systems. In: Proc. of CADE 2019, LNCS, vol. 11716, pp. 385\u2013405. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_23"},{"issue":"1","key":"9627_CR40","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":"9627_CR41","unstructured":"Segerberg, K.: An Essay in Classical Modal Logic, Filosofiska Studier, vol.\u00a013. Uppsala Universitet (1971)"},{"key":"9627_CR42","unstructured":"Shavrukov, V.: Subalgebras of diagonalizable algebras of theories containing arithmetic. Dissertationes Mathematicae CCCXXIII (1993)"},{"issue":"3","key":"9627_CR43","first-page":"24","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), 24 (2018)","journal-title":"Log. Methods Comput. Sci."},{"key":"9627_CR44","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proc. of FroCoS 1996, pp. 103\u2013119 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"10","key":"9627_CR45","doi-asserted-by":"publisher","first-page":"1927","DOI":"10.1016\/j.apal.2017.05.001","volume":"168","author":"SJ van Gool","year":"2017","unstructured":"van Gool, S.J., Metcalfe, G., Tsinakis, C.: Uniform interpolation and compact congruences. Ann. Pure Appl. Logic 168(10), 1927\u20131948 (2017)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9627_CR46","doi-asserted-by":"crossref","unstructured":"Visser, A.: Uniform interpolation and layered bisimulation. In: P.\u00a0H\u00e1jek (ed.) G\u00f6del 96: Logical foundations on mathematics, computer science and physics \u2013 Kurt G\u00f6del\u2019s legacy. Springer Verlag (1996)","DOI":"10.1007\/978-3-662-21963-8_9"},{"key":"9627_CR47","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Proc. of CADE 2005, LNCS, vol. 3632, pp. 353\u2013368. Springer (2005)","DOI":"10.1007\/11532231_26"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09627-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09627-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09627-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T05:10:26Z","timestamp":1661490626000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09627-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,12]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["9627"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09627-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,12]]},"assertion":[{"value":"17 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 May 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 August 2022","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Missing Open Access funding information has been added in the Funding Note","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}