{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:20:59Z","timestamp":1743135659888,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"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_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:03:49Z","timestamp":1330297429000},"page":"116-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Some pitfalls of LK-to-LJ translations and how to avoid them"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-84222-0","volume-title":"Relative Complexities of First Order Calculi","author":"E. Eder","year":"1992","unstructured":"E. Eder. Relative Complexities of First Order Calculi. Vieweg, Braunschweig, 1992."},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1006\/jsco.1996.0044","volume":"22","author":"U. Egly","year":"1996","unstructured":"U. Egly. On Different Structure-preserving Translations to Normal Form. J. Symbolic Computation, 22:121\u2013142, 1996.","journal-title":"J. Symbolic Computation"},{"issue":"1","key":"14_CR3","doi-asserted-by":"crossref","first-page":"165","DOI":"10.3233\/FI-1997-291208","volume":"29","author":"U. Egly","year":"1997","unstructured":"U. Egly. On Definitional Translations to Normal Form for Intuitionistic Logic. Fundamenta Informaticae, 29(1,2):165\u2013201, 1997.","journal-title":"Fundamenta Informaticae"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935. English translation in [13].","journal-title":"Mathematische Zeitschrift"},{"issue":"2","key":"14_CR5","doi-asserted-by":"publisher","first-page":"385","DOI":"10.2307\/2274689","volume":"56","author":"G. Mints","year":"1991","unstructured":"G. Mints. Proof Theory in the USSR 1925\u20131969. J. Symbolic Logic, 56(2):385\u2013424, 1991.","journal-title":"J. Symbolic Logic"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"G. Mints. Resolution Strategies for the Intuitionistic Logic. In B. Mayoh, E. Tyugu, and J. Penyam, editors, Constraint Programming, Nato ASI Series, pages 289\u2013311. Springer Verlag, 1994.","DOI":"10.1007\/978-3-642-85983-0_11"},{"key":"14_CR7","unstructured":"V. P. Orevkov. On Glivenko Sequent Classes. In V. P. Orevkov, editor, The calculi of Symbolic Logic I, volume 98, pages 147\u2013173. Steklov Institute of Mathematics, 1971."},{"key":"14_CR8","first-page":"137","volume":"88","author":"V. P. Orevkov","year":"1979","unstructured":"V. P. Orevkov. Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR, 88:137\u2013161, 1979. English translation in J. Soviet Mathematics, 2337\u20132350, 1982.","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. J. Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"J. Symbolic Computation"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"D. Pym, E. Ritter, and L. Wallen. On the Intuitionistic Force of Classical Search. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, pages 295\u2013311. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61208-4_19"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"D. Pym, E. Ritter, and L. Wallen. Proof-Terms for Classical and Intuitionistic Resolution. In M.A. McRobbie and J. K. Slaney, editors, Proceedings of the Conference on Automated Deduction, pages 17\u201331. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_66"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","unstructured":"R. Statman. Intuitionistic Propositional Logic is Polynomial-Space Complete. J. Theoretical Computer Science, 9:67\u201372, 1979.","journal-title":"J. Theoretical Computer Science"},{"key":"14_CR13","unstructured":"M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1969."},{"key":"14_CR14","unstructured":"G. Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1975."},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning, pages 466\u2013483. Springer Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Theorem Proving in Non-standard Logics Based on the Inverse Method. In D. Kapur, editor, Proceedings of the Conference on Automated Deduction, pages 648\u2013662. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_198"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,3]],"date-time":"2020-07-03T07:31:14Z","timestamp":1593761474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_14","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"}}]}}