{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T03:06:05Z","timestamp":1648955165083},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,10,18]],"date-time":"2012-10-18T00:00:00Z","timestamp":1350518400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10817-012-9263-4","type":"journal-article","created":{"date-parts":[[2012,10,17]],"date-time":"2012-10-17T19:48:51Z","timestamp":1350503331000},"page":"325-356","source":"Crossref","is-referenced-by-count":0,"title":["SMELS: Satisfiability Modulo Equality with Lazy Superposition"],"prefix":"10.1007","volume":"51","author":[{"given":"Christopher","family":"Lynch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Quang-Trung","family":"Ta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Duc-Khanh","family":"Tran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,18]]},"reference":[{"issue":"2","key":"9263_CR1","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inform. J. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inform. J. Comput."},{"key":"9263_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, chap.\u00a02, pp.\u00a019\u2013100. The MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"9263_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Automated Deduction\u2014CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA. Lecture Notes in Computer Science, vol.\u00a0607, pp.\u00a0462\u2013476. Springer (1992)","DOI":"10.1007\/3-540-55602-8_185"},{"key":"9263_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907), Berlin, Germany. Lecture Notes in Computer Science, vol.\u00a04590, pp.\u00a0298\u2013302. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"9263_CR5","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1016\/j.artint.2007.09.005","volume":"172","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172, 591\u2013632 (2008)","journal-title":"Artif. Intell."},{"issue":"2","key":"9263_CR6","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/j.jsc.2008.10.008","volume":"45","author":"MP Bonacina","year":"2010","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. Symb. J. Comput. 45(2), 229\u2013260 (2010)","journal-title":"Symb. J. Comput."},{"issue":"3","key":"9263_CR7","doi-asserted-by":"crossref","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"},{"issue":"7","key":"9263_CR8","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9263_CR9","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Engineering dpll(t) + saturation. In: Automated Reasoning, 4th International Joint Conference, Sydney, Australia, 12\u20131 August 2008. Lecture Notes in Computer Science, vol. 5195, pp. 475\u2013490. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_40"},{"key":"9263_CR10","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: : An Efficient SMT Solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary. Lecture Notes in Computer Science, vol.\u00a04963, pp.\u00a0337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9263_CR11","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Press, I.C.S. (ed.) Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM\u201903) (2003)","DOI":"10.1109\/SEFM.2003.1236224"},{"key":"9263_CR12","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol.\u00a0B, chap.\u00a06, pp.\u00a0244\u2013320 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"9263_CR13","doi-asserted-by":"crossref","unstructured":"Deshane, T., Hu, W., Jablonski, P., Lin, H., Lynch, C., McGregor, R.E.: Encoding first order proofs in SAT. In: Proceedings Automated Deduction\u2014CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, 17\u201320 July 2007. Lecture Notes in Computer Science, vol.\u00a04603, pp.\u00a0476\u2013491. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_35"},{"issue":"3","key":"9263_CR14","doi-asserted-by":"crossref","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":"9263_CR15","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on Logic in Computer Science (LICS\u201903), pp.\u00a055\u201364. IEEE Computer Society Press (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"9263_CR16","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201904), Boston, Massachusetts. Lecture Notes in Computer Science, vol.\u00a03114, pp.\u00a0175\u2013188. Springer (2004). ftp:\/\/ftp.cs.uiowa.edu\/pub\/tinelli\/papers\/GanHNOT-CAV-04.pdf"},{"issue":"5","key":"9263_CR17","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"JN Hooker","year":"2002","unstructured":"Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first-order logic. J. Autom. Reasoning 28(5), 371\u2013396 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"9263_CR18","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Automating first-order relational logic. In: SIGSOFT FSE, pp. 130\u2013139 (2000)","DOI":"10.1145\/357474.355063"},{"key":"9263_CR19","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver\u2014an instantiation-based theorem prover for first-order logic (system description). In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, 12\u201315 August 2008, Proceedings. Lecture Notes in Computer Science, vol.\u00a05195, pp.\u00a0292\u2013298. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"9263_CR20","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Computer Science Logic (CSL\u201907). Lecture Notes in Computer Science, vol.\u00a04646, pp.\u00a0223\u2013237. Springer (2007)","DOI":"10.1007\/978-3-540-74915-8_19"},{"issue":"1","key":"9263_CR21","first-page":"25","volume":"9","author":"SJ Lee","year":"1992","unstructured":"Lee, S.J., Plaisted, D.A.: Eliminating duplication with the hyper-linking strategy. J. Autom. Reasoning 9(1), 25\u201342 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"9263_CR22","unstructured":"Lynch, C., McGregor, R.E.: Combining instance generation and resolution. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, 16\u201318 September 2009. Lecture Notes in Computer Science, vol.\u00a05749, pp.\u00a0304\u2013318. Springer (2009)"},{"issue":"7","key":"9263_CR23","doi-asserted-by":"crossref","first-page":"1026","DOI":"10.1016\/j.ic.2011.03.005","volume":"209","author":"C Lynch","year":"2011","unstructured":"Lynch, C., Ranise, S., Ringeissen, C., Tran, D.K.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026\u20131047 (2011)","journal-title":"Inf. Comput."},{"key":"9263_CR24","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Hand of Automated Reasoning. The MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"2","key":"9263_CR25","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"1","key":"9263_CR26","doi-asserted-by":"crossref","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":"9263_CR27","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E\u2013 a brainiac theorem prover. J. AI Commun. 15(2\/3), 111\u2013126 (2002)","journal-title":"J. AI Commun."},{"key":"9263_CR28","doi-asserted-by":"crossref","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with sat. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings, Copenhagen, Denmark, 27\u201331 July 2002. Lecture Notes in Computer Science, vol.\u00a02404, pp.\u00a0209\u2013222. Springer (2002)","DOI":"10.1007\/3-540-45657-0_16"},{"issue":"1","key":"9263_CR29","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/AIC-2010-0469","volume":"23","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The cade-22 automated theorem proving system competition\u2014CASC-22. AI Commun. 23(1), 47\u201359 (2010)","journal-title":"AI Commun."},{"issue":"2","key":"9263_CR30","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"14","author":"C Weidenbach","year":"1997","unstructured":"Weidenbach, C.: Spass version 0.49. J. Autom. Reasoning 14(2), 247\u2013252 (1997)","journal-title":"J. Autom. Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9263-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9263-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9263-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,30]],"date-time":"2022-01-30T09:48:50Z","timestamp":1643536130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9263-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,18]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["9263"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9263-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,18]]}}}