{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:06Z","timestamp":1749124086925},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_169","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:19:50Z","timestamp":1330233590000},"page":"239-252","source":"Crossref","is-referenced-by-count":2,"title":["LIM+ challenge problems by RUE hyper-resolution"],"prefix":"10.1007","author":[{"given":"Vincent J.","family":"Digricoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eugene","family":"Kochendorfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"No.3","key":"19_CR1","first-page":"341","volume":"6","author":"W.W. Bledsoe","year":"1990","unstructured":"W.W. Bledsoe: Challenge Problems in Elementary Calculus. Jn. Automated Reasoning, Vol. 6, No.3, Sept1990, 341\u2013359.","journal-title":"Jn. Automated Reasoning"},{"key":"19_CR2","unstructured":"J.A.Robinson:Automatic Deduction with Hyperresolution. Int.Journal of Computational Math, 1965, 227\u2013234."},{"issue":"n2","key":"19_CR3","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/5383.5389","volume":"33","author":"V.J. Digricoli","year":"1986","unstructured":"V.J. Digricoli, M.C. Harrison:Equality-Based Binary Resolution. Journal ACM,v33, n2, Apr1986, 253\u2013289.","journal-title":"Journal ACM"},{"key":"19_CR4","unstructured":"V.J.Digricoli:The Management of Heuristic Search in Boolean Exp's with RUE Resolution.IJCAI-85,1154\u20131161."},{"key":"19_CR5","unstructured":"V.J.Digricoli,J.Lu,V.Subrahmanian:And-Or Graphs Applied to RUE Resolution.IJCAI-89,354\u2013358."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"L.A.Wos,R.A.Overbeek,L.Henschen:Hyperparamodulation-a Refinement of Paramodulation.CADE-5,1980,208\u2013219.","DOI":"10.1007\/3-540-10009-1_17"},{"key":"19_CR7","unstructured":"J.B.Morris:E-Resolution:an Extension of Resolution to Include the Equality Relation.IJCAI-69,287\u2013294."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"G.G.Birkhoff:Distributive Postulates for Systems Like Boolean Algebra.Trans Am Math Society,v60,July\u2013Dec1946.","DOI":"10.1090\/S0002-9947-1946-0017735-7"},{"key":"19_CR9","unstructured":"C.Chang,R.Lee:Symbolic Logic and Mechanical Theorem Proving.Academic Press, 1989."},{"key":"19_CR10","unstructured":"V.J.Digricoli:Resolution by Unification and Equality. Dissertation Courant Institute,February 1983."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_169.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:00:10Z","timestamp":1605628810000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_169"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_169","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}