{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:49:37Z","timestamp":1743115777901,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_9","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"71-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Integrating Equational Reasoning into Instantiation-Based Theorem Proving"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[]},{"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"key":"9_CR1","first-page":"353","volume-title":"Automated Deduction \u2014 A Basis for Applications, ch. 11","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2014 A Basis for Applications, ch. 11, vol.\u00a0I, pp. 353\u2013397. Kluwer, Dordrecht (1998)"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 19\u2013100. Elsevier, Amsterdam (2001)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/10721959_16","volume-title":"Automated Deduction - CADE-17","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL \u2013 a first-order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 200\u2013219. Springer, Heidelberg (2000)"},{"key":"9_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The disconnection method: a confluent integration of unification in the analytic framework. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"issue":"6","key":"9_CR6","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. J. of Symbolic Computation\u00a013(6), 613\u2013641 (1992)","journal-title":"J. of Symbolic Computation"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: 16th Int. Conf. on Computer Aided Verification. LNCS (2004, To appear)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9_CR8","first-page":"55","volume-title":"Proc. 18th IEEE Symposium on Logic in Computer Science","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on Logic in Computer Science, pp. 55\u201364. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J.N. Hooker","year":"2002","unstructured":"Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first order logic. J. of Automated Reasoning\u00a028, 371\u2013396 (2002)","journal-title":"J. of Automated Reasoning"},{"issue":"3","key":"9_CR10","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Francaise d\u2019Intelligence Artificielle\u00a04(3), 9\u201352 (1990), Special issue on automated deduction","journal-title":"Revue Francaise d\u2019Intelligence Artificielle"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.J. Lee","year":"1992","unstructured":"Lee, S.J., Plaisted, D.: Eliminating duplication with the Hyper-linking strategy. J. of Automated Reasoning\u00a09, 25\u201342 (1992)","journal-title":"J. of Automated Reasoning"},{"key":"9_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 142\u2013156. Springer, Heidelberg (2001)"},{"key":"9_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45616-3_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 176\u2013190. Springer, Heidelberg (2002)"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D. Plaisted","year":"2000","unstructured":"Plaisted, D., Zhu, Y.: Ordered semantic hyper-linking. J. of Automated Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"J. of Automated Reasoning"},{"key":"9_CR16","unstructured":"Stenz, G.: The Disconnection Calculus. In: Logos, Dissertation, TU M\u00fcnchen (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T20:04:00Z","timestamp":1579723440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}