{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:02Z","timestamp":1749125402384,"version":"3.41.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,4]]},"DOI":"10.1023\/a:1005992522805","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"5-25","source":"Crossref","is-referenced-by-count":2,"title":["An Algorithm for the Retrieval of Unifiers from Discrimination Trees"],"prefix":"10.1007","volume":"20","author":[{"given":"Hans","family":"de Nivelle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"146974_CR1","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.-L. Chang","year":"1973","unstructured":"Chang, C.-L. and Lee, R. C.-T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"146974_CR2","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF00881866","volume":"10","author":"J. Christian","year":"1993","unstructured":"Christian, J.: Flatterms, discrimination nets, and fast term rewriting, J. Automated Reasoning\n10 (1993), 95\u2013113.","journal-title":"J. Automated Reasoning"},{"key":"146974_CR3","doi-asserted-by":"crossref","unstructured":"Gottlob, G. and Leitsch, A.: Fast subsumption algorithms, Proc. EUROCAL'85, LNCS 204, 1985, pp. 64\u201377.","DOI":"10.1007\/3-540-15984-3_239"},{"key":"146974_CR4","doi-asserted-by":"crossref","unstructured":"Graf, P.: Extended path-indexing, Alan Bundy (ed.), Proc. CADE 12, 1994, pp. 514\u2013528.","DOI":"10.1007\/3-540-58156-1_37"},{"issue":"1","key":"146974_CR5","first-page":"398","volume":"23","author":"W. H. Joyner","year":"1976","unstructured":"Joyner, W. H.: Resolution strategies as decision procedures, ACM\n23(1) (1976), 398\u2013417.","journal-title":"ACM"},{"key":"146974_CR6","unstructured":"Kowalski, R. and Hayes, P. J.: Semantic trees in automated theorem proving, B. Meltzer and D. Michie (eds), Machine Intelligence 4, 1969."},{"key":"146974_CR7","volume-title":"Automated Theorem Proving, A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.: Automated Theorem Proving, A Logical Basis, North-Holland Publishing Company, Amsterdam, 1978."},{"key":"146974_CR8","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval, J. Automated Reasoning\n9 (1992), 147\u2013167.","journal-title":"J. Automated Reasoning"},{"key":"146974_CR9","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.0 Reference Manual and Guide + source, obtainable from info.mcs.anl.gov, 1994.","DOI":"10.2172\/10129052"},{"key":"146974_CR10","doi-asserted-by":"crossref","unstructured":"de Nivelle, H.: Resolution games and non-liftable resolution orderings, Proc. CSL'94, Springer-Verlag, 1994, pp. 279\u2013293.","DOI":"10.1007\/BFb0022263"},{"key":"146974_CR11","doi-asserted-by":"crossref","unstructured":"de Nivelle, H.: An algorithm for the retrieval of unifiers from discrimination trees, L. Pereira and Orlowska (eds), Proc. JELIA'96, 1996.","DOI":"10.1007\/3-540-61630-6_2"},{"issue":"2","key":"146974_CR12","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. S. Paterson","year":"1978","unstructured":"Paterson, M. S. and Wegman, M. N.: Linear unification, J. Comput. System Sci.\n16(2) (1978), 158\u2013167.","journal-title":"J. Comput. System Sci."},{"key":"146974_CR13","first-page":"23","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A machine oriented logic based on the resolution principle, ACM\n12 (1965), 23\u201341.","journal-title":"ACM"},{"key":"146974_CR14","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: Automated deduction with hyperresolution, Int. J. Computer Mathematics\n1 (1965), 227\u2013234.","journal-title":"Int. J. Computer Mathematics"},{"key":"146974_CR15","series-title":"Technical Note","doi-asserted-by":"crossref","DOI":"10.21236\/ADA460990","volume-title":"The path-indexing method for indexing terms","author":"M. Stickel","year":"1989","unstructured":"Stickel, M.: The path-indexing method for indexing terms, Technical Note 473, Artificial Intelligence Center SRI International, Menlo Park CA, 1989."},{"key":"146974_CR16","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00245457","volume":"9","author":"L. Wos","year":"1992","unstructured":"Wos, L.: A note on McCune's article on discrimination trees, J. Automated Reasoning\n9 (1992), 145\u2013146.","journal-title":"J. Automated Reasoning"},{"key":"146974_CR17","first-page":"5","volume":"128","author":"N. K. Zamov","year":"1972","unstructured":"Zamov, N. K.: On a bound for the complexity of terms in the resolution method, Trudy Mat. Inst. Steklov\n128 (1972), 5\u201313.","journal-title":"Trudy Mat. Inst. Steklov"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005992522805.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005992522805\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005992522805.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:38:52Z","timestamp":1749123532000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005992522805"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,4]]},"references-count":17,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1998,4]]}},"alternative-id":["146974"],"URL":"https:\/\/doi.org\/10.1023\/a:1005992522805","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,4]]}}}