{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:34Z","timestamp":1725568174711},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_33","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"365-379","source":"Crossref","is-referenced-by-count":1,"title":["Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms"],"prefix":"10.1007","author":[{"given":"Hans","family":"de Nivelle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/LICS.2001.932490","volume-title":"Proceedings of the 16-th Annual IEEE Symposion on Logic in Computer Science, LICS","author":"J. Avigad","year":"2001","unstructured":"Avigad, J.: Eliminating definitions and skolem functions in first-order logic. In: Mairson, H. (ed.) Proceedings of the 16-th Annual IEEE Symposion on Logic in Computer Science, LICS, Boston, Massachusetts, pp. 139\u2013146. IEEE Computer Society, Los Alamitos (2001)"},{"key":"33_CR2","first-page":"275","volume-title":"Handbook of Automated Reasoning","author":"M. Baaz","year":"2001","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 5, pp. 275\u2013333. Elsevier Science B.V, Amsterdam (2001)"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Baaz, M., Ferm\u00fcller, C.G., Leitsch, A.: A non-elementary speed-up in proof length by structural clause form transformation. In: IEEE Symposion on Logic in Computer Science 1994, pp. 213\u2013219 (1994)","DOI":"10.1109\/LICS.1994.316070"},{"issue":"20","key":"33_CR4","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"4","author":"M. Baaz","year":"1994","unstructured":"Baaz, M., Leitsch, A.: On skolemization and proof complexity. Fundamenta Informatika\u00a04(20), 353\u2013379 (1994)","journal-title":"Fundamenta Informatika"},{"key":"33_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 2, pp. 19\u2013100. Elsevier Science B.V, Amsterdam (2001)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/3-540-52885-7_106","volume-title":"10th International Conference on Automated Deduction","author":"D. Benanav","year":"1990","unstructured":"Benanav, D.: Simultaneous paramodulation. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 442\u2013455. Springer, Heidelberg (1990)"},{"key":"33_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/10721959_10","volume-title":"Automated Deduction - CADE-17","author":"M. Bezem","year":"2000","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 148\u2013163. Springer, Heidelberg (2000)"},{"issue":"3-4","key":"33_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. Journal of Automated Reasoning\u00a029(3-4), 253\u2013275 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Clote, P., Kraj\u00ed\u010dek, J.: Arithmetic, Proof Theory and Computational Complexity. Oxford Logic Guides, vol.\u00a023. Oxford Science Publications (1993)","DOI":"10.1093\/oso\/9780198536901.001.0001"},{"key":"33_CR10","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"T.B. Tour de la","year":"1992","unstructured":"de la Tour, T.B.: An optimality result for clause form transformation. Journal of Symbolic Computation\u00a014, 283\u2013301 (1992)","journal-title":"Journal of Symbolic Computation"},{"key":"33_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1007\/3-540-45793-3_39","volume-title":"Computer Science Logic","author":"H. Nivelle de","year":"2002","unstructured":"de Nivelle, H.: Extraction of proofs from the clausal normal form transformation. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS (LNAI), vol.\u00a02471, pp. 584\u2013598. Springer, Heidelberg (2002)"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/3-540-61532-6_34","volume-title":"PRICAI \u201996: Topics in Artificial Intelligence","author":"X. Huang","year":"1996","unstructured":"Huang, X.: Translating machine-generated resolution proofs into ND-proofs at the assertion level. In: Foo, N.Y., G\u00f6bel, R. (eds.) PRICAI 1996. LNCS, vol.\u00a01114, pp. 399\u2013410. Springer, Heidelberg (1996)"},{"key":"33_CR13","unstructured":"McCune, W., Shumsky, O.: Ivy: A preprocessor and proof checker for first-order logic. In: Kaufmann, M., Manolios, P., Moore, J. (eds.) Using the ACL2 Theorem Prover: A tutorial Introduction and Case Studies. Kluwer Academic Publishers, Dordrecht (2002); preprint: ANL\/MCS-P775-0899, Argonne National Labaratory, Argonne"},{"key":"33_CR14","unstructured":"Nonnengart, A.: Strong skolemization. Technical Report MPI-I-96-2-010, Max Planck Institut f\u00fcr Informatik Saarbr\u00fccken (1996)"},{"key":"33_CR15","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 6, pp. 335\u2013367. Elsevier Science B.V., Amsterdam (2001)"},{"key":"#cr-split#-33_CR16.1","unstructured":"Orevkov, V.P.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta Imenyi V.A. Steklova AN SSSR\u00a088, 137\u2013161 (1979);"},{"key":"#cr-split#-33_CR16.2","unstructured":"English translation in Journal of Soviet Mathematics, 2337\u20132350 (1982)"},{"key":"33_CR17","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/BFb0047133","volume-title":"7th International Conference on Automated Deduction","author":"F. Pfenning","year":"1984","unstructured":"Pfenning, F.: Analytic and non-analytic proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS (LNAI), vol.\u00a0170, pp. 394\u2013413. Springer, Heidelberg (1984)"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Statman, R.: Lower bounds on herbrand\u2019s theorem. In: Proceedings of the American Mathematical Society, vol.\u00a075-1, pp. 104\u2013107. American Mathematical Society (June 1979)","DOI":"10.2307\/2042682"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,31]],"date-time":"2024-03-31T20:35:16Z","timestamp":1711917316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}