{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:51Z","timestamp":1725663171683},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_94","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:58:58Z","timestamp":1330196338000},"page":"240-253","source":"Crossref","is-referenced-by-count":0,"title":["The heuristics and experimental results of a new hyperparamodulation: HL-resolution"],"prefix":"10.1007","author":[{"given":"Younghwan","family":"Lim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"20_CR1","unstructured":"Blasius, K. H., \"Equality Reasoning in Clause Graph,\" IJCAI, 1983."},{"key":"20_CR2","unstructured":"Darlington, J. L., \"Automated Theorem Proving with Equality Substitutions and Mathematical Induction,\" in Machine Intelligence, Vol. 3 (B. Meltzer and D. Michie, eds.), American Elsevier, New York, pp. 113\u2013127."},{"key":"20_CR3","unstructured":"Digricoli, V. J., \"Resolution by unification and Equality,\" Proceedings of 4th Workshop on Automated Deduction, 1979."},{"issue":"3","key":"20_CR4","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/322077.322078","volume":"25","author":"M. Harrison","year":"1978","unstructured":"Harrison, M. and N. Rubin, \"Another Generalization of Resolution,\" J. ACM, Vol. 25, No. 3, July 1978, pp.341\u2013351.","journal-title":"J. ACM"},{"key":"20_CR5","unstructured":"Lim, Younghwan, A New Hyperparamodulation Strategy for the Equality Clauses, Ph. D. Dissertation at Northwestern University, 1985."},{"key":"20_CR6","unstructured":"Younghwan Lim and Lawrence J. Henschen, \"A New Hyperparamodulation Strategy for the Equality Relation,\" IJCAI 85, pp. 1138\u20131145."},{"key":"20_CR7","unstructured":"McCune, W., Semantic Paramodulation for Horn Sets, Ph.D. Sissertation at Northwestern University, 1984."},{"key":"20_CR8","unstructured":"Morris, J., \"E-resolution: an Extension of Resolution to Include the Equality Relation,\" IJCAI, 1969."},{"issue":"1-A","key":"20_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","volume":"2","author":"R. Overbeek","year":"1976","unstructured":"Overbeek, R., J. McCharen and L. Wos, \"Complexity and Related Enhancements for Atomated Theorem-proving Program,\" Comp. and Maths. with Appls., Vol. 2, No. 1-A, 1976, pp.1\u201316.","journal-title":"Comp. and Maths. with Appls."},{"key":"20_CR10","first-page":"135","volume-title":"Machine Intelligence Vol. 4","author":"G. A. Robinson","year":"1969","unstructured":"Robinson, G. A. and L. Wos, \"Paramodulation and Theorem Proving in First Order Theories with Equality,\" in Machine Intelligence Vol. 4 (B. Meltzer and D. Michie, eds) Amerian Elsever, New York, 1969, pp.135\u2013150."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Siekmann, J. and G. Wrightson, \"Paramoulated Connection Graphs,\" Acta Informatica, 1980","DOI":"10.1007\/BF00288537"},{"key":"20_CR12","unstructured":"Wos, L., \"Paramodulation and Set of Support,\" the IRIA Symposium on Automatic Demonstration ar Versailles, 1968."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Wos, L., R. Overbeek and L. Henschen, \"HYPERPARAMODULATION: A Refinement of Paramodulation, \"Proceedings of the 5th Conference on Automated Deduction, 1980, pp.208\u2013219.","DOI":"10.1007\/3-540-10009-1_17"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_94.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:07:25Z","timestamp":1619557645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_94"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_94","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}