{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:43Z","timestamp":1767928003248,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"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>Shininess and strong politeness are properties related to theory combination procedures. In a paper titled \u201cMany-sorted equivalence of shiny and strongly polite theories\u201d, Casal and Rasga proved that for decidable theories, these properties are equivalent. We refine their result by showing that: (i) shiny theories are always decidable, and therefore strongly polite; and (ii) there are (undecidable) strongly polite theories that are not shiny. This line of research is tightly related to a recent series of papers that have sought to classify all the relations between theory combination properties. We finally complete this project, resolving all of the remaining problems that were previously left open.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_8","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:24Z","timestamp":1757887404000},"page":"135-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Shininess, Strong Politeness, and\u00a0Unicorns"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Przybocki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guilherme","family":"V. Toledo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"8_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"8_CR3","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"},{"issue":"2","key":"8_CR4","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-017-9411-y","volume":"60","author":"F Casal","year":"2017","unstructured":"Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. 60(2), 221\u2013236 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9411-y","journal-title":"J. Autom. Reason."},{"issue":"4","key":"8_CR5","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"LE Dickson","year":"1913","unstructured":"Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math. 35(4), 413 (1913)","journal-title":"Amer. J. Math."},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning, pp. xx+681. Cambridge University Press, Cambridge (2009). https:\/\/doi.org\/10.1017\/CBO9780511576430. ISBN 978-0-521- 89957-4","DOI":"10.1017\/CBO9780511576430"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press (1993). https:\/\/doi.org\/10.1017\/CBO9780511551574","DOI":"10.1017\/CBO9780511551574"},{"key":"8_CR8","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":"8_CR9","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer (2016)","DOI":"10.1007\/978-3-662-50497-0"},{"key":"8_CR10","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 (1993)"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"Greg Nelson","year":"1979","unstructured":"Nelson, Greg, Oppen, Derek C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979). https:\/\/doi.org\/10.1145\/357073.357079. ISSN 0164-0925","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12(3), 291\u2013302 (1980). https:\/\/doi.org\/10.1016\/0304-3975(80)90059-6. ISSN 0304-3975","journal-title":"Theor. Comput. Sci."},{"key":"8_CR13","unstructured":"Przybocki, B., Toledo, G.V., Zohar, Y.: Shininess, strong politeness, and unicorns. arXiv: 2507.04445 [cs.LO] (2025)"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Przybocki, B., et al.: The nonexistence of unicorns and many- sorted L\u00f6wenheim-Skolem theorems. In: Platzer, A., et al. (eds.) FM 2024, Part I. LNCS, vol. 14933, pp. 658\u2013675. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_34","DOI":"10.1007\/978-3-031-71162-6_34"},{"key":"8_CR15","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"},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10817-022-09625-3","volume":"66","author":"Y Sheng","year":"2022","unstructured":"Sheng, Y., et al.: Polite combination of algebraic datatypes. J. Autom. Reason. 66(3), 331\u2013355 (2022)","journal-title":"J. Autom. Reason."},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Tent, K., Ziegle, M.:. A Course in Model Theory. Lecture Notes in Logic, vol. 40, pp. x+248. Association for Symbolic Logic\/Cambridge University Press, La Jolla\/Cambridge (2012). https:\/\/doi.org\/10.1017\/CBO9781139015417. ISBN 978-0-521-76324-0","DOI":"10.1017\/CBO9781139015417"},{"issue":"1","key":"8_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1022587501759","volume":"30","author":"C Tinelli","year":"2003","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1\u201331 (2003)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining Nonstably Infinite Theories. J. Autom. Reason. 34(3), 209\u2013238 (2005)","journal-title":"J. Autom. Reason."},{"key":"8_CR20","unstructured":"Toledo, G.V., Przybocki, B., Zohar, Y.: Being polite is not enough (and other limits of theory combination). Accepted to CADE- 30 (2025)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1007\/978-3-031-38499-8_30","volume-title":"Automated Deduction \u2013 CADE 29","author":"GV Toledo","year":"2023","unstructured":"Toledo, G.V., Zohar, Y., Barrett, C.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 522\u2013541. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_30"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-031-43369-6_9","volume-title":"Frontiers of Combining Systems","author":"GV Toledo","year":"2023","unstructured":"Toledo, G.V., Zohar, Y., Barrett, C.: Combining finite combination properties: finite models and busy beavers. In: Sattler, U., Suda, M. (eds.) FroCoS 2023. LNCS, vol. 14279, pp. 159\u2013175. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43369-6_9"},{"key":"8_CR23","unstructured":"de Toledo, G.V., Zohar, Y.: Combining combination properties: minimal models. In: Proceedings of LPAR 2024 (2024)"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:26Z","timestamp":1757887406000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_8","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"}}]}}