{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:02:35Z","timestamp":1743022955154,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"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_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:04:49Z","timestamp":1330279489000},"page":"61-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["ILF-SETHEO"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Wolf","sequence":"first","affiliation":[]},{"given":"Johann","family":"Schumann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"8_CR1","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"},{"issue":"3","key":"8_CR2","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. Boyer","year":"1986","unstructured":"R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set theory in first-order logic: Clauses for G\u00f6del's axioms. JAR, 2(3): pp. 287\u2013327, 1986.","journal-title":"JAR"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"B. I. Dahn, J. Gehne, Th. Honigmann and A. Wolf. Integration of Automated and Interactive Theorem Proving in ILF. In this volume, 1997.","DOI":"10.1007\/3-540-63104-6_7"},{"key":"8_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":"8_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":"8_CR6","doi-asserted-by":"crossref","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39, 1939.","DOI":"10.1007\/BF01201353"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Chr. 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":"8_CR8","doi-asserted-by":"crossref","unstructured":"X. Huang. Reconstructing Proofs at the Assertion Level. In Proc. CADE-12, pp. 738\u2013752, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_53"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. JAR, (13): pp. 297\u2013337, 1994.","DOI":"10.1007\/BF00881947"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. JAR, 8(2): pp. 183\u2013212, 1992.","journal-title":"JAR"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"J. Schumann Automatic Verification of Cryptographic Protocols with SETHEO In this volume, 1997.","DOI":"10.1007\/3-540-63104-6_12"},{"key":"8_CR12","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":"8_CR13","unstructured":"A. Wolf. A Translation of Model Elimination Proofs into a Structured Natural Deduction. FLAIRS-97, Daytona Beach, 1997."}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:31:59Z","timestamp":1578508319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_8"}},"subtitle":["Processing model elimination proofs for natural language output"],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_8","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"}}]}}