{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:09:24Z","timestamp":1725728964680},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_7","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"109-125","source":"Crossref","is-referenced-by-count":1,"title":["Computing Tiny Clause Normal Forms"],"prefix":"10.1007","author":[{"given":"Noran","family":"Azmy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"SPASS Current Prototypes and Experiments, \n                  \n                    http:\/\/www.spass-prover.org\/prototypes\/index.html"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal Form Transformations. In: Voronkov, A., Robinson, A. (eds.) Handbook of Automated Reasoning, ch. 5, pp. 273\u2013333","DOI":"10.1016\/B978-044450813-3\/50007-2"},{"key":"7_CR3","unstructured":"Biere, A., Heule, M., Maaren, H.V., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (2009)"},{"issue":"4","key":"7_CR4","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"Thierry Boy de la Tour. An Optimality Result for Clause Form Translation","year":"1992","unstructured":"Thierry Boy de la Tour. An Optimality Result for Clause Form Translation. Journal of Symbolic Computation\u00a014(4), 283\u2013301 (1992)","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR5","unstructured":"Henschen, L., Lusk, E., Overbeek, R., Smith, B.T., Veroff, R., Winker, S., Wos, L.: Challenge Problem 1. SIGART Newsletter\u00a0(72), 30\u201331 (1980)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for bounded domains. In: Bonacina, M.P., Stickel, M.E. (eds.) McCune Festschrift. LNCS (LNAI), vol.\u00a07788, pp. 68\u2013100. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36675-8_4"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing Small Clause Normal Forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 6, pp. 337\u2013367 (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"issue":"3","key":"7_CR8","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A Structure-preserving Clause Form Translation. Journal of Symbolic Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR9","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library for Automated Theorem Provers (September 2010), \n                  \n                    http:\/\/www.tptp.org\/"},{"issue":"115-125","key":"7_CR10","first-page":"234","volume":"8","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a08(115-125), 234\u2013259 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T18:42:20Z","timestamp":1557772940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}