{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:54:47Z","timestamp":1725663287454},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540505174"},{"type":"electronic","value":"9783540460305"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50517-2_93","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:26:41Z","timestamp":1330183601000},"page":"400-418","source":"Crossref","is-referenced-by-count":1,"title":["A resolution rule for well-formed formulae"],"prefix":"10.1007","author":[{"given":"K. S. H. S. R.","family":"Bhatta","sequence":"first","affiliation":[]},{"given":"Harish","family":"Karnick","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Bhatta, K.S.H.S.R. Many-Sorted Resolution for Well-Formed Formulae with Equality, M. Tech. Dissertation, I.I.T. Kanpur, 1988.","DOI":"10.1007\/3-540-50517-2_93"},{"key":"27_CR2","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, Orlando, Fla., 1973."},{"key":"27_CR3","unstructured":"Manna, Z., and Waldinger, R. Special Relations in Program-Synthetic Deduction, Tech. Report, Comp. Sci. Dept., Stanford Univ., Stanford, California, and Artificial Intelligence Center, SRI International, Menlo Park, California, March 1982."},{"issue":"1","key":"27_CR4","first-page":"67","volume":"18","author":"N.V. Murray","year":"1982","unstructured":"Murray, N.V. \"Completely Non-Clausal Theorem Proving\", A1 18(1), 1982, pp.67\u201385.","journal-title":"A1"},{"key":"27_CR5","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. of Automated Reasoning 2, 1986, pp. 191\u2013216.","journal-title":"J. of Automated Reasoning"},{"key":"27_CR6","volume-title":"Methods of Logic","author":"W.V. Quine","year":"1961","unstructured":"Quine, W.V. Methods of Logic, Holt, Rinehart and Winston Inc., New York, 1961."},{"issue":"1","key":"27_CR7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A. \"A Machine-oriented Logic Based on Resolution Principle\", JACM 12(1), 1965, pp.23\u201341.","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50517-2_93.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:56:19Z","timestamp":1619556979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50517-2_93"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540505174","9783540460305"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-50517-2_93","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}