{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:46Z","timestamp":1749125146322},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1996,6,1]],"date-time":"1996-06-01T00:00:00Z","timestamp":833587200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1996,6]]},"DOI":"10.1007\/bf00252178","type":"journal-article","created":{"date-parts":[[2004,11,2]],"date-time":"2004-11-02T10:35:14Z","timestamp":1099391714000},"page":"223-239","source":"Crossref","is-referenced-by-count":44,"title":["Using hints to increase the effectiveness of an automated reasoning program: Case studies"],"prefix":"10.1007","volume":"16","author":[{"given":"Robert","family":"Veroff","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"BF00252178_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\u201335.","journal-title":"Artificial Intelligence"},{"key":"BF00252178_CR2","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S., and Moore, J. S. A Computational Logic Handbook, Academic Press, San Diego (1988)."},{"key":"BF00252178_CR3","first-page":"360","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"D. Kapur","year":"1991","unstructured":"Kapur, D. and Zhang, H.: A case study of the completion procedure: Proving ring commutativity problems, in J.-L.Lassez and G.Plotkin (eds), Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA, 1991, pp. 360\u2013394."},{"key":"BF00252178_CR4","volume-title":"Elements of Mathematical Logic","author":"J. Lukasiewicz","year":"1963","unstructured":"Lukasiewicz, J.: Elements of Mathematical Logic, Pergamon Press, Oxford, 1963."},{"key":"BF00252178_CR5","first-page":"131","volume-title":"Jan Lukasiewicz: Selected Works","author":"J. Lukasiewicz","year":"1970","unstructured":"Lukasiewicz, J.: Investigations into the sentential calculus, in L.Borkowski (ed.), Jan Lukasiewicz: Selected Works, North-Holland, Amsterdam, 1970, pp. 131\u2013152."},{"key":"BF00252178_CR6","first-page":"1","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R. A. and Wos, L.: Complexity and related enhancements for automated theorem-proving programs, Computers and Mathematics with Applications 2 (1976), 1\u201316.","journal-title":"Computers and Mathematics with Applications"},{"key":"BF00252178_CR7","series-title":"Technical Report ANL-94\/6","doi-asserted-by":"crossref","DOI":"10.2172\/10129052","volume-title":"OTTER 3.0 Reference Manual and Guide","author":"W. W. McCune","year":"1994","unstructured":"McCune, W. W.: OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, IL, 1994."},{"key":"BF00252178_CR8","unstructured":"McCune, W. W.: Private communication, 1994."},{"key":"BF00252178_CR9","series-title":"Technical Report ANL-88-2","volume-title":"Reference Manual for the Environmental Theorem Prover, An Incarnation of AURA","author":"B. T. Smith","year":"1988","unstructured":"Smith, B. T.: Reference Manual for the Environmental Theorem Prover, An Incarnation of AURA, Technical Report ANL-88\u20132, Argonne National Laboratory, Argonne, IL, 1988."},{"key":"BF00252178_CR10","series-title":"Lecture Notes in Computer Science","first-page":"248","volume-title":"Proc. 7th Conf. on Automated Deduction","author":"M. E. Stickel","year":"1984","unstructured":"Stickel, M. E.: A case study of theorem proving by the Knuth-Bendix method: Discovering that x 3=x implies ring commutativity, in Proc. 7th Conf. on Automated Deduction, Lecture Notes in Computer Science 170, Springer-Verlag, New York, 1984, pp. 248\u2013258."},{"key":"BF00252178_CR11","series-title":"Technical Report ANL-81-6","doi-asserted-by":"crossref","DOI":"10.2172\/6898399","volume-title":"Canonicalization and Demodulation","author":"R. L. Veroff","year":"1981","unstructured":"Veroff, R. L.: Canonicalization and Demodulation, Technical Report ANL-81\u20136, Argonne National Laboratory, Argonne, IL, 1981."},{"key":"BF00252178_CR12","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00244283","volume":"8","author":"R. L. Veroff","year":"1992","unstructured":"Veroff, R. L. and Wos, L.: The linked inference principle, I: The formal treatment, J. Automated Reasoning 8 (1992), 213\u2013274.","journal-title":"J. Automated Reasoning"},{"key":"BF00252178_CR13","unstructured":"Veroff, R. L.: An Updated Demodulation Strategy for Ring Problems, Technical Report CS94-12, Department of Computer Science, University of New Mexico, 1994."},{"key":"BF00252178_CR14","first-page":"437","volume":"3","author":"T. C. Wang","year":"1987","unstructured":"Wang, T. C.: Case studies of Z-module reasoning: Proving benchmark theorems from ring theory, J. Automated Reasoning 3 (1987), 437\u2013451.","journal-title":"J. Automated Reasoning"},{"key":"BF00252178_CR15","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00244359","volume":"6","author":"S. Winker","year":"1990","unstructured":"Winker, S.: Robbins algebra: conditions that make a near-Boolean algebra Boolean, J. Automated Reasoning 6 (1990), 465\u2013489.","journal-title":"J. Automated Reasoning"},{"key":"BF00252178_CR16","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00245821","volume":"6","author":"L. Wos","year":"1990","unstructured":"Wos, L.: Meeting the challenge of fifty years of logic, J. Automated Reasoning 6 (1990), 213\u2013232.","journal-title":"J. Automated Reasoning"},{"key":"BF00252178_CR17","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-011-3488-0_15","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"L. Wos","year":"1991","unstructured":"Wos, L.: Automated reasoning and Bledsoe's dream for the field, in R. S.Boyer (ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, Dordrecht, 1991, pp. 297\u2013345."},{"key":"BF00252178_CR18","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0898-1221(94)00220-F","volume":"29","author":"L. Wos","year":"1995","unstructured":"Wos, L.: The resonance strategy, Computers and Mathematics with Applications 29 (1995), 133\u2013178.","journal-title":"Computers and Mathematics with Applications"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00252178.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00252178\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00252178","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T11:56:18Z","timestamp":1554292578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00252178"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,6]]},"references-count":18,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,6]]}},"alternative-id":["BF00252178"],"URL":"https:\/\/doi.org\/10.1007\/bf00252178","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,6]]}}}