{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:55Z","timestamp":1725488935369},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_40","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"517-531","source":"Crossref","is-referenced-by-count":0,"title":["Proof Analysis by Resolution"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"40_CR1","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","volume":"97","author":"M. Baaz","year":"1999","unstructured":"M. Baaz and A. Leitsch. Cut normal forms and proof complexity. Annals of Pure and Applied Logic, 97:127\u2013177, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"key":"40_CR2","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/jsco.1999.0359","volume":"29","author":"M. Baaz","year":"2000","unstructured":"M. Baaz and A. Leitsch. Cut-elimination and redundancy-elimination by resolution. J. Symbolic Computation, 29:149\u2013176, 2000.","journal-title":"J. Symbolic Computation"},{"key":"40_CR3","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Leitsch, and G. Moser. System description: Cutres 01, cut elimination by resolution. In Conference on automated deduction, CADE-16, Lecture Notes in Artificial Intelligence, pages 212\u2013216. Springer, 1999.","DOI":"10.1007\/3-540-48660-7_16"},{"key":"40_CR4","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische schlie\u00dfen. Mathematische Zeitschrift, 39:405\u2013431, 1934.","journal-title":"Mathematische Zeitschrift"},{"key":"40_CR5","unstructured":"Jean-Yves Girard and Paul Taylor. Proofs and Types. Cambridge University Press, 1989."},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"R. H\u00e4hnle. Tableaux and related methods. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, pages 101\u2013178. Elsevier, 2001.","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"40_CR7","doi-asserted-by":"publisher","first-page":"234","DOI":"10.2307\/2275028","volume":"54","author":"H. Luckhard","year":"1989","unstructured":"H. Luckhard. Herbrand-Analysen zweier Beweise des Satzes von Roth: polynomiale Anzahlschranken. The Journal of Symbolic Logic, 54:234\u2013263, 1989.","journal-title":"The Journal of Symbolic Logic"},{"key":"40_CR8","unstructured":"G. Takeuti. Proof Theory. North-Holland, second edition, 1987."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:55:52Z","timestamp":1556740552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}