{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:46:09Z","timestamp":1743147969794,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_25","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:04:06Z","timestamp":1330279446000},"page":"260-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["CODE: A powerful prover for problems of condensed detachment"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Fuchs","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Fuchs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"25_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF00881866","volume":"10","author":"J. Christian","year":"1993","unstructured":"Christian, J.:Flatterms, discrimination nets, and fast term rewriting, JAR 10, 1993, pp. 95\u2013113.","journal-title":"JAR"},{"key":"25_CR2","first-page":"343","volume":"861","author":"J. Denzinger","year":"1994","unstructured":"Denzinger, J.; Fuchs, M.:Goal oriented equational theorem proving using teamwork, Proc. 18th KI-94, Saarbr\u00fccken, GER, Springer LNAI 861, 1994, pp. 343\u2013354.","journal-title":"Springer LNAI"},{"key":"25_CR3","unstructured":"Fuchs, M.:Powerful Search Heuristics Based on Weighted Symbols, Level and Features, Proc. FLAIRS '96, Key West, FL, USA, 1996, pp. 449\u2013453."},{"key":"25_CR4","first-page":"523","volume":"1104","author":"M. Fuchs","year":"1996","unstructured":"Fuchs, M.:Experiments in the Heuristic Use of Past Proof Experience, Proc. CADE-13, New Brunswick, NJ, USA, 1996, Springer LNAI 1104, pp. 523\u2013537.","journal-title":"Springer LNAI"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Graf P.:Term Indexing, Springer Verlag, Springer LNAI 1053, 1995.","DOI":"10.1007\/3-540-61040-5"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T.; Buch, A.; Fettig, R.:On Gaining Efficiency in Completion-Based Theorem Proving, Proc. 7th RTA, 1996, Springer LNCS 1103, pp. 432\u2013435.","DOI":"10.1007\/3-540-61464-8_74"},{"key":"25_CR7","unstructured":"Lukasiewicz, J.:Selected Works, L. Borkowski (ed.), North-Holland, 1970."},{"key":"25_CR8","first-page":"209","volume":"607","author":"W. McCune","year":"1992","unstructured":"McCune, W.; Wos, L.:Experiments in Automated Deduction with Condensed Detachment, Proc. CADE-11, Saratoga Springs, NY, USA, 1992, Springer LNAI 607, pp. 209\u2013223.","journal-title":"Springer LNAI"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"McCune, W.:OTTER 3.0 Reference Manual and Guide, Techn. Report ANL-94\/6, Argonne Natl. Laboratory, 1994.","DOI":"10.2172\/10129052"},{"issue":"Number1","key":"25_CR10","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1305\/ndjfl\/1093888213","volume":"19","author":"G.J. Peterson","year":"1976","unstructured":"Peterson, G.J.:An automatic theorem prover for substitution and detachment systems, Notre Dame Journal of Formal Logic, Vol. 19, Number 1, January 1976, pp. 119\u2013122.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"25_CR11","first-page":"109","volume-title":"Proc. IJCAI '93","author":"J. Slaney","year":"1993","unstructured":"Slaney, J.:SCOTT: A Model-Guided Theorem Prover, Proc. IJCAI '93, Chambery, FRA, 1993, AAAI Press, pp. 109\u2013114."},{"key":"25_CR12","first-page":"252","volume":"814","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G.; Suttner, C.; Yemenis, T.:The TPTP Problem Library, Proc. CADE-12, Nancy, FRA, 1994, Springer LNAI 814, pp. 252\u2013266.","journal-title":"Springer LNAI"},{"key":"25_CR13","unstructured":"Tarski, A.:Logic, Semantics, Metamathematics, Oxford University Press, 1956."},{"key":"25_CR14","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00245821","volume":"6","author":"L. Wos","year":"1990","unstructured":"Wos, L.:Meeting the Challenge of Fifty Years of Logic, JAR 6, 1990, pp. 213\u2013232.","journal-title":"JAR"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF00881802","volume":"15","author":"L. Wos","year":"1995","unstructured":"Wos, L.:Searching for Circles of Pure Proofs, JAR 15, 1995, pp. 279\u2013315.","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:44:29Z","timestamp":1558255469000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}