{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:38Z","timestamp":1758053618942,"version":"3.44.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"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":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. We observe that decision procedures for the satisfiability of these theories rely on a kind of finite witnessability property. We use this insight to show the politeness of these theories with respect to the index and element sorts. Our results clarify the politeness of the theory of sets with the cardinality operator, which was left open in the literature.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_9","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:26Z","timestamp":1757887406000},"page":"153-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Polite Combination in\u00a0Parametric Array Theories"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0866-9257","authenticated-orcid":false,"given":"Rodrigo","family":"Raya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5937-6059","authenticated-orcid":false,"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s10703-017-0279-6","volume":"51","author":"F Alberti","year":"2017","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Design 51(3), 545\u2013574 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0279-6","journal-title":"Formal Methods Syst. Design"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Bansal, K., Barrett, C., Reynolds, A., Tinelli, C.: Reasoning with finite sets and cardinality constraints in SMT. Log. Methods Comput. Sci. 14(4) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(4:12)2018","DOI":"10.23638\/LMCS-14(4:12)2018"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-40229-1_7","volume-title":"Automated Reasoning","author":"K Bansal","year":"2016","unstructured":"Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 82\u201398. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_7"},{"issue":"1","key":"9_CR4","doi-asserted-by":"publisher","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S Feferman","year":"1959","unstructured":"Feferman, S., Vaught, R.: The first order properties of products of algebraic systems. Fundam. Math. 47(1), 57\u2013103 (1959)","journal-title":"Fundam. Math."},{"issue":"3","key":"9_CR5","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10817-020-09578-5","volume":"65","author":"S Ghilardi","year":"2020","unstructured":"Ghilardi, S., Pagani, E.: Higher-order quantifier elimination, counter simulations and fault-tolerant systems. J. Autom. Reason. 65(3), 425\u2013460 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09578-5","journal-title":"J. Autom. Reason."},{"key":"9_CR6","unstructured":"Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1993)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402\u2013416. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_29"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-73595-3_15","volume-title":"Automated Deduction \u2013 CADE-21","author":"V Kuncak","year":"2007","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215\u2013230. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_15"},{"issue":"1","key":"9_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2267454","volume":"17","author":"A Mostowski","year":"1952","unstructured":"Mostowski, A.: On direct products of theories. J. Symb. Log. 17(1), 1\u201331 (1952). https:\/\/doi.org\/10.2307\/2267454","journal-title":"J. Symb. Log."},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, pp. 45\u201352. IEEE, Austin (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2008.04.079","volume":"198","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. Electron. Notes Theor. Comput. Sci. 198(2), 37\u201349 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2008.04.079","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"9_CR12","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). https:\/\/doi.org\/10.1145\/357073.357079","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 218\u2013232. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_20"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_3"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. Rapport de recherche\u00a05678, INRIA (2005)","DOI":"10.1007\/11559306_3"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Raya, R., Kun\u010dak, V.: NP satisfiability for arrays as powers. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 301\u2013318. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_15","DOI":"10.1007\/978-3-030-94583-1_15"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"100978","DOI":"10.1016\/j.jlamp.2024.100978","volume":"140","author":"R Raya","year":"2024","unstructured":"Raya, R., Kun\u010dak, V.: Succinct ordering and aggregation constraints in algebraic array theories. J. Log. Algebraic Methods Program. 140, 100978 (2024). https:\/\/doi.org\/10.1016\/j.jlamp.2024.100978","journal-title":"J. Log. Algebraic Methods Program."},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Sheng, Y., et al.: Reasoning about vectors using an SMT theory of sequences. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 125\u2013143. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_9","DOI":"10.1007\/978-3-031-10769-6_9"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.: Polite combination of algebraic datatypes. J. Autom. Reason. 66(3), 331\u2013355 (2022). https:\/\/doi.org\/10.1007\/s10817-022-09625-3","DOI":"10.1007\/s10817-022-09625-3"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Stump, A., Barrett, C., Dill, D., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 29\u201337. IEEE Computer Society, Boston (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932480","DOI":"10.1109\/LICS.2001.932480"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-04222-5_23","volume-title":"Frontiers of Combining Systems","author":"T Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 366\u2013382. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_23"},{"issue":"1","key":"9_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-005-3075-8","volume":"34","author":"CG Zarba","year":"2005","unstructured":"Zarba, C.G.: Combining sets with cardinals. J. Autom. Reason. 34(1), 1\u201329 (2005). https:\/\/doi.org\/10.1007\/s10817-005-3075-8","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:27Z","timestamp":1757887407000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}