{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T08:38:56Z","timestamp":1725525536078},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540926863"},{"type":"electronic","value":"9783540926870"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-92687-0_15","type":"book-chapter","created":{"date-parts":[[2009,2,10]],"date-time":"2009-02-10T09:25:38Z","timestamp":1234257938000},"page":"214-229","source":"Crossref","is-referenced-by-count":2,"title":["A Clausal Approach to Proof Analysis in Second-Order Logic"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"15_CR1","doi-asserted-by":"publisher","first-page":"1239","DOI":"10.2307\/2275367","volume":"57","author":"U. Kohlenbach","year":"1992","unstructured":"Kohlenbach, U.: Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. Journal of Symbolic Logic\u00a057(4), 1239\u20131273 (1992)","journal-title":"Journal of Symbolic Logic"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/j.jsc.2003.10.005","volume":"41","author":"M. Baaz","year":"2006","unstructured":"Baaz, M., Leitsch, A.: Towards a clausal analysis of cut-elimination. Journal of Symbolic Computation\u00a041, 381\u2013410 (2006)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/jsco.1999.0359","volume":"29","author":"M. Baaz","year":"2000","unstructured":"Baaz, M., Leitsch, A.: Cut-elimination and Redundancy-elimination by Resolution. Journal of Symbolic Computation\u00a029(2), 149\u2013176 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.tcs.2008.02.043","volume":"403","author":"M. Baaz","year":"2008","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Ceres: An Analysis of F\u00fcrstenberg\u2019s Proof of the Infinity of Primes. Theoretical Computer Science\u00a0403, 160\u2013175 (2008)","journal-title":"Theoretical Computer Science"},{"key":"15_CR5","unstructured":"Hetzl, S.: Characteristic Clause Sets and Proof Transformations. PhD thesis, Vienna University of Technology (2007)"},{"key":"15_CR6","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: CERES in second-order logic. Technical report, Vienna University of Technology (2008), \n                  \n                    http:\/\/www.logic.at\/ceres\/downloads\/docs\/report_ceres2.pdf"},{"issue":"2","key":"15_CR7","first-page":"56","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. JSL\u00a05(2), 56\u201368 (1940)","journal-title":"JSL"},{"key":"15_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139164931","volume-title":"Computability and Logic","author":"G.S. Boolos","year":"2002","unstructured":"Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)","edition":"4"},{"key":"15_CR9","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Proof Theory","author":"G. Takeuti","year":"1975","unstructured":"Takeuti, G.: Proof Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a081. North-Holland Publishing Co., Amsterdam (1975)"},{"key":"15_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11812289_8","volume-title":"Mathematical Knowledge Management","author":"M. Baaz","year":"2006","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Proof transformation by CERES. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 82\u201393. Springer, Heidelberg (2006)"},{"issue":"3","key":"15_CR11","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in Type Theory. Journal of Symbolic Logic\u00a036(3), 414\u2013432 (1971)","journal-title":"Journal of Symbolic Logic"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","volume":"97","author":"M. Baaz","year":"1999","unstructured":"Baaz, M., Leitsch, A.: Cut normal forms and proof complexity. Annals of Pure and Applied Logic\u00a097, 127\u2013177 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"4","key":"15_CR13","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D.A. Miller","year":"1987","unstructured":"Miller, D.A.: A compact representation of proofs. Studia Logica\u00a046(4), 347\u2013370 (1987)","journal-title":"Studia Logica"},{"issue":"3","key":"15_CR14","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.B., Schellinx, H.: A New Deconstructive Logic: Linear Logic. Journal of Symbolic Logic\u00a062(3), 755\u2013807 (1997)","journal-title":"Journal of Symbolic Logic"},{"issue":"1-2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1020840027781","volume":"133","author":"C. Benzm\u00fcller","year":"2002","unstructured":"Benzm\u00fcller, C.: Comparing approaches to resolution based higher-order theorem proving. Synthese\u00a0133(1-2), 203\u2013335 (2002)","journal-title":"Synthese"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1016\/B978-044450813-3\/50018-7","volume-title":"Handbook of automated reasoning","author":"G. Dowek","year":"2001","unstructured":"Dowek, G.: Higher-order unification and matching. In: Handbook of automated reasoning, pp. 1009\u20131062. Elsevier Science Publishers B.V., Amsterdam (2001)"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-92687-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,5]],"date-time":"2019-03-05T07:46:16Z","timestamp":1551771976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92687-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540926863","9783540926870"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92687-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}