{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T01:37:00Z","timestamp":1783561020841,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615118","type":"print"},{"value":"9783540686873","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_113","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:04Z","timestamp":1330293064000},"page":"553-567","source":"Crossref","is-referenced-by-count":4,"title":["Advanced indexing operations on substitution trees"],"prefix":"10.1007","author":[{"given":"Peter","family":"Graf","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"50_CR1","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF00881885","volume":"12","author":"R. Butler","year":"1994","unstructured":"R. Butler and R. Overbeek. Formula databases for high-performance resolution\/paramodulation systems. Journal of Automated Reasoning, 12:139\u2013156, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"50_CR2","volume-title":"Computer Science and Applied Mathematics","author":"C.L. Chang","year":"1973","unstructured":"C.L. Chang and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science and Applied Mathematics. Academic Press, New York, New York, 1973."},{"key":"50_CR3","first-page":"117","volume":"914","author":"P. Graf","year":"1995","unstructured":"P. Graf. Substitution tree indexing. In 6th International Conference on Rewriting Techniques and Applications RTA-95, pages 117\u2013131. Springer LNCS 914, 1995.","journal-title":"Springer LNCS"},{"key":"50_CR4","doi-asserted-by":"crossref","unstructured":"P. Graf. Term Indexing. Springer LNAI 1053, 1996.","DOI":"10.1007\/3-540-61040-5"},{"key":"50_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","volume":"2","author":"J.D. McCharen","year":"1976","unstructured":"J.D. McCharen, R. Overbeek, and L. Wos. Complexity and related enhancements for automated theorem-proving programs. Computers and Mathematics with Applications, 2:1\u201316, 1976.","journal-title":"Computers and Mathematics with Applications"},{"issue":"2","key":"50_CR6","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"W. McCune. Experiments with discrimination-tree indexing and path-indexing for term retrieval. Journal of Automated Reasoning, 9(2):147\u2013167, October 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"50_CR7","volume-title":"Diploma thesis","author":"C. Meyer","year":"1996","unstructured":"C. Meyer. Parallel Unit Resulting Resolution. Diploma thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, 1996. http:\/\/www.mpi-sb.mpg.de\/papers\/masters_theses\/meyer.ps.gz."},{"key":"50_CR8","first-page":"479","volume-title":"Abstraction tree indexing for terms","author":"H.J. Ohlbach","year":"1990","unstructured":"H.J. Ohlbach. Abstraction tree indexing for terms. In Proceedings of the 9th European Conference on Artificial Intelligence, pages 479\u2013484. Pitman Publishing, London, August 1990."},{"key":"50_CR9","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. Automated deduction with hyper-resolution. International Journal of Comp. Mathematics, 1:227\u2013234, 1965.","journal-title":"International Journal of Comp. Mathematics"},{"issue":"1","key":"50_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A.Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, 1965.","journal-title":"Journal of the ACM"},{"issue":"2","key":"50_CR11","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BF00245457","volume":"9","author":"L. Wos","year":"1992","unstructured":"L. Wos. Note on McCune's article on discrimination trees. Journal of Automated Reasoning, 9(2):145\u2013146, 1992.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_113.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:14Z","timestamp":1605647234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_113"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_113","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}