{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:12Z","timestamp":1725664932412},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540610649"},{"type":"electronic","value":"9783540499442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61064-2_34","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:15:06Z","timestamp":1330272906000},"page":"135-148","source":"Crossref","is-referenced-by-count":1,"title":["Subsumption algorithms based on search trees"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Ta","family":"Chen","sequence":"additional","affiliation":[]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[]},{"given":"I. V.","family":"Ramakrishnan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"11_CR1","volume-title":"Computers and Intractability","author":"M. R. Garey","year":"1979","unstructured":"M. R. Garey and D. S. Johnson. Computers and Intractability. Freeman, San Francisco, 1979."},{"issue":"2","key":"11_CR2","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1987","unstructured":"G. Gottlob and A. Leitsch. On the efficiency of subsumption algorithms. JACM, 32(2):280\u2013295, April 1987.","journal-title":"JACM"},{"key":"11_CR3","volume-title":"Technical Report ANL-94\/6","author":"W. McCune","year":"1994","unstructured":"W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, Ill., 1994."},{"key":"11_CR4","first-page":"252","volume-title":"volume 814 of Lecture Notes in Artificial Intelligence","author":"G. Sutcliffe","year":"1994","unstructured":"Geoff Sutcliffe, Christian Suttner, and Theodor Yemenis. The TPTP problem library. In Proc. 12th Int. Conf. on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 252\u2013266. Springer-Verlag, Berlin, 1994."},{"issue":"4","key":"11_CR5","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1145\/321784.321792","volume":"20","author":"R. B. Stillman","year":"1973","unstructured":"R. B. Stillman. The concept of weak substitution in theorem-proving. JACM, 20(4):648\u2013667, 1973.","journal-title":"JACM"},{"key":"11_CR6","unstructured":"L. Wos, R. Overbeek, and E. Lusk. Subsumption, a sometimes undervalued procedure. In J.-L. Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 3\u201340. MIT Press, 1991."}],"container-title":["Lecture Notes in Computer Science","Trees in Algebra and Programming \u2014 CAAP '96"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61064-2_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:29:13Z","timestamp":1619558953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61064-2_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540610649","9783540499442"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/3-540-61064-2_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}