{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:00:16Z","timestamp":1776553216174,"version":"3.51.2"},"reference-count":94,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50028-x","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"1853-1964","source":"Crossref","is-referenced-by-count":58,"title":["Term Indexing"],"prefix":"10.1016","author":[{"given":"R.","family":"Sekar","sequence":"first","affiliation":[]},{"given":"I.V.","family":"Ramakrishnan","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50028-X_bb0010","series-title":"Warren's Abstract Machine: a Tutorial Reconstruction","author":"A\u00eft-Kaci","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0015","series-title":"Proceedings of the 4th International Joint Conference on Theory and Practice of Software Development (TAPSOFT)","first-page":"61","article-title":"Associative-commutative discrimination nets","author":"Bachmair","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0020","series-title":"International Joint Conference on Artificial Intelligence","first-page":"348","article-title":"Experiments with associative-commutative discrimination nets","author":"Bachmair","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0025","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0030","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/S0747-7171(87)80027-5","article-title":"Complexity of matching problems","volume":"3","author":"Benanav","year":"1987","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0035","first-page":"749","article-title":"Solving numerical constraints","volume":"Vol. I","author":"Bockmayr","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0040","series-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming (JICSLP-92)","first-page":"639","article-title":"Multistage indexing algorithms for speeding Prolog execution","author":"Chen","year":"1992"},{"issue":"12","key":"10.1016\/B978-044450813-3\/50028-X_rf0045","doi-asserted-by":"crossref","first-page":"1097","DOI":"10.1002\/spe.4380241202","article-title":"Multistage indexing algorithms for speeding Prolog execution","volume":"24","author":"Chen","year":"1994","journal-title":"Software \u2014 Practice and Experience"},{"issue":"12","key":"10.1016\/B978-044450813-3\/50028-X_bb0045","doi-asserted-by":"crossref","first-page":"1097","DOI":"10.1002\/spe.4380241202","article-title":"Multistage indexing algorithms for speeding Prolog execution","volume":"24","author":"Chen","year":"1994","journal-title":"Software \u2014 Practice and Experience"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50028-X_bb0050","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/227595.227597","article-title":"Tabled evaluation with delaying for general logic programs","volume":"43","author":"Chen","year":"1996","journal-title":"Journal of the ACM"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50028-X_bb0055","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0743-1066(93)90039-J","article-title":"HILOG: a foundation for higher-order logic programming","volume":"15","author":"Cheng","year":"1993","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0060","series-title":"Proceedings of the 3rd International Conference on Rewriting Techniques and Applications","first-page":"551","article-title":"Fast Knuth-Bendix completion: A summary","author":"Christian","year":"1989"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50028-X_bb0065","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF00881866","article-title":"Flatterms, discrimination nets, and fast term rewriting","volume":"10","author":"Christian","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0070","series-title":"17th Annual Symposium on Foundations of Computer Science","first-page":"197","article-title":"Complexity of trie index construction (extended abstract)","author":"Comer","year":"1976"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0080","series-title":"Programming Languages: Implementations, Logics and Programs, 7th International Symposium, PLILP'95","first-page":"133","article-title":"Design and implementation of jump tables for fast indexing of logic programs","author":"Dawson","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0080","series-title":"ACM Symposium on Principles of Programming Languages","first-page":"247","article-title":"Unification factoring for efficient execution of logic programs","author":"Dawson","year":"1995"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50028-X_bb0085","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/232706.232722","article-title":"Principles and practice of unification factoring","volume":"18","author":"Dawson","year":"1996","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1\/2","key":"10.1016\/B978-044450813-3\/50028-X_bb0090","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1005992522805","article-title":"An algorithm for the retrieval of unifiers from discrimination trees","volume":"20","author":"de Nivelle","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0095","series-title":"Bliksem 1.10 User's Manual","author":"de Nivelle","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0100","series-title":"\u2018Handbook of Theoretical Computer Science\u2019, Vol. B: Formal Methods and Semantics","first-page":"243","article-title":"Rewrite systems","author":"Dershowitz","year":"1990"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50028-X_bb0105","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1093\/comjnl\/38.5.381","article-title":"Associative-commutative matching via bipartite graph matching","volume":"38","author":"Eker","year":"1995","journal-title":"Computer Journal"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0110","series-title":"Context trees","author":"Ganzinger","year":"2001"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0115","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","article-title":"On the efficiency of subsumption algorithms","volume":"32","author":"Gottlob","year":"1987","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0120","series-title":"RTA'91","first-page":"323","article-title":"Left-to-right tree pattern matching","author":"Graf","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0125","article-title":"Path indexing for term retrieval","author":"Graf","year":"1992","journal-title":"Technical Report MPI-I-92-237, Max-Planck-Institut f\u00fcr Informatik, Saarbrucken, Germany"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0130","series-title":"Rewriting Techniques and Applications","first-page":"117","article-title":"Substitution tree indexing","author":"Graf","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0135","article-title":"Term Indexing","author":"Graf","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0140","article-title":"Input transformations and resolution implementation techniques for theorem-proving in first-order logic","author":"Greenbaum","year":"1986","journal-title":"PhD thesis, University of Illinois at Urbana-Champaign"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0145","series-title":"6th Int'l Joint Conference on Artifical Intelligence (IJCAI)","first-page":"528","article-title":"An improved filter for literal indexing in resolution systems","author":"Henschen","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0150","article-title":"Description and theoretical analysis of Planner: A language for proving theorems and manipulating models in a robot","author":"Hewitt","year":"1971","journal-title":"PhD thesis, Department of Mathematics, MIT"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0155","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1023\/A:1005872405899","article-title":"Waldmeister: High-performance equational deduction","volume":"18","author":"Hillenbrand","year":"1997","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50028-X_bb0160","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/322290.322295","article-title":"Pattern matching in trees","volume":"29","author":"Hoffmann","year":"1982","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0170","article-title":"Computation in nonambiguous linear term rewriting systems","author":"Huet","year":"1978","journal-title":"Technical Report 359, IRIA, Le Chesney, France"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0175","series-title":"Computational Logic. Essays in Honor of Alan Robinson","first-page":"395","article-title":"Computation in orthogonal rewriting systems, I and II","author":"Huet","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0180","series-title":"Computational Logic. Essays in Honor of Alan Robinson","article-title":"Computation in orthogonal rewriting systems, I and II","author":"Huet","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0185","first-page":"395","article-title":"Computation in nonambiguous linear term rewriting systems","author":"Huet","year":"1978","journal-title":"Technical Report 359, IRIA, Le Chesney, France"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0175","series-title":"Sictus Prolog User's Manual","author":"Int","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0180","series-title":"1992 ACM Conference on Lisp and Functional Programming","first-page":"335","article-title":"Fast parallel implementation of lazy languages \u2014 the EQUALS experience","author":"Kaser","year":"1992"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0185","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1017\/S0956796897002669","article-title":"EQUALS \u2014 a parallel implementation of a lazy language","volume":"7","author":"Kaser","year":"1997","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0205","series-title":"ESOP'90, 3rd European Symposium on Programming","first-page":"256","article-title":"The specificity rule for lazy pattern matching in ambiguous term rewriting systems","author":"Kennaway","year":"1990"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0195","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1137\/0206024","article-title":"Fast pattern matching in strings","volume":"6","author":"Knuth","year":"1977","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0200","series-title":"Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 1: Colloquium on Trees in Algebra and Programming","first-page":"57","article-title":"Compilation of pattern matching with associative-commutative functions","author":"Kounalis","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0205","series-title":"Foundations of Software Technology and Theoretical Computer Science, 7th Conference","first-page":"400","article-title":"Lazy pattern matching in the ML language","author":"Laville","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0210","series-title":"Proceedings of the European Symposium on Programming","first-page":"298","article-title":"Implementation of lazy pattern matching algorithms","author":"Laville","year":"1988"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0215","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","article-title":"SETHEO: A high-performance theorem prover","volume":"8","author":"Letz","year":"1992","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0220","series-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'93)","first-page":"515","article-title":"Complement problems and tree automata in AC-like theories","author":"Lugiez","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0225","series-title":"Logic Programming and Automated Reasoning. International Conference LPAR'92","first-page":"96","article-title":"Controlling redundancy in large search spaces: Argonne-style theorem proving through the years","author":"Lusk","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0230","series-title":"ACM Conference on Lisp and Functional Programming","first-page":"21","article-title":"Compiling lazy pattern matching","author":"Maranget","year":"1992"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0235","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","article-title":"Experiments with discrimination-tree indexing and path indexing for term retrieval","volume":"9","author":"McCune","year":"1992","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0240","article-title":"OTTER 3.0 reference manual and guide","author":"McCune","year":"1994","journal-title":"Technical Report ANL-94\/6, Argonne National Laboratory\/IL, USA"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0245","article-title":"OTTER 3.0 reference manual and guide","author":"McCune","year":"1994","journal-title":"Technical Report ANL-94\/6, Argonne National Laboratory"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0250","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","article-title":"Otter\u2014the CADE-13 competition incarnations","volume":"18","author":"McCune","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0255","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","article-title":"SETHEO and E-SETHEO\u2014the CADE-13 systems","volume":"18","author":"Moser","year":"1997","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0260","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast decision procedures based on congruence closure","volume":"27","author":"Nelson","year":"1980","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0265","article-title":"An indexing scheme for AC-equational theories","author":"Nicolaita","year":"1992","journal-title":"Technical report, Research Institute for Infomatics, Bucharest, Romania"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0270","series-title":"Let's COMPIT: a method for COMParing Indexing Techniques in theorem provers","author":"Nieuwenhuis","year":"2001"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0275","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1005862710017","article-title":"The Barcelona prover","volume":"18","author":"Nieuwenhuis","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0280","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0300","series-title":"Proceedings of the 9th European Conference on Artificial Intelligence","first-page":"479","article-title":"Abstraction tree indexing for terms","author":"Ohlbach","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0290","series-title":"ACM Conference on Lisp and Functional Programming","first-page":"273","article-title":"Compiling pattern matching by term decomposition","author":"Puel","year":"1990"},{"issue":"3 & 4","key":"10.1016\/B978-044450813-3\/50028-X_bb0295","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0743-1066(91)90026-L","article-title":"Magic templates: A spellbinding approach to logic programs","volume":"11","author":"Ramakrishnan","year":"1991","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0300","series-title":"Proceedings of the Third International Conference on Logic Programming","first-page":"569","article-title":"A superimposed codewords indexing scheme for very large Prolog databases","author":"Ramamohanarao","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0305","series-title":"Foundations of Software Technology and Theoretical Computer Science, 14th Conference","first-page":"288","article-title":"Automata-driven efficient subterm unification","author":"Ramesh","year":"1994"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0310","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1145\/128749.128752","article-title":"Nonlinear pattern matching in trees","volume":"39","author":"Ramesh","year":"1992","journal-title":"JACM"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0330","series-title":"Seventh Annual ACM Symposium on Principles of Programming Languages","first-page":"281","article-title":"Automata-driven indexing of Prolog clauses","author":"Ramesh","year":"1990"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_rf0335","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0743-1066(94)00016-Y","article-title":"Automata-driven indexing of Prolog clauses","volume":"23","author":"Ramesh","year":"1995","journal-title":"Journal of Logic Programming"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0320","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0743-1066(94)00016-Y","article-title":"Automata-driven indexing of Prolog clauses","volume":"23","author":"Ramesh","year":"1995","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0325","series-title":"Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming","first-page":"112","article-title":"A thread in time saves tabling time","author":"Rao","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0330","series-title":"Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction","first-page":"292","article-title":"Vampire","author":"Riazanov","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0335","series-title":"Limited resource strategy in resolution theorem proving","author":"Riazanov","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0340","series-title":"Logics in Artificial Intelligence. European Workshop, JELIA 2000","first-page":"209","article-title":"Partially adaptive code trees","author":"Riazanov","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0345","series-title":"An efficient algorithm for backward subsumption using path indexing and database joins","author":"Riazanov","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0350","series-title":"Splitting without backtracking","author":"Riazanov","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0355","article-title":"Data Structures and Algorithms for Automated Deduction with Equality","author":"Rivero","year":"2000","journal-title":"Phd thesis, Universitat Polit\u00e8cnica de Catalunya, Barcelona"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0360","article-title":"The XSB programmer's manual: version 1.7","author":"Sagonas","year":"1997","journal-title":"Technical report, SUNY at Stony Brook"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0365","series-title":"Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction","first-page":"297","article-title":"System abstract: E 0.3","author":"Schulz","year":"1999"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50028-X_bb0370","doi-asserted-by":"crossref","first-page":"1207","DOI":"10.1137\/S0097539793246252","article-title":"Adaptive pattern matching","volume":"24","author":"Sekar","year":"1995","journal-title":"SIAM Journal on Computing"},{"key":"10.1016\/B978-044450813-3\/50028-X_rf0395","series-title":"Proceedings of the 19th International Colloquium on Automata, Languages and Programming","first-page":"247","article-title":"Adaptive pattern matching","author":"Sekar","year":"1992"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50028-X_rf0400","doi-asserted-by":"crossref","first-page":"1207","DOI":"10.1137\/S0097539793246252","article-title":"Adaptive pattern matching","volume":"24","author":"Sekar","year":"1995","journal-title":"SIAM Journal on Computing"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0380","series-title":"Rewriting Techniques and Applications, 3rd International Conference, RTA-89","first-page":"573","article-title":"A subsumption algorithm based on characteristic matrices","author":"Socher","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0385","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","article-title":"A PROLOG technology theorem prover: Implementation by an extended Prolog compiler","volume":"4","author":"Stickel","year":"1988","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0390","article-title":"The path-indexing method for indexing terms","author":"Stickel","year":"1989","journal-title":"Technical Report 473, SRI International, Menlo Park, California, USA"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0395","series-title":"A Guide to SNARK","author":"Stickel","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0400","series-title":"Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction","first-page":"341","article-title":"Deductive composition of astronomical software from subroutine libraries","author":"Stickel","year":"1994"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0405","doi-asserted-by":"crossref","DOI":"10.1023\/A:1005806324129","article-title":"The TPTP problem library \u2014 CNF release v. 1.2.1","volume":"21","author":"Sutcliffe","year":"1998","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0410","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/A:1005887414560","article-title":"Gandalf","volume":"18","author":"Tammet","year":"1997","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50028-X_bb0415","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0890-5401(92)90075-Q","article-title":"Tight complexity bounds for term matching problems","volume":"101","author":"Verma","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0420","series-title":"Programming Languages Implementation and Logic Programming. 6th International Symposium, PLILP'94","first-page":"147","article-title":"An implementation technique for a class of bottom-up procedures","author":"Voronkov","year":"1994"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0425","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF00881918","article-title":"The anatomy of Vampire: Implementing bottom-up procedures with code trees","volume":"15","author":"Voronkov","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0430","series-title":"The Implementation of Functional Programming Languages","article-title":"Efficient compilation of pattern matching","author":"Wadler","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0435","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"Vol. II","author":"Weidenbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0440","series-title":"Automated Deduction \u2014 CADE-13","first-page":"141","article-title":"Spass & flotter version 0.42","author":"Weidenbach","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50028-X_bb0445","series-title":"Proceedings of the International Symposium on Logic Programming","first-page":"203","article-title":"Indexing Prolog clauses via superimposed codewords and field encoded words","author":"Wise","year":"1984"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50028-X_bb0450","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00245457","article-title":"Note on McCune's article on discrimination trees","volume":"9","author":"Wos","year":"1992","journal-title":"Journal of Automated Reasoning"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B978044450813350028X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B978044450813350028X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T00:55:31Z","timestamp":1556499331000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B978044450813350028X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":94,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50028-x","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}