{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T16:24:58Z","timestamp":1648571098537},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540633853","type":"print"},{"value":"9783540698067","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63385-5_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:25:15Z","timestamp":1330298715000},"page":"140-152","source":"Crossref","is-referenced-by-count":1,"title":["Structuring of computer-generated proofs by cut introduction"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]},{"given":"Karin","family":"Genther","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P. B. Andrews","year":"1971","unstructured":"P. B. Andrews. Resolution in Type Theory. J. Symbolic Logic, 36:414\u2013432, 1971.","journal-title":"J. Symbolic Logic"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"P. B. Andrews. Transforming Matings into Natural Deduction Proofs. In W.Bibel and R. Kowalski, editors, Proceedings of the 5th Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 281\u2013292. Springer Verlag, 1980.","DOI":"10.1007\/3-540-10009-1_22"},{"issue":"2","key":"12_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"P. B. Andrews. Theorem Proving via General Matings. Journal of the ACM, 28(2):193\u2013214, 1981.","journal-title":"Journal of the ACM"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"M. Baaz, C. Ferm\u00fcller, and A. Leitsch. A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation. In Proceedings of the Logic in ] Computer Science Conference, pages 213\u2013219, 1994.","DOI":"10.1109\/LICS.1994.316070"},{"key":"12_CR5","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0168-0072(92)90042-X","volume":"57","author":"M. Baaz","year":"1992","unstructured":"M. Baaz and A. Leitsch. Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic, 57:181\u2013215, 1992.","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR6","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1994","unstructured":"M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae, 20:353\u2013379, 1994.","journal-title":"Fundamenta Informaticae"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"12_CR8","volume-title":"Deduction: Automated Logic","author":"W. Bibel","year":"1993","unstructured":"W. Bibel. Deduction: Automated Logic. Academic Press, London, 1993."},{"key":"12_CR9","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","volume":"53","author":"S. R. Buss","year":"1991","unstructured":"S. R. Buss. The Undecidability of k-Provability. Annals of Pure and Applied Logic, 53:75\u2013102, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR10","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"C. L. Chang and R. C. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973."},{"key":"12_CR11","doi-asserted-by":"crossref","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.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"U. Egly. Shortening Proofs by Quantifier Introduction. In A. Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 148\u2013159. Springer Verlag, 1992.","DOI":"10.1007\/BFb0013057"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"U. Egly.On Different Concepts of Function Introduction. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Proceedings of the Kurt G\u00f6del Colloquium, pages 172\u2013183. Springer Verlag, 1993.","DOI":"10.1007\/BFb0022565"},{"key":"12_CR14","unstructured":"U. Egly. On Methods of Function Introduction and Related Concepts. PhD thesis, TH Darmstadt, Alexanderstr. 10, D-64283 Darmstadt, 1994."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"U. Egly. On the Value of Antiprenexing. In F. Pfenning, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 69\u201383. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58216-9_30"},{"key":"12_CR16","doi-asserted-by":"crossref","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"},{"key":"12_CR17","unstructured":"A. P. Felty. Using Extended Tactics to do Proof Transformations. Technical Report MS-CIS-86-89 ZINC LAB 48, Department of Computer and Information Science, Moore School, University of Pennsylvania, Philadelphia, PA 19104, 1986."},{"key":"12_CR18","unstructured":"K. Genther. Repr\u00e4sentation von Konnektionsbeweisen in Gentzen-Kalk\u00fclen durch Transformation und Strukturierung. Master's thesis, TH Darmstadt, 1995."},{"key":"12_CR19","doi-asserted-by":"crossref","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: \u201cInvestigations into Logical Deduction\u201d in [27], pp. 68\u2013131.","journal-title":"Mathematische Zeitschrift"},{"issue":"6","key":"12_CR20","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1093\/jigpal\/3.6.827","volume":"3","author":"J. Goubault","year":"1995","unstructured":"J. Goubault. A BDD-Based Simplification and Skolemization Procedure. J. of the IGPL, 3(6):827\u2013855, 1995.","journal-title":"J. of the IGPL"},{"key":"12_CR21","unstructured":"C. Lingenfelder. Transformation and Structuring of Computer Generated Proofs. Technical Report SR-90-26, Universit\u00e4t Kaiserslautern, 1990."},{"key":"12_CR22","unstructured":"D. Miller and A. Felty. An Integration of Resolution and Natural Deduction Theorem Proving. In T. Kehler, S. Rosenschein, R. Folman, and P. F. Patel-Schneider, editors, Proceedings of the 5th AAAI National Conference on Artificial Intelligence, pages 198\u2013202. Morgan Kaufmann Publishers, 1986."},{"key":"12_CR23","unstructured":"D. A. Miller. Proofs in Higher-Order Logic. Technical Report MS-CIS-83-37, Department of Computer and Information Science, Moore School, University of Pennsylvania, Philadelphia, PA 19104, 1983."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"D. A. Miller. Expansion Tree Proofs and their Conversion to Natural Deduction Proofs. In R. E. Shostak, editor, Proceedings of the 7th Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 375\u2013393. Springer Verlag, 1984.","DOI":"10.1007\/978-0-387-34768-4_22"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"F. Pfenning and D. Nesmith. Presenting Intuitive Deductions via Symmetric Simplification. In M. E. Stickel, editor, Proceedings of the 10th Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 226\u2013350. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_98"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"R. Statman. Lower Bounds on Herbrand's Theorem. In Proc. AMS 75, pages 104\u2013107, 1979.","DOI":"10.2307\/2042682"},{"key":"12_CR27","volume-title":"The Collected Papers of Gerhard Gentzen","year":"1969","unstructured":"M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63385-5_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:43:58Z","timestamp":1619574238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63385-5_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633853","9783540698067"],"references-count":27,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-63385-5_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1997]]}}}