{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:45:12Z","timestamp":1782873912553,"version":"3.54.5"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_15","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:51:41Z","timestamp":1776289901000},"page":"295-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Enumerating Choice Terms in Model-Based Quantifier Instantiation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-9875-2627","authenticated-orcid":false,"given":"Lydia","family":"Kondylidou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8367-0936","authenticated-orcid":false,"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"15_CR1","unstructured":"Andrews, B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, APLS, vol.\u00a027. Springer (2022)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. Journal of Automated Reasoning 47, 451\u2013479 (2011)","DOI":"10.1007\/s10817-011-9233-2"},{"key":"15_CR3","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Fishman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) CADE 2019. LNCS, vol. 11716, pp. 35\u201354. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for higher-order logic. Journal of Automated Reasoning 67 (2023)","DOI":"10.1007\/s10817-022-09649-9"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Suda, M.: A higher-order Vampire (short paper). In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024. LNCS, vol. 14739, pp. 75\u201385. Springer (2024)","DOI":"10.1007\/978-3-031-63498-7_5"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Bouton, T., de\u00a0Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 151\u2013156. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Bozec, T., Blanchette, J.: Iterative monomorphisation. In: Thiemann, R., Weidenbach, C. (eds.) FroCoS 2025. LNCS, vol. 15979, pp. 269\u2013286. Springer (2025)","DOI":"10.1007\/978-3-032-04167-8_15"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: An automatic higher-order prover. Journal of Automated Reasoning 7364, 111\u2013117 (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56\u201368 (1940)","DOI":"10.2307\/2266170"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Journal of the ACM 52(3), 365\u2013473 (2005)","DOI":"10.1145\/1066100.1066102"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Dross, C., Conchon, S., Paskevic, A.: Reasoning with triggers. In: Fontaine, P., Goel, A. (eds.) SMT 2012. EPiC Series in Computing, vol.\u00a020, pp. 22\u201331 (2012)","DOI":"10.29007\/3c1n"},{"key":"15_CR14","unstructured":"Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Annals of Mathematics and Artificial Intelligence 55(1-2), 101\u2013122 (2009)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C.: Introduction to the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) HOL 1991. pp.\u00a02\u20133. IEEE (1991)","DOI":"10.1109\/HOL.1991.596265"},{"key":"15_CR17","unstructured":"Hilbert, D., Ackermann, W.: Grundz\u00fcge der Theoretischen Logik, Grundlehren der mathematischen Wissenschaften, vol.\u00a027. Springer (1928)"},{"key":"15_CR18","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik I, Grundlehren der mathematischen Wissenschaften, vol.\u00a040. Springer (1934)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Kondylidou, L., Reynolds, A., Blanchette, J.: Augmenting model-based instantiation with fast enumeration. In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025. LNCS, vol. 15696, pp. 85\u2013103. Springer (2025)","DOI":"10.1007\/978-3-031-90643-5_5"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Kondylidou, L., Reynolds, A., Blanchette, J., Tinelli, C.: Artifact for paper \u201cEnumerating choice terms in model-based quantifier instantiation\u201d. In: TACAS 2026. Zenodo (2026), https:\/\/doi.org\/10.5281\/zenodo.18304537","DOI":"10.5281\/zenodo.18304537"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Kondylidou, L., Reynolds, A., Blanchette, J., Tinelli, C.: Enumerating choice terms in model-based quantifier instantiation [data set]. In: TACAS 2026. Zenodo (2026), https:\/\/doi.org\/10.5281\/zenodo.18212605","DOI":"10.5281\/zenodo.18212605"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 183\u2013198. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS, vol. 12699, pp. 625\u2013635. Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"15_CR25","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13965, pp. 3\u201317. Springer (2023)"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. Journal on Satisfiability, Boolean Modeling and Computation 9, 53\u201358 (2014)","DOI":"10.3233\/SAT190101"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Syntax-guided quantifier instantiation. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12652, pp. 145\u2013163. Springer (2021)","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol.\u00a02283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Defining functions on equivalence classes. In: Guruswami, V., Glazener, T. (eds.) CoRR 2019. vol.\u00a07, pp. 658\u2013675. Association for Computing Machinery (2019)","DOI":"10.1145\/1183278.1183280"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D. (ed.) TACAS 2018. LNCS, vol. 10806, pp. 112\u2013131. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"15_CR31","unstructured":"Reynolds, A., Barbosa, H., N\u00d6tzli, A., Barrett, C.W., Tinelli, C.: cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019, Part II. LNCS, vol. 11562, pp. 74\u201383. Springer (2019)"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol.\u00a09706, pp. 133\u2013151. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_10"},{"key":"15_CR33","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol.\u00a09207, pp. 198\u2013216. Springer (2015)"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 640\u2013655. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_42"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de\u00a0Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD 2014. pp. 195\u2013202. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"15_CR36","unstructured":"Rocq Development Team: Rocq Prover. https:\/\/zenodo.org\/records\/15149629 (2025), Zenodo"},{"key":"15_CR37","unstructured":"Simpson, S.G.: The epsilon calculus and conservative extensions. Notre Dame Journal of Formal Logic 25(3), 193\u2013202 (1984)"},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"Steen, A.: Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III. Ph.D. thesis, Freie Universit\u00e4t Berlin (2020)","DOI":"10.1007\/s13218-019-00628-8"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure\u2014from CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59, 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"15_CR40","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. Journal of Automated Reasoning 66, 541\u2013564 (2022)","DOI":"10.1007\/s10817-021-09613-z"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:02:54Z","timestamp":1782871374000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}