{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T21:07:52Z","timestamp":1649192872164},"reference-count":6,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,5,10]],"date-time":"2015-05-10T00:00:00Z","timestamp":1431216000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s11225-015-9618-z","type":"journal-article","created":{"date-parts":[[2015,5,9]],"date-time":"2015-05-09T11:52:18Z","timestamp":1431172338000},"page":"663-667","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Book Review: Matthias Baaz and Alexander Leitsch, Methods of Cut-Elimination"],"prefix":"10.1007","volume":"103","author":[{"given":"Sam","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,10]]},"reference":[{"key":"9618_CR1","doi-asserted-by":"crossref","unstructured":"Baaz, M., A. Ciabattoni, and C. G. Ferm\u00fcller, First order G\u00f6del logics by hyperclause resolution, in Proc. Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, Springer-Verlag, 2008, pp. 451\u2013466.","DOI":"10.1007\/978-3-540-89439-1_32"},{"key":"9618_CR2","doi-asserted-by":"crossref","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 29, 149\u2013176 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"9618_CR3","doi-asserted-by":"crossref","unstructured":"Baaz, M., and A. Leitsch, CERES in many-valued logics, in Proc. Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2004), Lecture Notes in Artificial Intelligence 3452, Springer-Verlag, 2005, pp. 1\u201320.","DOI":"10.1007\/978-3-540-32275-7_1"},{"key":"9618_CR4","doi-asserted-by":"crossref","unstructured":"Dunchev, C., A. Leitsch, T. Libal, M. Reiner, M. Rukhaia, D. Weller, and B. Woltzenlogel-Paleo, ProofTool: A GUI for the GAPT framework, in Proc. 10th Workshop on User Interfaces for Theorem Provers (UITP 2012), Electronic Proceedings in Theoretical Computer Science 118, 2012, pp. 1\u201314.","DOI":"10.4204\/EPTCS.118.1"},{"key":"9618_CR5","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M.S. Paterson","year":"1978","unstructured":"Paterson M.S., Wegman M.N.: Linear unification. J. Comput. System Sci. 16, 158\u2013167 (1978)","journal-title":"J. Comput. System Sci."},{"key":"9618_CR6","first-page":"104","volume":"75","author":"R. Statman","year":"1979","unstructured":"Statman R.: Lower bounds on Herbrand\u2019s theorem. Proceedings of the American Mathematical Society 75, 104\u2013107 (1979)","journal-title":"Proceedings of the American Mathematical Society"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9618-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-015-9618-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9618-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,24]],"date-time":"2019-08-24T21:41:45Z","timestamp":1566682905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-015-9618-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,10]]},"references-count":6,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["9618"],"URL":"https:\/\/doi.org\/10.1007\/s11225-015-9618-z","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,10]]}}}