{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:07:52Z","timestamp":1725664072782},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540582168"},{"type":"electronic","value":"9783540485735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58216-9_30","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:36:18Z","timestamp":1330252578000},"page":"69-83","source":"Crossref","is-referenced-by-count":9,"title":["On the value of antiprenexing"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"No.2","key":"6_CR1","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 Association for Computing Machinery, 28, No.2:193\u2013214, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"6_CR2","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 Introduc-tion. Annals of Pure and Applied Logic, 57:181\u2013215, 1992.","journal-title":"Annals of Pure and Applied Logic"},{"doi-asserted-by":"crossref","unstructured":"M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae, 1994.","key":"6_CR3","DOI":"10.3233\/FI-1994-2044"},{"key":"6_CR4","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF02239498","volume":"12","author":"W. Bibel","year":"1974","unstructured":"W. Bibel. An Approach to a Systematic Theorem Proving Procedure in First-Order Logic. Computing, 12:43\u201355, 1974.","journal-title":"Computing"},{"key":"6_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving.","author":"W. Bibel","year":"1987","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second edition, 1987.","edition":"second edition"},{"key":"6_CR6","doi-asserted-by":"crossref","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."},{"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.","key":"6_CR7","DOI":"10.1007\/BFb0013057"},{"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.","key":"6_CR8","DOI":"10.1007\/BFb0022565"},{"unstructured":"U. Egly. Function Introduction and the Complexity of Proofs. PhD thesis, TH Darmstadt, Alexanderstr. 10, D-64283 Darmstadt, 1994. Forthcoming.","key":"6_CR9"},{"unstructured":"R. H\u00e4hnle and P. H. Schmitt. The Liberalized \u03b4-Rule in Free Variable Semantic Tableaux. Journal of Automated Reasoning. To appear.","key":"6_CR10"},{"issue":"1","key":"6_CR11","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H. R. Lewis","year":"1978","unstructured":"H. R. Lewis. Renaming a Set of Clauses as a Horn Set. Journal of the ACM, 25(1):134\u2013135, 1978.","journal-title":"Journal of the ACM"},{"volume-title":"volume 6 of Fun-damental Studies in Computer Science","year":"1978","author":"D. W. Loveland","unstructured":"D. W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fun-damental Studies in Computer Science. North-Holland Publishing Company, Amsterdam, New York, Oxford, 1978.","key":"6_CR12"},{"key":"6_CR13","doi-asserted-by":"crossref","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 Transla-tion. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"doi-asserted-by":"crossref","unstructured":"R. Statman. Lower Bounds on Herbrand's Theorem. In Proc. AMS 75, pages 104\u2013107, 1979.","key":"6_CR14","DOI":"10.2307\/2042682"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58216-9_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:12:54Z","timestamp":1619557974000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58216-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582168","9783540485735"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-58216-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}