{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T12:41:11Z","timestamp":1794487271536,"version":"4.9.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_14","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T15:11:50Z","timestamp":1414163510000},"page":"185-200","source":"Crossref","is-referenced-by-count":7,"title":["Extensional Crisis and Proving Identity"],"prefix":"10.1007","author":[{"given":"Ashutosh","family":"Gupta","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernhard","family":"Kragl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Experimental results of this paper, \n                  \n                    http:\/\/vprover.org\/extres"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New Results on Rewrite-Based Satisfiability Procedures. ACM Trans. Comput. Log.\u00a010(1) (2009)","DOI":"10.1145\/1459010.1459014"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Handbook of Automated Reasoning, pp. 19\u201399. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"14_CR4","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.\u00a05, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"14_CR5","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.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"14_CR6","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), \n                  \n                    www.SMT-LIB.org"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","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, vol.\u00a07898, pp. 39\u201357. Springer, Heidelberg (2013)"},{"key":"14_CR8","unstructured":"Bledsoe, W.W., Boyer, R.S.: Computer Proofs of Limit Theorems. In: Proc. of IJCAI, pp. 586\u2013600 (1971)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"14_CR10","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"14_CR12","series-title":"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.\u00a04246, pp. 497\u2013511. Springer, Heidelberg (2006)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What Else Is Decidable about Integer Arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"key":"14_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"14_CR15","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.\u00a08044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 7, pp. 371\u2013443. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"14_CR17","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Proc. of ESCoR, pp. 18\u201333 (2006)"},{"issue":"1-2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited Resource Strategy in Resolution Theorem Proving. J. of Symbolic Computation\u00a036(1-2), 101\u2013115 (2003)","journal-title":"J. of Symbolic Computation"},{"key":"14_CR19","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-18 2012. LNCS, vol.\u00a07180, pp. 359\u2013374. Springer, Heidelberg (2012)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Schulz","year":"2013","unstructured":"Schulz, S.: System Description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"issue":"4","key":"14_CR21","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\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"14_CR22","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T03:13:59Z","timestamp":1559013239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_14","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}