{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:22Z","timestamp":1776333382389,"version":"3.51.2"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319899626","type":"print"},{"value":"9783319899633","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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":[[2018]]},"DOI":"10.1007\/978-3-319-89963-3_7","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T18:53:00Z","timestamp":1523645580000},"page":"112-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Revisiting Enumerative Instantiation"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"7_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"Leo Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 19\u201399 (2001)"},{"key":"7_CR4","unstructured":"Barbosa, H.: New techniques for instantiation and proof production in SMT solving. Ph.D. thesis, Universit\u00e9 de Lorraine, Universidade Federal do Rio Grande do Norte (2017)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-662-54580-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2017","unstructured":"Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 214\u2013230. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_13"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M Barnett","year":"2008","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144\u2013152. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_16"},{"key":"7_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). www.SMT-LIB.org"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-22438-6_17","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 207\u2013221. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_17"},{"key":"7_CR9","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"issue":"7","key":"7_CR11","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"7_CR15","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"7_CR16","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, Burlington (2001)","edition":"2"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Symposium on Logic in Computer Science, p. 55 (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167\u2013182. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_12"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"PC Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory: its justification and realization. IBM J. Res. Dev. 4(1), 28\u201335 (1960)","journal-title":"IBM J. Res. Dev."},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Wendler, P.: figshare (2018). https:\/\/doi.org\/10.6084\/m9.figshare.5896615","DOI":"10.6084\/m9.figshare.5896615"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-40885-4_15","volume-title":"Frontiers of Combining Systems","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 214\u2013228. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_15"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"issue":"2","key":"7_CR24","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D Prawitz","year":"1960","unstructured":"Prawitz, D.: An improved proof procedure1. Theoria 26(2), 102\u2013139 (1960)","journal-title":"Theoria"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, A.: Conflicts, models and heuristics for quantifier instantiation in SMT. In: Kov\u00e1cs, L., Voronkov, A. (eds.) Vampire Workshop, EPiC Series in Computing, pp. 1\u201315. EasyChair (2016)","DOI":"10.29007\/jmd3"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-89963-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Andrew Reynolds","year":"2018","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. Technical report, University of Iowa, Inria (2018). https:\/\/hal.inria.fr\/hal-01744956"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation - Artifact (2018). figshare https:\/\/doi.org\/10.6084\/m9.figshare.5917384.v1","DOI":"10.6084\/m9.figshare.5917384.v1"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods In Computer-Aided Design (FMCAD), pp. 195\u2013202. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 377\u2013391. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_26"},{"issue":"1","key":"7_CR30","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"2,3","key":"7_CR31","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - A brainiac theorem prover. AI Commun. 15(2,3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"issue":"4","key":"7_CR33","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"7_CR34","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/aimag.v37i2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016)","journal-title":"AI Mag."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89963-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T17:29:10Z","timestamp":1751563750000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89963-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899626","9783319899633"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","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":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}