{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:30Z","timestamp":1749124050088},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"2","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\/bf00881889","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:38:17Z","timestamp":1104133097000},"page":"241-264","source":"Crossref","is-referenced-by-count":1,"title":["The rue theorem-proving system: The complete set of LIM+ challenge problems"],"prefix":"10.1007","volume":"12","author":[{"given":"Vincent J.","family":"Digricoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"CR1","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"Bledsoe, W. W., Challenge problems in elementary calculus,J. Automated Reasoning 6(3) (1990), 341?59.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"CR2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/5383.5389","volume":"33","author":"V. J. Digricoli","year":"1986","unstructured":"Digricoli, V. J. and Harrison, M. C., Equality-based binary resolution,J. ACM 33(2) (1986), 253?89.","journal-title":"J. ACM"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Digricoli, V. J. and Kochendorfer, E., LIM+ challenge problems by RUE hyper-resolution, Proc. CADE-11, June 1992, pp. 239?52.","DOI":"10.1007\/3-540-55602-8_169"},{"key":"CR4","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1989","unstructured":"Chang, C. and Lee, R.,Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1989."},{"key":"CR5","unstructured":"Digricoli, V. J., Lu, J. and Subrahmanian, V., And-or graphs applied to RUE resolution,IJCAI-89, pp. 354?58."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF00881797","volume":"10","author":"J. J. Lu","year":"1993","unstructured":"Lu, J. J. and Subrahmanian, V. S., Completeness issues IN RUE-NRF deduction: The undecidability of viability,J. Automated Reasoning 10 (1993), 371?88.","journal-title":"J. Automated Reasoning"},{"key":"CR7","unstructured":"Digricoli, V. J., The management of heuristic search in Boolean exp's with RUE resolution,IJCAI-85, pp. 1154?61."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Wos, L. A., Overbeek, R. A. and Henschen, L., Hyperparamodulation ? a refinement of paramodulation,Proc. of CADE-5, 1980, pp. 208?219.","DOI":"10.1007\/3-540-10009-1_17"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Wilson, G. A. and Minker, J., Resolution refinements and search strategies: A comparative study,IEEE Trans. Computers, C-25, No. 8 (Aug. 1976).","DOI":"10.1109\/TC.1976.1674697"},{"key":"CR10","unstructured":"Morris, J. B., E-resolution: An extension of resolution to include the equality relation,IJCAI-69, pp. 287?94."},{"key":"CR11","unstructured":"Robinson, J. A., Automatic deduction with hyperresolution,Int. J. Computational Math., (1965), 227?234."},{"issue":"8","key":"CR12","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. D. McCharen","year":"1976","unstructured":"McCharen, J. D., Overbeek, R. A. and Wos, L., Problems and experiments for and with automated theorem proving programs.IEEE Trans. Computers,C-25, No. 8 (Aug. 1976), 773?82.","journal-title":"IEEE Trans. Computers"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881889.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881889\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881889","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T12:58:11Z","timestamp":1556542691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881889"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":12,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881889"],"URL":"https:\/\/doi.org\/10.1007\/bf00881889","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}