{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T15:40:55Z","timestamp":1766504455388,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theoretic properties in theory combination, namely stable infiniteness, smoothness, convexity, finite witnessability, and strong finite witnessability (and therefore politeness and strong politeness as well). All of our examples are sharp, in the sense that we also offer proofs that no theories are available within simpler signatures. This table significantly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory over a single sort that is polite but not strongly polite (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem showing that in order to apply polite theory combination, it is sufficient for one theory to be stably infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential to greatly simplify the process of showing which theories can be used in polite combination, as showing stable infiniteness is considerably simpler than showing smoothness.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_30","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"522-541","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Combining Combination Properties: An Analysis of\u00a0Stable Infiniteness, Convexity, and\u00a0Politeness"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6539-398X","authenticated-orcid":false,"given":"Guilherme V.","family":"Toledo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-45988-X_11","volume-title":"Frontiers of Combining Systems","author":"CW Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak\u2019s method for combining decision procedures. In: Armando, A. (ed.) FroCoS 2002. LNCS (LNAI), vol. 2309, pp. 132\u2013146. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45988-X_11"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-45221-5_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Casal","year":"2013","unstructured":"Casal, F., Rasga, J.: Revisiting the equivalence of shininess and politeness. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 198\u2013212. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_15"},{"issue":"2","key":"30_CR4","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-017-9411-y","volume":"60","author":"F Casal","year":"2018","unstructured":"Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. 60(2), 221\u2013236 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9411-y","journal-title":"J. Autom. Reason."},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-04222-5_16","volume-title":"Frontiers of Combining Systems","author":"P Fontaine","year":"2009","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 263\u2013278. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_16"},{"key":"30_CR6","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":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-540-71209-1_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 602\u2013617. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_47"},{"key":"30_CR8","series-title":"Wiley Professional Computing","volume-title":"Many-sorted Logic and its Applications","author":"M Monzano","year":"1993","unstructured":"Monzano, M.: Introduction to many-sorted logic. In: Meinke, K., Tucker, J.V. (eds.) Many-sorted Logic and its Applications. Wiley Professional Computing, Wiley, Hoboken (1993)"},{"issue":"2","key":"30_CR9","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":"30_CR10","doi-asserted-by":"publisher","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. https:\/\/hal.inria.fr\/inria-00000570","DOI":"10.1007\/11559306_3"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-030-79876-5_9","volume-title":"Automated Deduction \u2013 CADE 28","author":"Y Sheng","year":"2021","unstructured":"Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C., Tinelli, C.: Politeness and stable infiniteness: stronger together. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 148\u2013165. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_9"},{"key":"30_CR12","doi-asserted-by":"publisher","unstructured":"Tinelli, C., Zarba, C.: Combining decision procedures for theories in sorted logics. Technical report 04-01, Department of Computer Science, The University of Iowa (2004). https:\/\/doi.org\/10.1007\/978-3-540-30227-8_53","DOI":"10.1007\/978-3-540-30227-8_53"},{"key":"30_CR13","unstructured":"Toledo, G.V., Zohar, Y., Barrett, C.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. arXiv arXiv:2305.02384 (2023). https:\/\/arxiv.org\/abs\/2305.02384. Accepted to CADE 2023"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:06:31Z","timestamp":1693609591000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","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":"77","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":"28","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":"36% - 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","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":"6","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}