{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:07:10Z","timestamp":1784844430425,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319899596","type":"print"},{"value":"9783319899602","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-89960-2_1","type":"book-chapter","created":{"date-parts":[[2018,4,11]],"date-time":"2018-04-11T14:14:43Z","timestamp":1523456083000},"page":"3-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,12]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-75560-9_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Akbarpour","year":"2007","unstructured":"Akbarpour, B., Paulson, L.C.: Extending a resolution prover for inequalities on elementary functions. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 47\u201361. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_6"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84\u201399. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"1_CR5","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.SMT-LIB.org"},{"key":"1_CR6","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-21401-6_25","volume-title":"Automated Deduction - CADE-25","author":"P Baumgartner","year":"2015","unstructured":"Baumgartner, P., Bax, J., Waldmann, U.: Beagle \u2013 a hierarchic superposition theorem prover. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 367\u2013377. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_25"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic Superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3"},{"issue":"2","key":"1_CR8","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR9","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":"1_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-71070-7_40","volume-title":"Automated Reasoning","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Engineering DPLL(T) + Saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475\u2013490. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_40"},{"key":"1_CR11","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":"1_CR12","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":"1_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497\u2013511. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_34"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Rewriting Techniques and Applications","author":"P Graf","year":"1995","unstructured":"Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117\u2013131. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59200-8_52"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-40229-1_22","volume-title":"Automated Reasoning","author":"K Hoder","year":"2016","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 313\u2013329. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_22"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223\u2013237. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 260\u2013270. ACM (2017)","DOI":"10.1145\/3009837.3009887"},{"key":"1_CR18","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"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"A Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 335\u2013367. Elsevier and MIT Press, Cambridge (2001)"},{"key":"1_CR20","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Proceedings of the FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, vol. 192, CEUR Workshop Proceedings, pp. 19\u201333 (2006)"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Reger, G., Bj\u00f8rner, N., Suda, M., Voronkov, A.: AVATAR modulo theories. In: 2nd Global Conference on Artificial Intelligence, GCAI 2016, EPiC Series in Computing, vol. 41, pp. 39\u201352. EasyChair (2016)","DOI":"10.29007\/k6tp"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M.: Set of support for theory reasoning. In: IWIL Workshop and LPAR Short Presentations, Kalpa Publications in Computing, vol. 1, pp. 124\u2013134. EasyChair (2017)","DOI":"10.29007\/ndjg"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-319-21401-6_28","volume-title":"Automated Deduction \u2013 CADE-25","author":"G Reger","year":"2015","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 399\u2013415. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_28"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: The challenges of evaluating a new feature in vampire. In: Proceedings of the 1st and 2nd Vampire Workshops, EPiC Series in Computing, vol. 38, pp. 70\u201374. EasyChair (2016)","DOI":"10.29007\/1ffk"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: 2nd Global Conference on Artificial Intelligence, GCAI 2016, EPiC Series in Computing, vol. 41, pp. 11\u201323. EasyChair (2016)","DOI":"10.29007\/dzfz"},{"key":"1_CR26","unstructured":"Reger, G., Suda, M., Voronkov, A.: Instantiation and pretending to be an SMT solver with Vampire. In: Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, CEUR Workshop Proceedings, vol. 1889, pp. 63\u201375 (2017)"},{"key":"1_CR27","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 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 195\u2013202 (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-28717-6_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2012","unstructured":"R\u00fcmmer, P.: E-matching with free variables. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 359\u2013374. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_28"},{"key":"1_CR30","doi-asserted-by":"publisher","first-page":"1853","DOI":"10.1016\/B978-044450813-3\/50028-X","volume-title":"Handbook of Automated Reasoning","author":"R Sekar","year":"2001","unstructured":"Sekar, R., Ramakrishnan, I., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 1853\u20131964. Elsevier Science, Amsterdam (2001). Chap. 26"},{"issue":"4","key":"1_CR31","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"ME Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. J. Autom. Reasoning 1(4), 333\u2013355 (1985)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Suda, M., Reger, G., Voronkov, A.: Unification with abstraction and theory instantiation in saturation-based reasoning. EasyChair Preprint no. 1. EasyChair (2017). https:\/\/easychair.org\/publications\/preprint\/1","DOI":"10.29007\/hsh2"},{"issue":"4","key":"1_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"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"}],"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-89960-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T15:50:28Z","timestamp":1751557828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89960-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899596","9783319899602"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1","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":"12 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"}}]}}