{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:04:52Z","timestamp":1763967892582},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf00881918","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:40:00Z","timestamp":1104003600000},"page":"237-265","source":"Crossref","is-referenced-by-count":46,"title":["The anatomy of vampire"],"prefix":"10.1007","volume":"15","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Astrakhan, O. L. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem prover in D. Kapur (ed.),11th Int. Conf. on Automated Deduction, Vol. 607 of Lecture Notes in Artificial Intelligence, Saratoga Springs, NY, June 1992. Springer Verlag, pp. 224?239.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Bancilhon, F., Maier, D., Sagiv, Y., and Ullman, J. D.: Magic sets and other strange ways to implement logic programs, inProc. of the 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems, Cambridge, MA, March 1986, pp. 1?15.","DOI":"10.1145\/6012.15399"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Beeri, C., Naqvi, Sh., Ramakrishnan, R., Shmueli, O., and Tsur, Sh.: Sets and negation in a logic database language (LDL1), inProc. 6th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, ACM Press, 1987, 21?36.","DOI":"10.1145\/28659.28662"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Beeri, C. and Ramakrishnan, R.: On the power of Magic, inProc. 6th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, ACM Press, 1987, pp. 269?283.","DOI":"10.1145\/28659.28689"},{"key":"CR5","unstructured":"Codish, M. and Demoen, B.: Analyzing logic programs using ?Prop?-ositional logic programs and a magic wand, in Dale Miller (ed.),Logic Programming ? Proc. of the 1993 Int. Symposium, The MIT Press, 1993, pp. 114?129."},{"key":"CR6","unstructured":"Das, S. K.:Deductive Databases and Logic Programming, Addison-Wesley, 1992."},{"key":"CR7","unstructured":"Decker, H.: Integrity enforcements on deductive databases, inProc. of the 1st Int. Conf. on Expert Database Systems, Charleston, South Carolina, April 1986, pp. 271?285."},{"key":"CR8","volume-title":"Computers and Intractability","author":"M. R. Garey","year":"1979","unstructured":"Garey, M. R. and Johnson, D. S.:Computers and Intractability, Freeman, San Francisco, 1979."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Goller, C., Letz, R., Mayr, K., and Schumann, J.: SETHEO V3.2: Recent developments, in A. Bundy (ed.),Automated Deduction ? CADE-12. 12th Int. Conf. on Automated Deduction, Vol. 814 of Lecture Notes in Artificial Intelligence, Nancy, France, June\/July 1994, pp. 778?782.","DOI":"10.1007\/3-540-58156-1_59"},{"issue":"2","key":"CR10","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1987","unstructured":"Gottlob, G. and Leitsch, A.: On the efficiency of subsumption algorithms,J. Association for Computing Machinery 32(2) (1987), 280?295.","journal-title":"J. Association for Computing Machinery"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Graf, P.: Extended path-indexing, in A. Bundy (ed.),Automated Deduction ? CADE-12. 12th Int. Conf. on Automated Deduction, Vol. 814 of Lecture Notes in Artificial Intelligence, Nancy, France, June\/July 1994, pp. 514?528.","DOI":"10.1007\/3-540-58156-1_37"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Lusk, E. L.: Controlling redundancy in large search spaces: Argonne-style theorem proving through the years, in A. Voronkov (ed.),Logic Programming and Automated Reasoning. International Conference LPAR'92, Vol. 624 of Lecture Notes in Artificial Intelligence, St. Petersburg, Russia, July 1992, pp. 96?106.","DOI":"10.1007\/BFb0013052"},{"key":"CR13","unstructured":"Lloyd, J. W., Sonenberg, E. A., and Topor, R. W.: Integrity constraint checking in stratified databases. Technical Report 86\/5, Department of Computer Science, University of Melbourne, 1986."},{"issue":"2","key":"CR14","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0743-1066(85)90013-5","volume":"2","author":"J. W. Lloyd","year":"1985","unstructured":"Lloyd, J. W. and Topor, R. W.: A basis for deductive database systems,J. Logic Programming 2(2) (1985), 93?109.","journal-title":"J. Logic Programming"},{"issue":"7","key":"CR15","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1002\/spe.4380240702","volume":"24","author":"A. M. Maeda","year":"1994","unstructured":"Maeda, A. M., Aoe, J.-I., and Tomabechi, H.: Signature-check based unification filter,Software ? Practice and Experience 24(7) (1994), 603?622.","journal-title":"Software ? Practice and Experience"},{"key":"CR16","first-page":"179","volume-title":"CADE'88 (9th Int. Conf. on Automated Deduction)","author":"R. Manthey","year":"1988","unstructured":"Manthey, R. and Bry, F.: SATCHMO: A theorem prover implemented in Prolog, inCADE'88 (9th Int. Conf. on Automated Deduction), Lecture Notes in Computer Science, Argonne, IL, May 1988, pp. 179?216."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Maslov, S. Yu.: An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus, in J. Siekmann and G. Wrightson (eds),Automation of Reasoning (Classical Papers on Computational Logic), Vol. 2, Springer Verlag, 1983, pp. 48?54.","DOI":"10.1007\/978-3-642-81955-1_3"},{"key":"CR18","first-page":"1","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., and Wos, L.: Complexity and related enhancements for automated theorem-proving programs,Computers and Mathematics with Applications 2 (1976), 1?16.","journal-title":"Computers and Mathematics with Applications"},{"issue":"8","key":"CR19","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., and Wos, L.: Problems and experiments for and with automated theorem-proving programs,IEEE Transactions on Computers C-25(8) (1976), 773?782.","journal-title":"IEEE Transactions on Computers"},{"issue":"9","key":"CR20","first-page":"7","volume":"1","author":"William W. McCune","year":"1988","unstructured":"McCune, William W.: An indexing method for finding more general formulas,Association for Automated Reasoning Newsletter 1(9) (1988), 7?8.","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"CR21","unstructured":"McCune, William W.: OTTER 2.0 users guide. Technical report, Argonne National Laboratory, March 1990."},{"issue":"2","key":"CR22","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"William W. McCune","year":"1992","unstructured":"McCune, William W.: Experiments with discrimination-tree in indexing and path indexing for term retrieval,J. Automated Reasoning 9(2) (1992), 147?167.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"CR23","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(90)90043-5","volume":"9","author":"V. Neiman","year":"1990","unstructured":"Neiman, V.: Refutation search for born sets by a subgoal-extraction method,J. Logic Programming 9(2) (1990), 267?284.","journal-title":"J. Logic Programming"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0898-1221(75)90019-X","volume":"1","author":"R. Overbeek","year":"1975","unstructured":"Overbeek, R.: An implementation of hyper-resolution,Computers and Mathematics with Applications 1 (1975), 201?214.","journal-title":"Computers and Mathematics with Applications"},{"issue":"2","key":"CR25","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J.: Seventy-five problems for testing automatic theorem provers,J. Automated Reasoning 2(2) (1986), 191?216.","journal-title":"J. Automated Reasoning"},{"key":"CR26","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: Automatic deduction with hyper-resolution,Int. J. Computer Mathematics 1 (1965), 227?234.","journal-title":"Int. J. Computer Mathematics"},{"issue":"1","key":"CR27","doi-asserted-by":"crossref","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. the Association for Computing Machinery 12(1) (1965), 23?41.","journal-title":"J. the Association for Computing Machinery"},{"key":"CR28","volume-title":"Machine Intelligence, Vol. 4","author":"G. Robinson","year":"1969","unstructured":"Robinson, G. and Wos, L. T.: Paramodulation and theorem-proving in first order theories with equality, inMachine Intelligence, Vol. 4. Edinburgh University Press, Edinburgh, 1969."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Stickel, M.: A PROLOG technology theorem prover: Implementation by an extended Prolog compiler,J. Automated Reasoning (4) (1988), 353?380.","DOI":"10.1007\/BF00297245"},{"key":"CR30","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":"Stickel, M.: The path indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, Menlo Park, Calif., October 1989."},{"key":"CR31","unstructured":"Sudarshan, S. and Ramakrishnan, R.: Optimizations of bottom-up evaluation with non-ground terms (extended abstract), in Dale Miller (ed.),Logic Programming. Proc. of the 1993 Int. Symp., The MIT Press, 1993, pp. 557?574."},{"key":"CR32","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0004-3702(94)90097-3","volume":"68","author":"M. Tambe","year":"1994","unstructured":"Tambe, M. and Rosenbloom, P. S.: Investigating production system representations for non-combinatorial match,Artificial Intelligence 68 (1994), 155?190.","journal-title":"Artificial Intelligence"},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"Tamaki, H. and Sato, T.: OLDT resolution with tabulation, inInt. Conf. on Logic Programming, 1986, pp. 84?98.","DOI":"10.1007\/3-540-16492-8_66"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(89)90088-1","volume":"69","author":"Laurent Vieille","year":"1989","unstructured":"Vieille, Laurent: Recursive query processing: The power of logic,Theoretical Computer Science 69 (1989), 1?53.","journal-title":"Theoretical Computer Science"},{"key":"CR35","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: LISS ? The Logic Inference Search System, in Mark Stickel (ed.),Proc. Int. Conf. on Automated Deduction, Vol. 449 of Lecture Notes in Computer Science, Kaiserslautern, Germany, 1990. Springer Verlag, pp. 677?678.","DOI":"10.1007\/3-540-52885-7_138"},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Theorem proving in non-standard logics based on the inverse method, in D. Kapur (ed.),11th Int. Conf. on Automated Deduction, Vol. 607 of Lecture Notes in Artificial Intelligence, Saratoga Springs, NY, USA, June 1992. Springer Verlag, pp. 648?662.","DOI":"10.1007\/3-540-55602-8_198"},{"key":"CR37","unstructured":"Warren, David H. D.: An abstract Prolog instruction set. SRI Tech. Note 309, SRI Intl., Menlo Park, Calif., 1983."},{"issue":"3","key":"CR38","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/131295.131299","volume":"35","author":"D. S. Warren","year":"1992","unstructured":"Warren, D. S.: Memoing for logic programs,Communications of the ACM 35(3) (1992), 93?111.","journal-title":"Communications of the ACM"},{"key":"CR39","first-page":"3","volume-title":"Computational Logic. Essays in Honor of Alan Robinson","author":"Larry Wos","year":"1991","unstructured":"Wos, Larry, Overbeek, Ross, and Lusk, Ewing: Subsumption, a sometimes undervalued procedure, in Jean-Louis Lassez and Gordon Plotkin (eds),Computational Logic. Essays in Honor of Alan Robinson, The MIT Press, Cambridge, MA, 1991, pp. 3?40."},{"issue":"2","key":"CR40","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00245457","volume":"9","author":"Larry Wos","year":"1992","unstructured":"Wos, Larry: Note on McCune's article on discrimination trees,J. Automated Reasoning 9(2) (1992), 145?146.","journal-title":"J. Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881918.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881918\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881918","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:30:14Z","timestamp":1586043014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881918"}},"subtitle":["Implementing bottom-up procedures with code trees"],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881918"],"URL":"https:\/\/doi.org\/10.1007\/bf00881918","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}