{"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":1758053618811,"version":"3.44.0"},"publisher-location":"Cham","reference-count":27,"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>The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such properties can be partly captured by the natural density of the spectrum of the studied theories, which is the set of sizes of their finite models. This enriches the toolbox of the theory combination researcher, by providing new tools to determine the possibility of combining theories. It also reveals interesting and surprising connections between theory combination and number theory.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_10","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:49Z","timestamp":1757887429000},"page":"169-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Number Theory Combination: Natural Density and\u00a0SMT"],"prefix":"10.1007","author":[{"given":"Guilherme","family":"V. Toledo","sequence":"first","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":"10_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). http:\/\/smt-lib.org"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, chap. 33, pp. 825\u2013885. IOS Press (2021). http:\/\/www.cs.stanford.edu\/~barrett\/pubs\/BSST21.pdf","DOI":"10.3233\/FAIA201017"},{"key":"10_CR3","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1090\/conm\/558\/11049","volume":"558","author":"J Bell","year":"2011","unstructured":"Bell, J., Burris, S.: Compton\u2019s method for proving logical limit laws. Contemp. Math. 558, 97\u2013128 (2011)","journal-title":"Contemp. Math."},{"key":"10_CR4","unstructured":"Carnap, R.: Logical Foundations of Probability. Chicago University of Chicago Press, Chicago (1950)"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/0168-0072(87)90017-0","volume":"36","author":"KJ Compton","year":"1987","unstructured":"Compton, K.J., Henson, C.W., Shelah, S.: Nonconvergence, undecidability, and intractability in asymptotic problems. Ann. Pure Appl. Log. 36, 207\u2013224 (1987). https:\/\/doi.org\/10.1016\/0168-0072(87)90017-0","journal-title":"Ann. Pure Appl. Log."},{"key":"10_CR6","unstructured":"de\u00a0Toledo, G.V., Zohar, Y.: Combining combination properties: minimal models (2024). http:\/\/arxiv.org\/abs\/2405.01478"},{"issue":"1","key":"10_CR7","doi-asserted-by":"crossref","first-page":"50","DOI":"10.2307\/2272945","volume":"41","author":"R Fagin","year":"1976","unstructured":"Fagin, R.: Probabilities on finite models. J. Symb. Log. 41(1), 50\u201358 (1976)","journal-title":"J. Symb. Log."},{"key":"10_CR8","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":"10_CR9","first-page":"17","volume":"5","author":"YV Glebskii","year":"1969","unstructured":"Glebskii, Y.V., Kogan, D.I., Liogon\u2019kii, M.I., Talanov, V.A.: Volume and fraction of satisfiability of formulas of the lower predicate calculus. Kibernetica (Kiev) 5, 17\u201327 (1969)","journal-title":"Kibernetica (Kiev)"},{"key":"10_CR10","unstructured":"Immerman, N.: Descriptive Complexity. Texts in Computer Science, 1999th edn. Springer, New York (1998)"},{"key":"10_CR11","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"},{"issue":"2","key":"10_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."},{"issue":"3","key":"10_CR13","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. Bell Syst. Tech. J. 41(3), 877\u2013884 (1962). https:\/\/doi.org\/10.1002\/j.1538-7305.1962.tb00480.x","journal-title":"Bell Syst. Tech. J."},{"key":"10_CR14","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, 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":"10_CR15","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.: Polite combination of algebraic datatypes. J. Autom. Reason. 66(3), 331\u2013355 (2022). https:\/\/doi.org\/10.1007\/s10817-022-09625-3","journal-title":"J. Autom. Reason."},{"key":"10_CR16","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":"10_CR17","unstructured":"Smullyan, R.R.: First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete. 2. Folge. Springer, Heidelberg (2012). https:\/\/books.google.com.br\/books?id=ZyLyCAAAQBAJ"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"199","DOI":"10.4064\/aa-27-1-199-245","volume":"27","author":"E Szemer\u00e9di","year":"1975","unstructured":"Szemer\u00e9di, E.: On sets of integers containing k elements in arithmetic progression. Acta Arithm. 27, 199\u2013245 (1975). https:\/\/doi.org\/10.4064\/aa-27-1-199-245","journal-title":"Acta Arithm."},{"key":"10_CR19","unstructured":"Tenenbaum, G.: Introduction to Analytic and Probabilistic Number Theory. Cambridge Studies in Advanced Mathematics, vol. 46. Cambridge University Press, Cambridge (1995). Transl. from the 2nd French ed. by C.B. Thomas"},{"issue":"3","key":"10_CR20","doi-asserted-by":"crossref","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."},{"issue":"3","key":"10_CR21","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). https:\/\/doi.org\/10.1007\/s10817-005-5204-9","journal-title":"J. Autom. Reason."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Toledo, G., Zohar, Y., Barrett, C.: Combining finite combination properties: finite models and busy beavers (2023). http:\/\/arxiv.org\/abs\/2307.07885","DOI":"10.1007\/978-3-031-43369-6_9"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Toledo, G.V., Zohar, Y.: Combining combination properties: minimal models. In: Bjorner, N., Heule, M., Voronkov, A. (eds.) Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 100, pp. 19\u201335. EasyChair (2024). https:\/\/easychair.org\/publications\/paper\/9KKC, https:\/\/doi.org\/10.29007\/6qkh","DOI":"10.29007\/6qkh"},{"key":"10_CR24","unstructured":"Toledo, G.V., Zohar, Y.: Number theory combination: natural density and SMT (2025). http:\/\/arxiv.org\/abs\/2505.16840"},{"key":"10_CR25","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-031-38499-8_30"},{"key":"10_CR26","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-031-43369-6_9"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Turing, A.M.: On computable numbers, with an application to the entscheidungsproblem. Proc. London Math. Soc. s2-42(1)2, 30\u2013265 (1937). https:\/\/londmathsoc.onlinelibrary.wiley.com\/doi\/abs\/10.1112\/plms\/s2-42.1.230, http:\/\/arxiv.org\/abs\/https:\/\/londmathsoc.onlinelibrary.wiley.com\/doi\/pdf\/10.1112\/plms\/s2-42.1.230, https:\/\/doi.org\/10.1112\/plms\/s2-42.1.230","DOI":"10.1112\/plms\/s2-42.1.230"}],"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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:52Z","timestamp":1757887432000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_10","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"}}]}}