{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:18Z","timestamp":1725664278656},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584025"},{"type":"electronic","value":"9783540486954"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58402-1_12","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:52:47Z","timestamp":1330271567000},"page":"147-164","source":"Crossref","is-referenced-by-count":0,"title":["An implementation technique for a class of bottom-up procedures"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"12_CR1","first-page":"224","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"O. L. Astrakhan","year":"1992","unstructured":"O.L. Astrakhan and M.E. Stickel. Caching and lemmaizing in model elimination theorem prover. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 224\u2013239, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"issue":"1","key":"12_CR2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/151646.151650","volume":"15","author":"R. Barbuti","year":"1993","unstructured":"R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics-based bottom-up abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems, 15(1):133\u2013181, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"F. Bancilhon, D. Maier, Y. Sagiv, and J.D. Ullman. Magic sets and other strange ways to implement logic programs. In Proceedings of the 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems, pages 1\u201315, Cambridge, MA, March 1986.","DOI":"10.1145\/6012.15399"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"C. Beeri, Sh. Naqvi, R. Ramakrishnan, O. Shmueli, and Sh. Tsur. Sets and negation in a logic database language (LDL1). In Proc. 6th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 21\u201336. ACM Press, 1987.","DOI":"10.1145\/28659.28662"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"C. Beeri and R. Ramakrishnan. On the power of Magic. In Proc. 6th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 269\u2013283. ACM Press, 1987.","DOI":"10.1145\/28659.28689"},{"key":"12_CR6","first-page":"101","volume-title":"Machine Intelligence","author":"R. S. Boyer","year":"1972","unstructured":"R.S. Boyer and J.S. Moore. The sharing of structure in theorem-proving programs. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 101\u2013116. Edinburgh University Press, Edinburgh, 1972."},{"key":"12_CR7","unstructured":"M. Codish and B. Demoen. Analyzing logic programs using \u201cProp\u201d-ositional logic programs and a magic wand. In Dale Miller, editor, Logic Programming \u2014 Proceedings of the 1993 International Symposium, pages 114\u2013129. The MIT Press, 1993."},{"key":"12_CR8","unstructured":"S.K. Das. Deductive Databases and Logic Programming. Addison-Wesley, 1992."},{"key":"12_CR9","unstructured":"H. Decker. Integrity enforcements on deductive databases. In Proc. of the 1st International Conference on Expert Database Systems, pages 271\u2013285, Charleston, South Carolina, April 1986."},{"key":"12_CR10","volume-title":"Technical Report MPI-I-92-237","author":"P. Graf","year":"1992","unstructured":"P. Graf. Path indexing for term retrieval. Technical Report MPI-I-92-237, Max-Planck Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, December 1992."},{"key":"12_CR11","unstructured":"J.W. Lloyd, E.A. Sonenberg, and R.W. Topor. Integrity constraint checking in stratified databases. Technical Report 86\/5, Department of Computer Science, University of Melbourne, 1986."},{"issue":"2","key":"12_CR12","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0743-1066(85)90013-5","volume":"2","author":"J. W. Lloyd","year":"1985","unstructured":"J.W. Lloyd and R.W. Topor. A basis for deductive database systems. Journal of Logic Programming, 2(2):93\u2013109, 1985.","journal-title":"Journal of Logic Programming"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In CADE'88 (9th Int. Conf. on Automated Deduction), Lecture Notes in Computer Science, pages 179\u2013216, Argonne, Illinois, May 1988.","DOI":"10.1007\/BFb0012847"},{"issue":"9","key":"12_CR14","first-page":"7","volume":"1","author":"William W. W. McCune","year":"1988","unstructured":"William W. McCune. An indexing method for finding more general formulas. Association for Automated Reasoning Newsletter, 1(9):7\u20138, 1988.","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"12_CR15","unstructured":"William W. McCune. OTTER 2.0 users guide. Technical report, Argonne National Laboratory, March 1990."},{"issue":"2","key":"12_CR16","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"William W. W. McCune","year":"1992","unstructured":"William W. McCune. Experiments with discrimination-tree in indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147\u2013167, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"S.Yu. Maslov. An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 2, pages 48\u201354. Springer Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1_3"},{"issue":"2","key":"12_CR18","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(90)90043-5","volume":"9","author":"V. Neiman","year":"1990","unstructured":"V. Neiman. Refutation search for horn sets by a subgoal-extraction method. Journal of Logic Programming, 9(2):267\u2013284, 1990.","journal-title":"Journal of Logic Programming"},{"issue":"2","key":"12_CR19","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F.J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2(2):191\u2013216, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR20","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"J.A. Robinson. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1:227\u2013234, 1965.","journal-title":"International Journal of Computer Mathematics"},{"issue":"1","key":"12_CR21","doi-asserted-by":"crossref","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 Association for Computing Machinery, 12(1):23\u201341, 1965.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"12_CR22","volume-title":"Machine Intelligence, volume 4","author":"G. Robinson","year":"1969","unstructured":"G. Robinson and L.T. Wos. Paramodulation and theorem-proving in first order theories with equality. In Machine Intelligence, volume 4. Edinburgh University Press, Edinburgh, 1969."},{"key":"12_CR23","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. Stickel","year":"1988","unstructured":"M. Stickel. A PROLOG technology theorem prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, (4):353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR24","volume-title":"Technical Report 473","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":"12_CR25","unstructured":"S. Sudarshan and R. Ramakrishnan. Optimizations of bottom-up evaluation with non-ground terms (extended abstract). In Dale Miller, editor, Logic Programming. Proceedings of the 1993 International Symposium, pages 557\u2013574. The MIT Press, 1993."},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"H. Tamaki and T. Sato. OLDT resolution with tabulation. In International Conference on Logic Programming, pages 84\u201398, 1986.","DOI":"10.1007\/3-540-16492-8_66"},{"key":"12_CR27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(89)90088-1","volume":"69","author":"L. Vieille","year":"1989","unstructured":"Laurent Vieille. Recursive query processing: The power of logic. Theoretical Computer Science, 69:1\u201353, 1989.","journal-title":"Theoretical Computer Science"},{"key":"12_CR28","first-page":"677","volume-title":"volume 449 of Lecture Notes in Computer Science","author":"A. Voronkov","year":"1990","unstructured":"A. Voronkov. LISS \u2014 the Logic Inference Search System. In Mark Stickel, editor, Proc. Int. Conf. on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 677\u2013678, Kaiserslautern, Germany, 1990. Springer Verlag."},{"key":"12_CR29","first-page":"648","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"A. Voronkov","year":"1992","unstructured":"A. Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 648\u2013662, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"A. Voronkov. The Anatomy of Vampire: Implementing Bottom-up Procedures with Code Trees. Submitted to Journal of Automated Reasoning, 1994.","DOI":"10.1007\/BF00881918"},{"key":"12_CR31","volume-title":"SRI Tech. Note 309","author":"David H. H. D. D. Warren","year":"1983","unstructured":"David H. D. Warren. An abstract Prolog instruction set. SRI Tech. Note 309, SRI Intl., Menlo Park, Calif., 1983."},{"issue":"3","key":"12_CR32","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/131295.131299","volume":"35","author":"D. S. Warren","year":"1992","unstructured":"D.S. Warren. Memoing for logic programs. Communications of the ACM (invited paper), 35(3):93\u2013111, 1992.","journal-title":"Communications of the ACM (invited paper)"},{"key":"12_CR33","first-page":"3","volume-title":"Computational Logic. Essays in Honor of Alan Robinson","author":"L. Wos","year":"1991","unstructured":"Larry Wos, Ross Overbeek, and Ewing Lusk. Subsumption, a sometimes undervalued procedure. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic. Essays in Honor of Alan Robinson., pages 3\u201340. The MIT Press, Cambridge, Massachusetts, 1991."},{"issue":"2","key":"12_CR34","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00245457","volume":"9","author":"L. Wos","year":"1992","unstructured":"Larry 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","Programming Language Implementation and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58402-1_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:19:55Z","timestamp":1605647995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58402-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584025","9783540486954"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-58402-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}