{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:41Z","timestamp":1774837841360,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631040","type":"print"},{"value":"9783540691402","type":"electronic"}],"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_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:04:46Z","timestamp":1330279486000},"page":"57-60","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Integration of automated and interactive theorem proving in ILF"],"prefix":"10.1007","author":[{"given":"B. I.","family":"Dahn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Gehne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Th.","family":"Honigmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Wolf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"J. Avenhaus, J. Denzinger, and Matt. Fuchs. DISCOUNT: A System For Distributed Equational Deduction. In Proc. 6, RTA, pp. 397\u2013402, Springer, 1995.","DOI":"10.1007\/3-540-59200-8_72"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. Br\u00fcning, U. Egly, and T. Rath. KoMeT, system description. In Proc. CADE-12, pp. 783\u2013787, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_60"},{"key":"7_CR3","unstructured":"B. I. Dahn, J. Gehne, Th. Honigmann, L. Walther, and A. Wolf. Integrating Logical Functions with Ilf. TR 94-10, Humboldt Univ. Berlin, Math. Dept., 1994."},{"key":"7_CR4","unstructured":"B. I. Dahn and A. Wolf. A Calculus Supporting Structured Proofs. Journal for Information Processing and Cybernetics (EIK), (5\u20136): pp. 261\u2013276, 1994."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"B. I. Dahn and A. Wolf. Natural Language Presentation and Combination of Automatically Generated Proofs. In Proc. FroCoS'96, pp. 175\u2013192, Kluwer, 1996.","DOI":"10.1007\/978-94-009-0349-4_9"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent Developments (System Abstract). In Proc. CADE-12, pp. 778\u2013782, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_59"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"W. McCune. Otter 2.0. In Proc. CADE-10, pp. 663\u2013664, Springer, 1990.","DOI":"10.1007\/3-540-52885-7_131"},{"key":"7_CR8","first-page":"40","volume":"14","author":"C. S. Mellish","year":"1988","unstructured":"C. S. Mellish. Implementing systemic classification by unification. Comp. Ling., 14:40\u201351, 1988.","journal-title":"Comp. Ling."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. In Proc. CADE-12, pp. 252\u2013266, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede, and G. Rock. Spass & flotter, version 0.42. In Proc. CADE-13, pp. 141\u2013145, Springer, 1996.","DOI":"10.1007\/3-540-61511-3_75"},{"key":"7_CR11","unstructured":"A. Wolf and J. Schumann. ILF-SETHEO. In Proc. CADE-14, accepted paper."}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:45:52Z","timestamp":1558255552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}