{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:11Z","timestamp":1725663371948},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_76","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:45:13Z","timestamp":1330206313000},"page":"16-27","source":"Crossref","is-referenced-by-count":6,"title":["A complete semantic back chaining proof system"],"prefix":"10.1007","author":[{"given":"Xumin","family":"Nie","sequence":"first","affiliation":[]},{"given":"David A.","family":"Plaisted","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"2_CR1","first-page":"3","volume":"10","author":"A. Ballantyne","year":"1982","unstructured":"Ballantyne, A. and W.W. Bledsoe, \"On Generating and Using Examples in Proof Discovery\", Machine Intelligence, V 10, pp. 3\u201339, Harwood, Chichester 1982.","journal-title":"Machine Intelligence"},{"key":"2_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90100-2","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1982","unstructured":"Bibel, W., \"Automated Theorem Proving\", Friedr. Vieweg & Sohn Verlagsgesellschaft MbH, Braunschweig 1982."},{"key":"2_CR3","unstructured":"Bledsoe, W.W., \"Using Examples to Generate Instantiations for Set Variables\", Technical Report No. ATP-67, Department of Computer Science, University of Texas at Austin, July 1982."},{"key":"2_CR4","volume-title":"Locking: A Restriction of Resolution","author":"R. Boyer","year":"1970","unstructured":"Boyer, R., \"Locking: A Restriction of Resolution\", Ph.D. dissertation, University of Texas at Austin, Austin, TX, 1970."},{"key":"2_CR5","unstructured":"Gelernter, H., \"Realization of a Geometry Theorem-Proving Machine\", Proc. ICIP, pp. 273\u2013282, Paris UNESCO House, 1959."},{"issue":"3","key":"2_CR6","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D.W. Loveland","year":"1969","unstructured":"Loveland, D.W., \"A Simplified Format for the Model Elimination Theorem-Proving Procedure\", J. ACM, Vol. 16, No. 3, pp. 349\u2013363, July 1969.","journal-title":"J. ACM"},{"key":"2_CR7","first-page":"163","volume-title":"Refinement Theorems in Resolution Theory","author":"D. Luckham","year":"1970","unstructured":"Luckham, D., \"Refinement Theorems in Resolution Theory\", Proc. IRIA Symp. Automatic Demonstration, Versailles, France, 1968, Springer-Verlag, New York, pp. 163\u2013190, 1970."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A., \"Non-Horn Clause Logic Programming Without Contrapositives\", Journal of Automated Reasoning, Vol. 4, Nov. 3, September 1988.","DOI":"10.1007\/BF00244944"},{"issue":"4","key":"2_CR9","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TC.1976.1674613","volume":"C-25","author":"R. Reiter","year":"1976","unstructured":"Reiter, R., \"A Semantically Guided Deductive System for Automatic Theorem Proving\", IEEE Transaction on Computers, Vol. C-25, No. 4, pp. 328\u2013334, April 1976.","journal-title":"IEEE Transaction on Computers"},{"key":"2_CR10","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 the Resolution Principles\", JACM 12, pp. 23\u201341, 1965.","journal-title":"JACM"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Sandford, D.M., \"Using Sophisticated Models in Resolution Theorem Proving\", Lecture Notes in Computer Science, No. 90, G. Goos and J. Hartmanis eds, Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10231-0"},{"issue":"4","key":"2_CR12","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J.R. Slagle","year":"1967","unstructured":"Slagle, J.R., \"Automatic Theorem Proving with Renamable and Semantics Resolution\", JACM, Vol. 14, No. 4, pp. 687\u2013697, October 1967.","journal-title":"JACM"},{"issue":"4","key":"2_CR13","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M.E. Stickel","year":"1988","unstructured":"Stickel, M.E., \"A PROLOG Technology Theorem Prover\", Journal of Automated Reasoning, Vol. 4, No. 4, pp. 353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR14","unstructured":"Walther, C., \"A Mechanical Solution of Schubert's Steamroller by Manysorted Resolution\", Proc. 8th AAAI, pp. 330\u2013334, 1984."},{"key":"2_CR15","unstructured":"Wang, T.C., \"Designing Examples for Semantically Guided Hierarchical Deduction\", Proc. of IJCAI, pp. 1201\u20131207, 1985."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Wang, T.C. and W.W. Bledsoe, \"Hierarchical Deduction\", Journal of Automated Reasoning, Vol. 3, No. 1, 1987.","DOI":"10.1007\/BF00381144"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Wos, L.T., G.A. Robinson and D.F. Carson, \"Efficiency and Completeness of the Set of Support Strategy in Theorem Proving\", J. of ACM, Vol. 12, No. 4, October 1965.","DOI":"10.1145\/321296.321302"}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_76.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:35Z","timestamp":1605648335000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_76"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_76","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}