{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:08Z","timestamp":1725664208581},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_103","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:48Z","timestamp":1330293048000},"page":"403-417","source":"Crossref","is-referenced-by-count":5,"title":["On the practical value of different definitional translations to normal form"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Rath","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"issue":"2","key":"40_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"P. Andrews. Theorem Proving via General Matings. JACM, 28(2):193\u2013214, 1981.","journal-title":"JACM"},{"key":"40_CR2","unstructured":"M. Baaz, C. Ferm\u00fcller, and A. Leitsch. A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation. In LICS, 1994."},{"key":"40_CR3","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, second edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"40_CR4","unstructured":"W. Bibel, S. Br\u00fcning, U. Egly, and T. Rath. Towards an Adequate Theorem Prover Based on the Connection Method. In Proceedings of the Sixth International Conference on Artificial Intelligence and Information-Control of Robots, pages 137\u2013148. World Scientific Publishing Company, 1994."},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"W. Bibel and E. Eder. Methods and Calculi for Deduction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, pages 67\u2013182. Oxford University Press, 1993.","DOI":"10.1093\/oso\/9780198537458.003.0003"},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour. Minimizing the Number of Clauses by Renaming. In Mark E. Stickel, editor, Proceedings of the Conference on Automated Deduction, Lecture Notes in Computer Science, pages 558\u2013572. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_114"},{"key":"40_CR7","unstructured":"M. Bruschi. The Halting Problem. AAR Newsletter, pages 7\u201312, March 1991."},{"key":"40_CR8","doi-asserted-by":"crossref","unstructured":"A. Bundy, editor. Proceedings of the Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, Springer Verlag, 1994.","DOI":"10.1007\/3-540-58156-1"},{"issue":"3","key":"40_CR9","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/24658.24665","volume":"18","author":"L. Burkholder","year":"1987","unstructured":"L. Burkholder. The Halting Problem. SIGACT News, 18(3):48\u201360, 1987.","journal-title":"SIGACT News"},{"key":"40_CR10","doi-asserted-by":"crossref","unstructured":"Heng Chu and D. A. Plaisted. Semantically Guided First-Order Theorem Proving using Hyper-Linking. In [8], pages 192\u2013206.","DOI":"10.1007\/3-540-58156-1_14"},{"key":"40_CR11","unstructured":"L. Dafa. A Mechanical Proof of the Halting Problem in Natural Deduction Style. AAR Newsletter, pages 4\u20139, June 1993."},{"key":"40_CR12","unstructured":"L. Dafa. The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem. AAR Newsletter, pages 1\u20137, October 1994."},{"key":"40_CR13","unstructured":"E. Eder. An Implementation of a Theorem Prover Based on the Connection Method. In W. Bibel and B. Petkoff, editors, AIMSA 84. North-Holland, 1984."},{"key":"40_CR14","doi-asserted-by":"crossref","unstructured":"E. Eder. Relative Complexities of First Order Calculi. Vieweg, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"40_CR15","volume-title":"PhD thesis","author":"U. Egly","year":"1994","unstructured":"U. Egly. On Methods of Function Introduction and Related Concepts. PhD thesis, TH Darmstadt, Alexanderstr. 10, D-64283 Darmstadt, 1994."},{"key":"40_CR16","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":"40_CR17","doi-asserted-by":"crossref","unstructured":"U. Egly. On Different Structure-Preserving Translations to Normal Form, 1996. Submitted.","DOI":"10.1006\/jsco.1996.0044"},{"key":"40_CR18","first-page":"10","volume":"30","author":"U. Egly","year":"1995","unstructured":"U. Egly and T. Rath. The Halting Problem: An Automatically Generated Proof. AAR Newsletter, 30:10\u201316, 1995.","journal-title":"AAR Newsletter"},{"key":"40_CR19","doi-asserted-by":"crossref","unstructured":"S. Greenbaum, A. Nagasaka, P. O'Rorke, and D. Plaisted. Comparison of Natural Deduction and Locking Resolution Implementations. In D. W. Loveland, editor, Proceedings of the Conference on Automated Deduction, Lecture Notes in Computer Science, pages 159\u2013171. Springer Verlag, 1982.","DOI":"10.1007\/BFb0000058"},{"key":"40_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13:297\u2013337, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"40_CR21","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BF00881919","volume":"15","author":"H. J. Ohlbach","year":"1995","unstructured":"H. J. Ohlbach and C. Weidenbach. A Note on Assumptions about Skolem Functions. Journal of Automated Reasoning, 15:267\u2013275, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"40_CR22","first-page":"8","volume":"31","author":"F. J. Pelletier","year":"1995","unstructured":"F. J. Pelletier and G. Sutcliffe. An Erratum for Some Errata to Automated Theorem Proving Problems, AAR Newsletter, 31:8\u201314, 1995.","journal-title":"AAR Newsletter"},{"key":"40_CR23","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 Translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"40_CR24","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Technical Note 464, SRI International, 1989.","DOI":"10.1007\/3-540-52531-9_135"},{"key":"40_CR25","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, Ch. Suttner, and T. Yemenis. The TPTP Problem Library. In [8], pages 252\u2013266.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"40_CR26","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"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_103.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:32:21Z","timestamp":1713634341000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_103","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}