{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:51:46Z","timestamp":1781927506080,"version":"3.54.5"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031433689","type":"print"},{"value":"9783031433696","type":"electronic"}],"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,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"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>This work is a part of an ongoing effort to understand the relationships between properties used in theory combination. We here focus on including two properties that are related to shiny theories: the finite model property and stable finiteness. For any combination of properties, we consider the question of whether there exists a theory that exhibits it. When there is, we provide an example with the simplest possible signature. One particular class of interest includes theories with the finite model property that are not finitely witnessable. To construct such theories, we utilize the Busy Beaver function.<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_9","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"159-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Combining Finite Combination Properties: Finite Models and\u00a0Busy Beavers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6539-398X","authenticated-orcid":false,"given":"Guilherme V.","family":"Toledo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"issue":"2","key":"9_CR1","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)","journal-title":"J. Autom. Reason."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. Technical report TR2010-922, Department of Computer Science, New York University, January 2010","DOI":"10.1007\/978-3-642-16242-8_29"},{"key":"9_CR3","first-page":"247","volume":"40","author":"H Marxen","year":"1990","unstructured":"Marxen, H., Buntrock, J.: Attacking the busy beaver 5. Bull. EATCS 40, 247\u2013251 (1990)","journal-title":"Bull. EATCS"},{"issue":"2","key":"9_CR4","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."},{"issue":"3","key":"9_CR5","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1002\/j.1538-7305.1962.tb00480.x","volume":"41","author":"T Rad\u00f3","year":"1962","unstructured":"Rad\u00f3, T.: On non-computable functions. The Bell Syst. Techn. J. 41(3), 877\u2013884 (1962)","journal-title":"The Bell Syst. Techn. J."},{"key":"9_CR6","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"},{"issue":"3","key":"9_CR7","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10817-022-09625-3","volume":"66","author":"Y Sheng","year":"2022","unstructured":"Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Polite combination of algebraic datatypes. J. Autom. Reason. 66(3), 331\u2013355 (2022)","journal-title":"J. Autom. Reason."},{"key":"9_CR8","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 1928","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":"9_CR9","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.: Combining decision procedures for theories in sorted logics. Technical report 04\u201301, Department of Computer Science, The University of Iowa, February 2004","DOI":"10.1007\/978-3-540-30227-8_53"},{"key":"9_CR10","unstructured":"Toledo, G.V., Zohar, Y., Barrett, C.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. Accepted to CADE 2023 (2023). https:\/\/arxiv.org\/abs\/2305.02384"},{"key":"9_CR11","unstructured":"Toledo, G.V., Zohar, Y., Barrett, C.: Finite models and busy beavers, Combining finite combination properties (2023)"}],"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-031-43369-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:33:47Z","timestamp":1694702027000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","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":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}