{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:29Z","timestamp":1749124049740},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"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":[[1994]]},"DOI":"10.1007\/bf00885766","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T21:27:37Z","timestamp":1104182857000},"page":"359-388","source":"Crossref","is-referenced-by-count":5,"title":["Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures"],"prefix":"10.1007","volume":"12","author":[{"given":"Shie-Jue","family":"Lee","sequence":"first","affiliation":[]},{"given":"Chih-Hung","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.W.: Non-resolution theorem proving,Artificial Intelligence 9 (1977), 1?35.","journal-title":"Artificial Intelligence"},{"key":"CR2","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.2172\/6569195","volume-title":"A tutorial on the construction of high-performance resolution\/paramodulation systems","author":"R. Butler","year":"1990","unstructured":"Butler, R. and Overbeek, R.: A tutorial on the construction of high-performance resolution\/paramodulation systems, Technical Report ANL-90\/30, Argonne National Laboratory, Argonne, Ill., 1990."},{"key":"CR3","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C. and Lee, R.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"CR4","volume-title":"Artificial Intelligence Programming","author":"E. Charniak","year":"1980","unstructured":"Charniak, E., Reisbeck C. and McDermott, D.:Artificial Intelligence Programming, Lawrence Earlbaum Assoc., Hillside, N.J., 1980."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Christian, J.: Fast knuth-Bendix completion: A summary, inProc. 3rd International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 355, New York, 1990, pp. 551?555.","DOI":"10.1007\/3-540-51081-8_136"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory,J. Assoc. Comput. Machinery 7 (1960), 201?215.","journal-title":"J. Assoc. Comput. Machinery"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C. L. Forgy","year":"1982","unstructured":"Forgy, C. L.: Rete: A fast algorithm for the many pattern\/many object pattern match problem,Artificial Intelligence 19 (1982), 17?37.","journal-title":"Artificial Intelligence"},{"key":"CR8","first-page":"958","volume":"21","author":"E. C. Freuder","year":"1978","unstructured":"Freuder, E. C.: Synthesizing contraint expressions,Comm. Assoc. Comput. Machinery 21 (1978), 958?966.","journal-title":"Comm. Assoc. Comput. Machinery"},{"key":"CR9","unstructured":"Fujita, H. and Hasegawa, R.: A model generation theorem prover in KL1 using a ramified-stack algorithm, inProc. 8th International Conference on Logic Programming, 1991, pp. 535?548."},{"key":"CR10","volume-title":"Expert Systems: Principles and Programming","author":"J. Giarratano","year":"1989","unstructured":"Giarratano, J. and Riley, G.:Expert Systems: Principles and Programming, PWS-KENT Publishing Company, Boston, 1989."},{"key":"CR11","unstructured":"Greenbaum, S.:Input Transformations and Resolution Implementation Techniques for Theorem Proving in First-Order Logic, Ph.D. thesis, University of Illinois at Urbana-Champaign, 1986."},{"key":"CR12","unstructured":"Lee, S.-J. and Plaisted, D.: New applications of a fast propositional calculus decision procedure, inProc. 8th Biennial Conference of Canadian Society for Computational Studies of Intelligence, Ottawa, Canada, 1990, pp. 204?211."},{"issue":"1","key":"CR13","first-page":"25","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J. and Plaisted, D.: Eliminating duplication with the hyperlinking strategy,J. Automated Reasoning 9(1) (1992), 25?42.","journal-title":"J. Automated Reasoning"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Lee, S.-J. and Plaisted, D.: Problem solving by searching for models with a theorem prover,Artificial Intelligence (to appear).","DOI":"10.1016\/0004-3702(94)90082-5"},{"key":"CR15","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"Loveland, D.:Automated Theorem Proving: A Logical Basis, North-Holland, New York, 1978."},{"key":"CR16","first-page":"103","volume":"1","author":"E. Lusk","year":"1985","unstructured":"Lusk, E. and Overbeek, R.: Non-Horn problems,J. Automated Reasoning 1 (1985), 103?114.","journal-title":"J. Automated Reasoning"},{"key":"CR17","first-page":"1","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R. and Wos, L.: Complexity and related enhancements for automated theoremproving programs,Computers and Mathematics with Applications 2 (1976), 1?16.","journal-title":"Computers and Mathematics with Applications"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-Tree indexing and path indexing for term retrieval,J. Automatic Reasoning 9 (1992), 147?169.","journal-title":"J. Automatic Reasoning"},{"key":"CR19","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 (1986), 191?216.","journal-title":"J. Automated Reasoning"},{"key":"CR20","volume-title":"C-Prolog User's Manual","author":"F. Pereira","year":"1984","unstructured":"Pereira, F.:C-Prolog User's Manual, SRI International, Menlo Park, California, 1984."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","volume":"18","author":"D. Plaisted","year":"1982","unstructured":"Plaisted, D.: A simplified problem reduction format,Artificial Intelligence 18 (1982), 227?261.","journal-title":"Artificial Intelligence"},{"key":"CR22","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"Plaisted, D. and Greenbaum, S.: A structure-preserving clause form translation.J. of Symbolic Computation 2 (1986), 293?304.","journal-title":"J. of Symbolic Computation"},{"key":"CR23","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/321160.321166","volume":"10","author":"J. Robinson","year":"1963","unstructured":"Robinson, J.: Theorem proving on the computer,J. Assoc. Comput. Machinery 10 (1963), 163?174.","journal-title":"J. Assoc. Comput. Machinery"},{"key":"CR24","unstructured":"Scales, D. J.: Efficient matching algorithm for the SOAR\/OPS5 production system, Technical Report STAN-CS-86-1124, Departments of Computer Sciences, Stanford University, 1986."},{"key":"CR25","volume-title":"The Art of Prolog","author":"L. Sterling","year":"1986","unstructured":"Sterling, L. and Shapiro, E.:The Art of Prolog, MIT Press, Cambridge, Massachusetts, 1986."},{"key":"CR26","series-title":"Technical Note","doi-asserted-by":"crossref","DOI":"10.21236\/ADA460990","volume-title":"The path-indexing method for indexing terms","author":"M. E. Stickel","year":"1989","unstructured":"Stickel, M. E.: The path-indexing method for indexing terms, Technical Note 473, Artificial Intelligence Center, SRI International, Menlo Park, California, 1989."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E.: A Prolog technology theorem prover: Implementation by an extended Prolog compiler,J. Automated Reasoning 4 (1988), 353?380.","journal-title":"J. Automated Reasoning"},{"key":"CR28","unstructured":"Sutcliffe, G.: The TPTP problem library, release v1.0.0, Technical Report, Department of Computer Sciences, James Cook University, 1993."},{"key":"CR29","unstructured":"Ullman, J. D.:Database and Knowledge-Base Systems, Vol. 1: Classical Database Systems, Computer Science Press, 1988."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00885766.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00885766\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00885766","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T00:11:06Z","timestamp":1586045466000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00885766"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00885766"],"URL":"https:\/\/doi.org\/10.1007\/bf00885766","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}