{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T00:19:21Z","timestamp":1787530761911,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030510732","type":"print"},{"value":"9783030510749","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-51074-9_11","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T22:02:47Z","timestamp":1593468167000},"page":"181-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Combined Covers and Beth Definability"],"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":[[2020,6,24]]},"reference":[{"issue":"1","key":"11_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":"11_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\u20135:34 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"11_CR3","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":"11_CR4","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability (extended version). Technical report arXiv:1911.07774, arXiv.org (2019)","DOI":"10.1007\/978-3-030-51074-9_11"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-030-26619-6_12","volume-title":"Business Process Management","author":"D Calvanese","year":"2019","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: Hildebrandt, T., van Dongen, B.F., R\u00f6glinger, M., Mendling, J. (eds.) BPM 2019. LNCS, vol. 11675, pp. 157\u2013175. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-26619-6_12"},{"key":"11_CR6","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":"11_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-030-29436-6_9","volume-title":"Automated Deduction \u2013 CADE 27","author":"D Calvanese","year":"2019","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 142\u2013160. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_9"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes: challenges and opportunities for automated reasoning. In: Proceedings of ARCADE, EPTCS, vol. 311 (2019)","DOI":"10.4204\/EPTCS.311.9"},{"issue":"3","key":"11_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."},{"key":"11_CR10","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"},{"issue":"3","key":"11_CR11","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":"11_CR12","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":"11_CR13","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":"11_CR14","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":"11_CR15","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Compactly representing uniform interpolants for EUF using (conditional) DAGS. Technical report arXiv:2002.09784, arXiv.org (2020)"},{"key":"11_CR16","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":"11_CR17","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-94-015-9936-8"},{"issue":"3","key":"11_CR18","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":"11_CR19","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. Logica 55(2), 259\u2013271 (1995)","journal-title":"Stud. Logica"},{"issue":"1","key":"11_CR20","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. Log. 88(1), 27\u201346 (1997)","journal-title":"Ann. Pure Appl. Log."},{"key":"11_CR21","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":"11_CR22","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)"},{"issue":"7","key":"11_CR23","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":"2","key":"11_CR24","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":"11_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-030-29436-6_23","volume-title":"Automated Deduction \u2013 CADE 27","author":"D Peuter","year":"2019","unstructured":"Peuter, D., Sofronie-Stokkermans, V.: On invariant synthesis for parametric systems. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 385\u2013405. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_23"},{"issue":"1","key":"11_CR26","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":"11_CR27","unstructured":"Segerberg, K.: An Essay in Classical Modal Logic. Filosofiska Studier, vol. 13. Uppsala Universitet (1971)"},{"key":"11_CR28","unstructured":"Shavrukov, V.: Subalgebras of diagonalizable algebras of theories containing arithmetic. Dissertationes Mathematicae, CCCXXIII (1993)"},{"issue":"3","key":"11_CR29","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":"11_CR30","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"},{"issue":"10","key":"11_CR31","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. Log. 168(10), 1927\u20131948 (2017)","journal-title":"Ann. Pure Appl. Log."},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Visser, A.: Uniform interpolation and layered bisimulation. In H\u00e1jek, P. (ed.) G\u00f6del 1996. Logical Foundations on Mathematics, Computer Science and Physics \u2013 Kurt G\u00f6del\u2019s Legacy. Springer, Heidelberg (1996)","DOI":"10.1007\/978-3-662-21963-8_9"},{"key":"11_CR33","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 Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51074-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T21:33:34Z","timestamp":1656797614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-51074-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510732","9783030510749"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51074-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}