{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T21:46:32Z","timestamp":1649195192268},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"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":[[1993]]},"DOI":"10.1007\/bf00881797","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:36:06Z","timestamp":1104132966000},"page":"371-388","source":"Crossref","is-referenced-by-count":1,"title":["Completeness issues in RUE-NRF deduction: The undecidability of viability"],"prefix":"10.1007","volume":"10","author":[{"given":"James J.","family":"Lu","sequence":"first","affiliation":[]},{"given":"V. S.","family":"Subrahmanian","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"Blair, H. A., ?Canonical conservative extensions of logic program completions?,Proc. 4th IEEE Symp. on Logic Programming, IEEE Computer Society Press, pp. 154?161 (1987)."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(89)90126-6","volume":"68","author":"H. A. Blair","year":"1989","unstructured":"Blair, H. A. and Subrahmanian, V.S., ?Paraconsistent logic programming?,Theoretical Computer Science 68, 135?154 (1989).","journal-title":"Theoretical Computer Science"},{"key":"CR3","unstructured":"Chang, C. L. and Lee, R. C. T.,Symbolic Logic and Mechanical Theorem Proving, Academic Press (1973)."},{"issue":"2","key":"CR4","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?,JACM 33(2), 253?289 (1986).","journal-title":"JACM"},{"key":"CR5","unstructured":"Digricoli, V. J., Lu, J. J. and Subrahmanian, V. S., ?And-Or graphs applied to RUE-resolution,Proc. IJCAI-89, 354?358 (1989)."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Lloyd, J. W.,Foundations of Logic Programming, Springer-Verlag (1987).","DOI":"10.1007\/978-3-642-83189-8"},{"key":"CR7","unstructured":"Lu, J. J. and Subrahmanian, V. S., ?Completeness issues in RUE-NRF deduction?, LPRG-TR-88-24, Syracuse University (1988)."},{"key":"CR8","unstructured":"Lim, Y. and Henschen, L. J., ?A new hyperparamodulation strategy for the equality relation?,Proc. IJCAI, 1138?1145 (1985)."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Mancarella, P. and Pedreschi, D., ?An algebra of logic programs?,Proc. 5th Intl. Conf. and Symp. on Logic Programming (eds. K. Bowen and R. Kowalski), MIT Press, pp. 1006?1023 (1988).","DOI":"10.1016\/0743-1066(88)90013-1"},{"key":"CR10","unstructured":"Mancarella, P., Pedreschi, D., Rondinelli, M. and Tagliatti, M., ?Algebraic properties of a class of logic programs?,Proc. of the 1990 North American Conference on Logic Programming (eds. S. Debray and M. Hermenegildo), MIT Press, pp. 23?39 (1990)."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"McCune, W. W., ?Negative paramodulation?,Proc. 8th Conf. on Automated Deduction, Lecture Notes in Computer Science Vol. 230, Springer-Verlag, pp. 229?239 (1986).","DOI":"10.1007\/3-540-16780-3_93"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/BF00244271","volume":"1","author":"W.W. McCune","year":"1985","unstructured":"McCune, W.W. and Henschen, L.J., ?Experiments with semantic paramodulation?,J. Automated Reasoning 1, 231?261 (1985).","journal-title":"J. Automated Reasoning"},{"key":"CR13","unstructured":"Morris, J. B., ?E-resolution: an extension of resolution to include the equality relation?,Proc. 1st IJCAI, Washington DC, pp. 287?294 (1989)."},{"key":"CR14","unstructured":"Sebelik, J. and Stepanek, P., ?Horn clause programs for recursive functions?, in:Logic Programming (eds. K. Clark and S. A. Tarnlund), Academic Press, pp. 324?340 (1982)."},{"key":"CR15","unstructured":"Wos, L. and Robinson, G. A., ?Paramodulation and theorem proving in first order theories with equality, in:Machine Intelligence 4 (eds. B. Meltzer and D. Michie), pp. 135?150 (1969)."},{"key":"CR16","unstructured":"Wos, L., Overbeek, R. and Henschen, L., ?Hyperparamodulation: A refinement of paramodulation, inProc. 5th Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 87, Springer-Verlag, pp. 208?219 (1980)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881797.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881797\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881797","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:54:00Z","timestamp":1586044440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881797"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881797"],"URL":"https:\/\/doi.org\/10.1007\/bf00881797","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}