{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:07Z","timestamp":1747546927693},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["NGCO"],"published-print":{"date-parts":[[1998,6]]},"DOI":"10.1007\/bf03037315","type":"journal-article","created":{"date-parts":[[2009,4,22]],"date-time":"2009-04-22T02:00:02Z","timestamp":1240365602000},"page":"163-200","source":"Crossref","is-referenced-by-count":7,"title":["On semantic resolution with lemmaizing and contraction and a formal treatment of caching"],"prefix":"10.1007","volume":"16","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Jieh","family":"Hsiang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF03037315_CR1","series-title":"number 516 in Lecture Notes in Computer Science","first-page":"156","volume-title":"Proceedings of the Second International Workshop on Conditional and Typed Term Rewriting Systems","author":"S. Anantharaman","year":"1990","unstructured":"Anantharaman, S. and Bonacina, M. P., \u201cAn Application of Automated Equational Reasoning to Many-Valued Logic,\u201d inProceedings of the Second International Workshop on Conditional and Typed Term Rewriting Systems (M. Okada and S. Kaplan, eds.),number 516 in Lecture Notes in Computer Science, Montr\u00e9al, Canada, June 1990, Springer-Verlag, pp. 156\u2013161, 1990."},{"issue":"1","key":"BF03037315_CR2","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/BF00302643","volume":"6","author":"S. Anantharaman","year":"1990","unstructured":"Anantharaman, S. and Hsiang, J., \u201cAutomated Proofs of the Moufang Identities in Alternative Rings,\u201dJournal of Automated Reasoning, 6, 1, pp. 76\u2013109, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037315_CR3","unstructured":"Astrachan, O. L., \u201cInvestigations in Theorem Proving Based on Model Elimination,\u201dPh.D. thesis, Department of Computer Science, Duke University, 1992."},{"key":"BF03037315_CR4","series-title":"Automated Reasoning Series","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-94-011-3488-0_2","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"O. L. Astrachan","year":"1991","unstructured":"Astrachan, O. L. and Loveland, D. W., \u201cMETEORs: High Performance Theorem Provers Using Model Elimination,\u201d inAutomated Reasoning: Essays in Honor of Woody Bledsoe (R. S. Boyer, ed.), Automated Reasoning Series, Kluwer Academic Publisher, Dordrecht, Netherlands, pp. 31\u201360, 1991."},{"key":"BF03037315_CR5","series-title":"Technical Report","first-page":"224","volume-title":"Eleventh Conference on Automated Deluction, volume 607 of Lecture Notes in Artificial Intelligence","author":"O. L. Astrachan","year":"1992","unstructured":"Astrachan, O. L. and Stickel, M. E., \u201cCaching and Lemmaizing in Model Elimination Theorem Provers,\u201d inEleventh Conference on Automated Deluction, volume 607 of Lecture Notes in Artificial Intelligence (D. Kapur, ed.), Saratoga Springs, New York, U.S.A., June 1992, Springer-Verlag, pp. 224\u2013238, 1992. Full version available asTechnical Report, 513, SRI International, December 1991."},{"key":"BF03037315_CR6","doi-asserted-by":"crossref","unstructured":"Bachmair, L. and Ganzinger, H., \u201cOn Restrictions of Ordered Paramodulation with Simplification,\u201d inTenth Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence (M. E. Stickel, ed.), Springer-Verlag, pp. 427\u2013441, 1990.","DOI":"10.1007\/3-540-52885-7_105"},{"issue":"1 & 2","key":"BF03037315_CR7","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0743-1066(92)90050-D","volume":"14","author":"M. P. Bonacina","year":"1992","unstructured":"Bonacina, M. P. and Hsiang, J., \u201cOn Rewrite Programs: Semantics and Relationship with Prolog,\u201dJournal of Logic Programming, 14, 1 & 2, pp. 155\u2013180, October 1992.","journal-title":"Journal of Logic Programming"},{"key":"BF03037315_CR8","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"M. P. Bonacina","year":"1995","unstructured":"Bonacina, M. P. and Hsiang, J., \u201cTowards a Foundation of Completion Procedures as Semidecision Procedures,\u201dTheoretical Computer Science, 146, pp. 199\u2013242, July 1995.","journal-title":"Theoretical Computer Science"},{"key":"BF03037315_CR9","first-page":"372","volume-title":"Fourth Pacific Rim International Conference on Artificial Intelligence, volume 1114 of Lecture Notes in Artificial Intelligence","author":"M. P. Bonacina","year":"1996","unstructured":"Bonacina, M. P. and Hsiang, J., \u201cOn Semantic Resolution with Lemmaizing and Contraction,\u201d inFourth Pacific Rim International Conference on Artificial Intelligence, volume 1114 of Lecture Notes in Artificial Intelligence (N. Foo and R. Goebel, eds.), Cairns, Australia, August 1996, Springer-Verlag, pp. 372\u2013386, 1996."},{"key":"BF03037315_CR10","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"Chang, C. L. and Lee, R. C.,Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, U.S.A., 1973."},{"key":"BF03037315_CR11","first-page":"551","volume-title":"Third Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science","author":"J. D. Christian","year":"1989","unstructured":"Christian, J. D., \u201cFast Knuth-Bendix Completion: Summary,\u201d, inThird Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science (N. Dershowitz, ed.), Chapel Hill, North Carolina, U.S.A., April 1989, Springer-Verlag, pp. 551\u2013555, 1989."},{"key":"BF03037315_CR12","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., \u201cA Computing Procedure for Quantification Theory,\u201dJournal of the ACM, 7, pp. 201\u2013215, 1960.","journal-title":"Journal of the ACM"},{"key":"BF03037315_CR13","first-page":"267","volume-title":"Eighteenth International Conference on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science","author":"N. Dershowitz","year":"1991","unstructured":"Dershowitz, N., \u201cCanonical Sets of Horn Clauses,\u201d inEighteenth International Conference on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science (J. Leach Albert, B. Monien, and M. Rodr\u00edguez Artalejo, eds.), Madrid, Spain, 1991, Springer-Verlag, pp. 267\u2013278, 1991."},{"key":"BF03037315_CR14","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1145\/321796.321807","volume":"21","author":"S. Fleisig","year":"1974","unstructured":"Fleisig, S., Loveland, D., Smiley, A., and Yarmush, D., \u201cAn Implementation of the Model Elimination Proof Procedure,\u201dJournal of the ACM, 21, pp. 124\u2013139, 1974.","journal-title":"Journal of the ACM"},{"key":"BF03037315_CR15","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"Hsiang, J. and Rusinowitch, M., \u201cProving Refutational Completeness of Theorem Proving Strategies: The Transfinite Semantic Tree Method,\u201dJournal of the ACM, 38, pp. 559\u2013587, 1991.","journal-title":"Journal of the ACM"},{"key":"BF03037315_CR16","doi-asserted-by":"crossref","first-page":"768","DOI":"10.1007\/BFb0012889","volume-title":"Nineth Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science","author":"D. Kapur","year":"1988","unstructured":"Kapur, D. and Zhang, H., \u201cRRL: A Rewrite Rule Laboratory,\u201d inNineth Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science (E. Lusk and R. Overbeek, eds.), Argonne, Illinois, U.S.A., May 1988, Springer-Verlag, pp. 768\u2013770, 1988."},{"key":"BF03037315_CR17","first-page":"360","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"D. Kapur","year":"1991","unstructured":"Kapur, D. and Zhang, H., \u201cA Case Study of the Completion Procedure: Proving Ring Commutativity Problems,\u201d inComputational Logic: Essays in Honor of Alan Robinson (J.-L. Lassez and G. Plotkin, eds.), MIT Press, Cambridge, Massachusetts, pp. 360\u2013394, 1991."},{"issue":"1","key":"BF03037315_CR18","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"Korf, R. E., \u201cDepth-First Iterative Deepening: An Optimal Admissible Tree Search,\u201dArtificial Intelligence, 27, 1, pp. 97\u2013109, 1985.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"BF03037315_CR19","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., and Bibel, W., \u201cSETHEO: A High Performance Theorem Prover,\u201dJournal of Automated Reasoning, 8, 2, pp. 183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"BF03037315_CR20","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. W. Loveland","year":"1969","unstructured":"Loveland, D. W., \u201cA Simplified Format for the Model Elimination Procedure,\u201dJournal of the ACM, 16, 3, pp. 349\u2013363, 1969.","journal-title":"Journal of the ACM"},{"issue":"2","key":"BF03037315_CR21","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1145\/321694.321706","volume":"19","author":"D. W. Loveland","year":"1972","unstructured":"Loveland, D. W., \u201cA Unifying View of Some Linear Herbrand Procedures,\u201dJournal of the ACM, 19, 2, pp. 366\u2013384, 1972.","journal-title":"Journal of the ACM"},{"issue":"2","key":"BF03037315_CR22","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W., \u201cExperiments with Discrimination Tree Indexing and Path Indexing for Term Retrieval,\u201dJournal of Automated Reasoning, 9, 2, pp. 147\u2013167, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037315_CR23","doi-asserted-by":"crossref","unstructured":"McCune, W., \u201cOtter 3.0 Reference Manual and Guide,\u201dTechnical Report, 94\/6, Mathematics and Computer Science Division, Argonne National Laboratory, 1994.","DOI":"10.2172\/10129052"},{"key":"BF03037315_CR24","unstructured":"McCune, W., \u201cSolution of the Robbins Problem,\u201dPre-print of the Mathematics and Computer Science Division, Argonne National Laboratory, 1997."},{"issue":"3","key":"BF03037315_CR25","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. A. Plaisted","year":"1988","unstructured":"Plaisted, D. A., \u201cNon-Horn Clause Logic Programming without Contrapositives,\u201dJournal of Automated Reasoning, 4, 3, pp. 287\u2013325, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037315_CR26","doi-asserted-by":"crossref","unstructured":"Plaisted, D. A., \u201cThe Search Efficiency of Theorem Proving Strategies,\u201d inTwelfth Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence (A. Bundy, ed.), Springer-Verlag, pp. 57\u201371, 1994. Full version available asTechnical Report of the Max Planck Institut f\u00fcr Informatik, MPI-I-94-233.","DOI":"10.1007\/3-540-58156-1_5"},{"key":"BF03037315_CR27","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A., \u201cAutomatic Deduction with Hyper-Resolution,\u201dInternational Journal of Computer Mathematics, 1, pp. 227\u2013234, 1965.","journal-title":"International Journal of Computer Mathematics"},{"issue":"1 & 2","key":"BF03037315_CR28","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"Rusinowitch, M., \u201cTheorem-Proving with Resolution and Superposition,\u201dJournal of Symbolic Computation, 11, 1 & 2, pp. 21\u201350, 1991.","journal-title":"Journal of Symbolic Computation"},{"key":"BF03037315_CR29","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"Shostak, R. E., \u201cRefutation Graphs,\u201dArtificial Intelligence, 7, pp. 51\u201364, 1976.","journal-title":"Artificial Intelligence"},{"issue":"4","key":"BF03037315_CR30","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J. R. Slagle","year":"1967","unstructured":"Slagle, J. R., \u201cAutomatic Theorem Proving with Renamable and Semantic Resolution,\u201dJournal of the ACM, 14, 4, pp. 687\u2013697, 1967.","journal-title":"Journal of the ACM"},{"key":"BF03037315_CR31","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E., \u201cA Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler,\u201dJournal of Automated Reasoning, 4, pp. 353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"BF03037315_CR32","doi-asserted-by":"crossref","unstructured":"Stickel, M. E., \u201cThe Path-Indexing Method for Indexing Terms,\u201dTechnical Report, 473, SRI International, 1989.","DOI":"10.21236\/ADA460990"},{"key":"BF03037315_CR33","series-title":"Automated Reasoning Series","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/978-94-011-3488-0_14","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"M. E. Stickel","year":"1991","unstructured":"Stickel, M. E., \u201cPTTP and Linked Inference,\u201d inAutomated Reasoning: Essays in Honor of Woody Bledsoe (R. S. Boyer, ed.), Automated Reasoning Series, Kluwer Academic Publisher, Dordrecht, Netherlands, pp. 283\u2013296, 1991."},{"issue":"6","key":"BF03037315_CR34","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1093\/jigpal\/3.6.921","volume":"3","author":"K. Wallace","year":"1995","unstructured":"Wallace, K. and Wrightson, G., \u201cRegressive Merging in Model Elimination Tableau-Based Theorem Provers,\u201dJournal of the IGPL, 3, 6, pp. 921\u2013937, 1995.","journal-title":"Journal of the IGPL"},{"key":"BF03037315_CR35","unstructured":"Warren, D. H. D., \u201cAn Abstract Prolog Instruction Set,\u201dTechnical Report, 309, SRI International, 1983."},{"issue":"3","key":"BF03037315_CR36","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1145\/131295.131299","volume":"35","author":"D. S. Warren","year":"1992","unstructured":"Warren, D. S., \u201cMemoing for Logic Programs,\u201dCommunications of the ACM, 35, 3, pp. 94\u2013111, 1992.","journal-title":"Communications of the ACM"},{"key":"BF03037315_CR37","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Carson, D., and Robinson, G., \u201cEfficiency and Completeness of the Set of Support Strategy in Theorem Proving,\u201dJournal of the ACM, 12, pp. 536\u2013541, 1965.","journal-title":"Journal of the ACM"}],"container-title":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03037315.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF03037315\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03037315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T00:52:34Z","timestamp":1558572754000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF03037315"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,6]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,6]]}},"alternative-id":["BF03037315"],"URL":"https:\/\/doi.org\/10.1007\/bf03037315","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"value":"0288-3635","type":"print"},{"value":"1882-7055","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,6]]}}}