{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:53:33Z","timestamp":1781927613499,"version":"3.54.5"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T00:00:00Z","timestamp":1624233600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T00:00:00Z","timestamp":1624233600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100008815","name":"Libera Universit\u00e0 di Bolzano","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008815","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Uniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as \u201ccovers\u201d) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the <jats:sc>mcmt<\/jats:sc> tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.<\/jats:p>","DOI":"10.1007\/s10817-021-09596-x","type":"journal-article","created":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T09:03:00Z","timestamp":1624266180000},"page":"941-969","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Model Completeness, Uniform Interpolants and Superposition Calculus"],"prefix":"10.1007","volume":"65","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":[[2021,6,21]]},"reference":[{"key":"9596_CR1","doi-asserted-by":"crossref","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. pp. 1413\u20131452 (2006)","DOI":"10.1016\/j.ic.2005.05.009"},{"key":"9596_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, United Kingdom (1998)"},{"issue":"3","key":"9596_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":"9596_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":"9596_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":"9596_CR6","first-page":"39","volume":"7898","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. Proc. CADE LNCS (LNAI) 7898, 39\u201357 (2013)","journal-title":"Proc. CADE LNCS (LNAI)"},{"issue":"1","key":"9596_CR7","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. Studia Logica 85(1), 1\u201331 (2007)","journal-title":"Studia Logica"},{"key":"9596_CR8","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., Segoufin, L., Toru\u0144czyk, S.: Verification of database-driven systems via amalgamation. In: Proc. of PODS, pp. 63\u201374 (2013)","DOI":"10.1145\/2463664.2465228"},{"issue":"1","key":"9596_CR9","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":"9596_CR10","doi-asserted-by":"crossref","unstructured":"Calvanese, D., De\u00a0Giacomo, G., Montali, M.: Foundations of data aware process analysis: a database theory perspective. In: Proc. of PODS (2013)","DOI":"10.1145\/2463664.2467796"},{"key":"9596_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 (2018)"},{"key":"9596_CR12","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, LNCS, vol. 11675, pp. 157\u2013175. Springer (2019)","DOI":"10.1007\/978-3-030-26619-6_12"},{"key":"9596_CR13","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, vol. 11560, pp. 212\u2013239. Springer (2019)","DOI":"10.1007\/978-3-030-22102-7_10"},{"key":"9596_CR14","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Proc. of CADE, LNCS (LNAI), vol. 11716, pp. 142\u2013160. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_9"},{"key":"9596_CR15","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 the 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE), vol. 311. EPTCS (2019)","DOI":"10.4204\/EPTCS.311.9"},{"key":"9596_CR16","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability. In: Proc. of IJCAR, LNCS (LNAI), vol. 12166, pp. 181\u2013200. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_11"},{"issue":"3","key":"9596_CR17","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":"9596_CR18","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-London (1990)","edition":"3"},{"key":"9596_CR19","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems - tool paper. In: Proc. of CAV, pp. 718\u2013724 (2012)","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"9596_CR20","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proc. of ICDT, pp. 252\u2013267 (2009)","DOI":"10.1145\/1514894.1514924"},{"key":"9596_CR21","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Li, Y., Vianu, V.: Verification of hierarchical artifact systems. In: Proc. of PODS, pp. 179\u2013194. ACM Press (2016)","DOI":"10.1145\/2902251.2902275"},{"issue":"3","key":"9596_CR22","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":"9596_CR23","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":"9596_CR24","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Proc. of FroCoS, LNCS (LNAI), vol. 10483, pp. 316\u2013332. Springer (2017)","DOI":"10.1007\/978-3-319-66167-4_18"},{"issue":"8","key":"9596_CR25","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":"9596_CR26","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Compactly representing uniform interpolants for EUF using (conditional) DAGS. Technical Report arXiv:2002.09784 (2020)"},{"key":"9596_CR27","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Computing uniform interpolants for EUF via (conditional) DAG-based compact representations. In: Proc. of CILC, CEUR Workshop Proceedings, vol. 2710, pp. 67\u201381. CEUR-WS.org (2020)"},{"key":"9596_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, LNCS, vol. 12168, pp. 55\u201374. Springer (2020)","DOI":"10.1007\/978-3-030-58666-9_4"},{"key":"9596_CR29","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., van Gool, S.J.: Monadic second order logic as the model companion of temporal logic. In: Proc. of LICS, pp. 417\u2013426 (2016)","DOI":"10.1145\/2933575.2933609"},{"issue":"1","key":"9596_CR30","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":"9596_CR31","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. ACM Trans. Comput. Log. pp. 1\u201354 (2008)","DOI":"10.1145\/1342991.1342992"},{"key":"9596_CR32","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Proc. of IJCAR, LNCS (LNAI), vol. 6173, pp. 22\u201329. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"9596_CR33","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Zawadowski, M.: Sheaves, games, and model completions, Trends in Logic\u2014Studia Logica Library, vol.\u00a014. Kluwer Academic Publishers, Dordrecht (2002). A categorical approach to nonclassical propositional logics","DOI":"10.1007\/978-94-015-9936-8"},{"issue":"3","key":"9596_CR34","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":"9596_CR35","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. Studia Logica 55(2), 259\u2013271 (1995)","journal-title":"Studia Logica"},{"issue":"1","key":"9596_CR36","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":"9596_CR37","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Proc. of ESOP, Held as Part of ETAPS, pp. 193\u2013207 (2008)","DOI":"10.1007\/978-3-540-78739-6_16"},{"key":"9596_CR38","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Proc. of SAT, pp. 157\u2013171 (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"issue":"3","key":"9596_CR39","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":"9596_CR40","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Proc. of RTA, pp. 23\u201337 (1997)","DOI":"10.1007\/3-540-62950-5_59"},{"key":"9596_CR41","unstructured":"Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with ISSAC (2017)"},{"key":"9596_CR42","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Proc. of CADE, LNCS (LNAI), vol. 5663, pp. 199\u2013213. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_17"},{"issue":"7","key":"9596_CR43","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. Logic 170(7), 825\u2013841 (2019)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"9596_CR44","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":"9596_CR45","unstructured":"Lipparini, P.: Locally finite theories with model companion. In: Atti della Accademia Nazionale dei Lincei. Classe di Scienze Fisiche, Matematiche e Naturali. Rendiconti, Serie 8, vol.\u00a072. Accademia Nazionale dei Lincei (1982)"},{"key":"9596_CR46","doi-asserted-by":"crossref","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth\u2013Bendix ordering with lPO-like properties. In: Proc. of LPAR, pp. 348\u2013362 (2007)","DOI":"10.1007\/978-3-540-75560-9_26"},{"key":"9596_CR47","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. of CAV, pp. 123\u2013136 (2006)","DOI":"10.1007\/11817963_14"},{"issue":"2","key":"9596_CR48","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"9596_CR49","doi-asserted-by":"crossref","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Proc. of FroCoS, LNCS (LNAI), vol. 5749, pp. 319\u2013334. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_20"},{"key":"9596_CR50","doi-asserted-by":"crossref","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Proc. of TACAS, LNCS, vol. 5505, pp. 428\u2013442. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_35"},{"key":"9596_CR51","doi-asserted-by":"crossref","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fund. Inform. pp. 163\u2013187 (2010)","DOI":"10.3233\/FI-2010-362"},{"issue":"4","key":"9596_CR52","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"issue":"4","key":"9596_CR53","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":"9596_CR54","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning (in 2 volumes), pp. 371\u2013443. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"1","key":"9596_CR55","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":"9596_CR56","volume-title":"On the Metamathematics of Algebra. Studies in Logic and the Foundations of Mathematics","author":"A Robinson","year":"1951","unstructured":"Robinson, A.: On the Metamathematics of Algebra. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam (1951)"},{"key":"9596_CR57","unstructured":"Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003, Revised Papers, pp. 222\u2013237 (2003)"},{"key":"9596_CR58","unstructured":"Shavrukov, V.: Subalgebras of diagonalizable algebras of theories containing arithmetic. Dissertationes Mathematicae CCCXXIII (1993)"},{"key":"9596_CR59","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Proc. of IJCAR, LNCS (LNAI), vol. 9706, pp. 273\u2013289. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_19"},{"key":"9596_CR60","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3) (2018)"},{"key":"9596_CR61","doi-asserted-by":"crossref","unstructured":"Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proc. of ICDT, pp. 1\u201313 (2009)","DOI":"10.1145\/1514894.1514896"},{"issue":"10","key":"9596_CR62","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":"9596_CR63","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"},{"issue":"3\u20134","key":"9596_CR64","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. Israel J. Math. 25(3\u20134), 305\u2013330 (1976)","journal-title":"Israel J. Math."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09596-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09596-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09596-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T13:08:49Z","timestamp":1674565729000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09596-x"}},"subtitle":["(With Applications to Verification of Data-Aware Processes)"],"short-title":[],"issued":{"date-parts":[[2021,6,21]]},"references-count":64,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["9596"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09596-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,21]]},"assertion":[{"value":"15 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 June 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}