{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:58Z","timestamp":1749125158994,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054274","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"397-411","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["On generating small clause normal forms"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Nonnengart","sequence":"first","affiliation":[]},{"given":"Georg","family":"Rock","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"35_CR1","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"T. B. de la Tour","year":"1992","unstructured":"Thierry Boy de la Tour. An Optimality Result for Clause Form Translation. Journal of Symbolic Computation, 14:283\u2013301, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"35_CR2","unstructured":"Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science and Applied Mathematics. Academic Press, 1973."},{"key":"35_CR3","first-page":"1","volume":"27","author":"L. Dafa","year":"1994","unstructured":"Li Dafa. The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem. Association for Automated Reasoning Newsletter, 27:1\u20137, 1994.","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"35_CR4","first-page":"57","volume-title":"volume 1249 of LNAI","author":"I. Dahn","year":"1997","unstructured":"Ingo Dahn, J. Gehne, Thomas Honigmann, and Andreas Wolf. Integration of Automated and Interactive Theorem Proving in ILF. In Proceedings of the 14th International Conference on Automated Deduction, CADE-14, volume 1249 of LNAI,pages 57\u201360, Townsville, Australia, 1997. Springer."},{"key":"35_CR5","doi-asserted-by":"crossref","unstructured":"Elmar Eder. Relative Complexities of First Order Calculi. Artificial Intelligence. Vieweg, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"Uwe Egly. On the Value of Antiprenexing. In Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, volume 822 of LNAI, pages 69\u201383. Springer, July 1994.","DOI":"10.1007\/3-540-58216-9_30"},{"key":"35_CR7","first-page":"10","volume":"30","author":"U. Egly","year":"1995","unstructured":"Uwe Egly and Thomas Rath. The Halting Problem: An Automatically Generated Proof. AAR Newsletter, 30:10\u201316, 1995.","journal-title":"AAR Newsletter"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"Uwe Egly and Thomas Rath. On the Practical Value of Different Definitional Translations to Normal Form. In M.A. McRobbie and J.K. Slaney, editors, 13th International Conference on Automated Deduction, CADE-13, volume 1104 of LNAI, pages 403\u2013417. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_103"},{"issue":"2","key":"35_CR9","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1985","unstructured":"Georg Gottlob and Alexander Leitsch. On the Efficiency of Subsumption Algorithms. Journal of the ACM, 32(2):280\u2013295, 1985.","journal-title":"Journal of the ACM"},{"key":"35_CR10","unstructured":"Donald W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North-Holland, 1978."},{"issue":"2","key":"35_CR11","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W. McCune","year":"1997","unstructured":"William McCune and Larry Wos. Otter. Journal of Automated Reasoning,18(2):211\u2013220, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR12","volume-title":"Technical Report MPI-I-96-2-010","author":"A. Nonnengart","year":"1996","unstructured":"Andreas Nonnengart. Strong Skolemization. Technical Report MPI-I-96-2-010, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, 1996.http:\/\/www.mpi-sb.mpg.de\/~nonnenga\/publications\/, submitted."},{"issue":"2","key":"35_CR13","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BF00881919","volume":"15","author":"H. J. Ohlbach","year":"1995","unstructured":"Hans J\u00fcrgen Ohlbach and Christoph Weidenbach. A Note on Assumptions about Skolem Functions. Journal of Automated Reasoning, 15(2):267\u2013275, 1995.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"35_CR14","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Francis Jeffry Pelletier. Seventy-Five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2(2):191\u2013216, 1986. Errata: Journal of Automated Reasoning, 4(2):235\u2013236,1988.","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR15","first-page":"8","volume":"31","author":"F. J. Pelletier","year":"1995","unstructured":"Francis Jeffry Pelletier and Geoff Sutcliffe. An Erratum for Some Errata to Automated Theorem Proving Problems. Association for Automated Reasoning Newsletter, 31:8\u201314, December 1995.","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"35_CR16","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"David A. Plaisted and Steven Greenbaum. A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"35_CR17","volume-title":"Transformations of First-Order Formulae for Automated Reasoning","author":"G. Rock","year":"1995","unstructured":"Georg Rock. Transformations of First-Order Formulae for Automated Reasoning.Diplomarbeit, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, April 1995. Supervisors: H.J. Ohlbach, C. Weidenbach."},{"key":"35_CR18","first-page":"4","volume":"4","author":"T. Skolem","year":"1920","unstructured":"Thoralf Skolem. Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit oder Beweisbarkeit mathematischer S\u00c4tze nebst einem Theoreme \u00fcber dichte Mengen. Skrifter utgit av Videnskappsellkapet i Kristiania, 4:4\u201336, 1920. Reprinted in: From Frege to G\u00f6del, A Source Book in Mathematical Logic, 1879-1931, van Heijenoort, Jean, editor, pages 252\u2013263, Harvard University Press, 1976.","journal-title":"Skrifter utgit av Videnskappsellkapet i Kristiania"},{"key":"35_CR19","first-page":"252","volume-title":"volume 814 of Lecture Notes in Artificial Intelligence, LNAI","author":"G. Sutcliffe","year":"1994","unstructured":"Geoff Sutcliffe, Christian B. Suttner, and Theodor Yemenis. The TPTP Problem Library. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, LNAI, pages 252\u2013266, Nancy, France, June 1994. Springer."},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"G.S. Tseitin. On the complexity of derivations in propositional calculus. In A.O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic.1968. Reprinted in: Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, editors, pages 466\u2013483, Springer, 1983.","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"Christoph Weidenbach, Bernd Gaede, and Georg Rock. SPASS & FLOTTER, Version 0.42. In M.A. McRobbie and J.K. Slaney, editors, 13th International Conference on Automated Deduction, CADE-13, volume 1104 of LNAI, pages 141\u2013145.Springer, 1996.","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054274","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,27]],"date-time":"2023-01-27T20:39:24Z","timestamp":1674851964000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054274"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0054274","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}