{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T23:48:40Z","timestamp":1791416920930,"version":"4.3.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642046162","type":"print"},{"value":"9783642046179","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04617-9_55","type":"book-chapter","created":{"date-parts":[[2009,9,15]],"date-time":"2009-09-15T06:55:02Z","timestamp":1252997702000},"page":"435-443","source":"Crossref","is-referenced-by-count":15,"title":["Comparing Unification Algorithms in First-Order Theorem Proving"],"prefix":"10.1007","author":[{"given":"Kry\u0161tof","family":"Hoder","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"55_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/BFb0020799","volume-title":"STACS 91","author":"L. Albert","year":"1991","unstructured":"Albert, L., Casas, R., Fages, F., Torrecillas, A., Zimmermann, P.: Average case analysis of unification algorithms. In: Jantzen, M., Choffrut, C. (eds.) STACS 1991. LNCS, vol.\u00a0480, pp. 196\u2013213. Springer, Heidelberg (1991)"},{"key":"55_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/3-540-59200-8_72","volume-title":"Rewriting Techniques and Applications","author":"J. Avenhaus","year":"1995","unstructured":"Avenhaus, J., Denzinger, J., Fuchs, M.: Discount: A system for distributed equational deduction. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 397\u2013402. Springer, Heidelberg (1995)"},{"key":"55_CR3","unstructured":"Corbin, J., Bidoit, M.: A rehabilitation of Robinson\u2019s unification algorithm. In: IFIP Congress, pp. 909\u2013914 (1983)"},{"issue":"2","key":"55_CR4","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0004-3702(88)90005-7","volume":"36","author":"G. Escalada-Imaz","year":"1988","unstructured":"Escalada-Imaz, G., Ghallab, M.: A practically efficient and almost linear unification algorithm. Artif. Intell.\u00a036(2), 249\u2013263 (1988)","journal-title":"Artif. Intell."},{"issue":"2","key":"55_CR5","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1016\/0022-0000(78)90046-6","volume":"16","author":"L.J. Guibas","year":"1978","unstructured":"Guibas, L.J., Szemer\u00e9di, E.: The analysis of double hashing. J. Comput. Syst. Sci.\u00a016(2), 226\u2013274 (1978)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"55_CR6","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T. Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: Waldmeister: High-performance equational deduction. Journal of Automated Reasoning\u00a018(2), 265\u2013270 (1997)","journal-title":"Journal of Automated Reasoning"},{"issue":"11","key":"55_CR7","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/368996.369025","volume":"5","author":"A.B. Kahn","year":"1962","unstructured":"Kahn, A.B.: Topological sorting of large networks. Commun. ACM\u00a05(11), 558\u2013562 (1962)","journal-title":"Commun. ACM"},{"issue":"2","key":"55_CR8","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst.\u00a04(2), 258\u2013282 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"55_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-45744-5_19","volume-title":"Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 257\u2013271. Springer, Heidelberg (2001)"},{"key":"55_CR10","first-page":"181","volume-title":"STOC 1976","author":"M.S. Paterson","year":"1976","unstructured":"Paterson, M.S., Wegman, M.N.: Linear unification. In: STOC 1976, pp. 181\u2013186. ACM, New York (1976)"},{"key":"55_CR11","doi-asserted-by":"crossref","unstructured":"Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853\u20131964 (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"issue":"2,3","key":"55_CR12","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun.\u00a015(2,3), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"1","key":"55_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"55_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/BFb0017173","volume-title":"Mathematical Foundations of Computer Science 1988","author":"P. Ruzicka","year":"1988","unstructured":"Ruzicka, P., Pr\u00edvara, I.: An almost linear robinson unification algorithm. In: Koubek, V., Janiga, L., Chytil, M.P. (eds.) MFCS 1988. LNCS, vol.\u00a0324, pp. 501\u2013511. Springer, Heidelberg (1988)"},{"key":"55_CR15","unstructured":"Schulz, S.: E \u2014 a brainiac theorem prover\u00a015(2-3), 111\u2013126 (2002)"},{"issue":"2","key":"55_CR16","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R.E. Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM\u00a022(2), 215\u2013225 (1975)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","KI 2009: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04617-9_55","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T11:54:11Z","timestamp":1558526051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04617-9_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642046162","9783642046179"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04617-9_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}