{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:01Z","timestamp":1776333421159,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646754","type":"print"},{"value":"9783540691105","type":"electronic"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054276","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"427-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Towards efficient subsumption"],"prefix":"10.1007","author":[{"given":"Tanel","family":"Tammet","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, N. Zamov. Resolution methods for decision problems. Lecture Notes in Artificial Intelligence vol. 679, Springer Verlag, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"P. Graf. Term Indexing. Lecture Notes in Computer Science. 1053, Springer Verlag, 1996.","DOI":"10.1007\/3-540-61040-5"},{"issue":"2","key":"37_CR3","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1985","unstructured":"G. Gottlob, A. Leitsch. On the efficiency of subsumption algorithms, Journa of ACM\n                        32(2):280\u2013295, April 1985.","journal-title":"Journa of ACM"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"L. Magnusson, B. Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for Proofs and Programs, pages 213\u2013237, Lecture Notes in Computer Science vol. 806, Springer Verlag, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"37_CR5","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/BF01051768","volume":"2","author":"G. Mints","year":"1993","unstructured":"G. Mints. Resolution Calculus for The First Order Linear Logic. Journal of Logic, Language and Information, 2, 58\u201393 (1993).","journal-title":"Journal of Logic, Language and Information"},{"key":"37_CR6","volume-title":"Tech. Report ANL-94\/6","author":"W. McCune","year":"1994","unstructured":"W. McCune. OTTER 3.0 Reference Manual and Users Guide. Tech. Report ANL-94\/6, Argonne National Laboratory, Argonne, IL, January 1994."},{"issue":"2","key":"37_CR7","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"W. McCune. Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147\u2013167, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"37_CR8","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1093\/logcom\/5.4.449","volume":"4","author":"T. Tammet","year":"1995","unstructured":"T. Tammet. Completeness of Resolution for Definite Answers. Journal of Logic and Computation, (1995), vol 4 nr 5, 449\u2013471.","journal-title":"Journal of Logic and Computation"},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"T. Tammet. A Resolution Theorem Prover for Intuitionistic Logic. In CADE-13, pages 2\u201316, Lecture Notes in Computer Science vol. 1104, Springer Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_65"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"T. Tammet, J. Smith. Optimised Encodings of Fragments of Type Theory in First Order Logic. In Types for Proofs and Programs, pages 265\u2013287, Lecture Notes in Computer Science vol. 1158, Springer Verlag,1996.","DOI":"10.1007\/3-540-61780-9_75"},{"issue":"2","key":"37_CR11","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2): 199\u2013204, 1997.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054276","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T18:39:08Z","timestamp":1676054348000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0054276","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}