{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:28:49Z","timestamp":1784845729357,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540422549","type":"print"},{"value":"9783540457442","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_19","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"257-271","source":"Crossref","is-referenced-by-count":18,"title":["On the Evaluation of Indexing Techniques for Theorem Proving"],"prefix":"10.1007","author":[{"given":"Robert","family":"Nieuwenhuis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"Riazanov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"19_CR1","unstructured":"P. Cheeseman, B. Kanefsky, and W. M. Taylor. Where the really hard problems are. In R. Reiter J. Mylopoulos, editor, IJCAI 1991. Proceedings of the 12th International Joint Conference on Artificial Intelligence, pages 331\u2013340, Sydney, Australia, 1991. Morgan Kaufmann."},{"issue":"1","key":"19_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF00881866","volume":"10","author":"J. Christian","year":"1993","unstructured":"J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95\u2013113, February 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"H. Ganzinger, R. Nieuwenhuis, and P. Nivela. Context trees. In IJCAR 2001, Proceedings of the International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, Siena, Italy, June 2001. Springer Verlag.","DOI":"10.1007\/3-540-45744-5_18"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"P. Graf. Extended path-indexing. In A. Bundy, editor, CADE-12. 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 514\u2013528, Nancy, France, June\/July 1994.","DOI":"10.1007\/3-540-58156-1_37"},{"key":"19_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Procs. 6th International Conference on Rewriting Techniques and Applications (RTA-95)","author":"P. Graf","year":"1995","unstructured":"P. Graf. Substitution tree indexing. In J. Hsiang, editor, Procs. 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 117\u2013131, Kaiserslautern, 1995."},{"key":"19_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Term Indexing","author":"P. Graf","year":"1996","unstructured":"P. Graf. Term Indexing, volume 1053 of Lecture Notes in Computer Science. Springer Verlag, 1996."},{"key":"19_CR7","unstructured":"J. Gu, P.W. Purdom, J. Franco, and B.W. Wah. Algorithms for the Satisfiability Problems. Cambridge University Press, 2001."},{"key":"19_CR8","series-title":"PhD thesis","volume-title":"Description and theoretical analysis of Planner: a language for proving theorems and manipulating models in a robot","author":"C. Hewitt","year":"1971","unstructured":"C. Hewitt. Description and theoretical analysis of Planner: a language for proving theorems and manipulating models in a robot. PhD thesis, Department of Mathematics, MIT, Cambridge, Mass., January 1971."},{"issue":"2","key":"19_CR9","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T. Hillenbrand","year":"1997","unstructured":"T. Hillenbrand, A. Buch, R. Vogt, and B. L\u00f6chner. Waldmeister: High-performance equational deduction. Journal of Automated Reasoning, 18(2):265\u2013270, 1997.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"19_CR10","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258\u2013282, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"19_CR11","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W.W. McCune","year":"1992","unstructured":"W.W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147\u2013167, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"W.W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, January 1994.","DOI":"10.2172\/10129052"},{"key":"19_CR13","first-page":"459","volume-title":"Procs. 10th National Conference on Artificial Intelligence","author":"D.G. Mitchell","year":"1992","unstructured":"D.G. Mitchell, B. Selman, and H.J. Levesque. Hard and easy distributions of SAT problems. In W.R. Swartout, editor, Procs. 10th National Conference on Artificial Intelligence, pages 459\u2013465, San Jose, CA, January 1992. AAAI Press\/MIT Press."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis. Rewrite-based deduction and symbolic constraints. In H. Ganzinger, editor, CADE-16. 16th Int. Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 302\u2013313, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_28"},{"issue":"2","key":"19_CR15","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1005862710017","volume":"18","author":"R. Nieuwenhuis","year":"1997","unstructured":"R. Nieuwenhuis, J.M. Rivero, and M.\u00c1. Vallejo. The Barcelona prover. Journal of Automated Reasoning, 18(2):171\u2013176, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR16","unstructured":"H.J. Ohlbach. Abstraction tree indexing for terms. In H.-J. B\u00f6rkert and W. Nutt, editors, Extended Abstracts of the Third International Workshop on Unification, pages 131\u2013135. Universit\u00e4t Kaiserslautern, 1989. SEKI-Report SR 89-17."},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. Paterson","year":"1978","unstructured":"M. Paterson and M. Wegman. Linear unification. Journal of Computer and System Sciences, 16:158\u2013167, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"19_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-15976-2_21","volume-title":"Rewriting Techniques and Applications","author":"P.W. Purdom","year":"1985","unstructured":"P.W. Purdom and C.A. Brown. Fast many-to-one matching algorithms. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, First International Conference, RTA-85, volume 202 of Lecture Notes in Computer Science, pages 407\u2013416, Dijon, France, 1985. Springer Verlag."},{"key":"19_CR19","unstructured":"I.V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 1\u201397. Elsevier Science and MIT Press, 2001. To appear."},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov.Vampire. In H. Ganzinger, editor, CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 292\u2013296, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_26"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov. Partially adaptive code trees. In M. Ojeda-Aciego, I.P. de Guzm\u00e1n, G. Brewka, and L.M. Pereira, editors, Logics in Artificial Intelligence. European Workshop, JELIA 2000, volume 1919 of Lecture Notes in Artificial Intelligence, pages 209\u2013223, M\u00e1laga, Spain, 2000. Springer Verlag.","DOI":"10.1007\/3-540-40006-0_15"},{"key":"19_CR22","series-title":"Phd thesis","volume-title":"Data Structures and Algorithms for Automated Deduction with Equality","author":"J.M.A. Rivero","year":"2000","unstructured":"J.M.A. Rivero. Data Structures and Algorithms for Automated Deduction with Equality. Phd thesis, Universitat Polit\u00e8ecnica de Catalunya, Barcelona, May 2000."},{"key":"19_CR23","unstructured":"S. Schulz. Learning Search Control Knowledge for Equational Deduction, volume 230 of Dissertationen zur k\u00f6nstliche Intelligenz. Akademische Verlagsgesellschaft Aka GmmH, 2000."},{"key":"19_CR24","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.21236\/ADA460990","volume-title":"The path indexing method for indexing terms","author":"M. Stickel","year":"1989","unstructured":"M. Stickel. The path indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1989."},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe and C. Suttner. The TPTP problem library \u2014 CNF release v. 1.2.1. Journal of Automated Reasoning, 21(2), 1998.","DOI":"10.1023\/A:1005806324129"},{"issue":"2","key":"19_CR26","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"A. Voronkov. The anatomy of Vampire: Implementing bottom-up procedures with code trees. Journal of Automated Reasoning, 15(2):237\u2013265, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR27","volume-title":"CASC 16 1\/2","author":"A. Voronkov","year":"2000","unstructured":"A. Voronkov. CASC 16 1\/2. Preprint CSPP-4, Department of Computer Science, University of Manchester, February 2000."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T01:50:43Z","timestamp":1556934643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001]]}}}