{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:17:06Z","timestamp":1725520626772},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"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-89439-1_32","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"451-466","source":"Crossref","is-referenced-by-count":4,"title":["Cut Elimination for First Order G\u00f6del Logic by Hyperclause Resolution"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agata","family":"Ciabattoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian G.","family":"Ferm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/BF01531058","volume":"4","author":"A. Avron","year":"1991","unstructured":"Avron, A.: Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence\u00a04, 225\u2013248 (1991)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Avron, A.: The Method of Hypersequents in Proof Theory of Propositional Non-Classical Logics. In: Logic: From Foundations to Applications, pp. 1\u201332. Clarendon Press (1996)","key":"32_CR2","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45616-3_3","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Baaz","year":"2002","unstructured":"Baaz, M., Ciabattoni, A.: A Sch\u00fctte-Tait style cut-elimination proof for first-order G\u00f6del logic. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS, vol.\u00a02381, pp. 24\u201338. Springer, Heidelberg (2002)"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-45653-8_14","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Baaz","year":"2001","unstructured":"Baaz, M., Ciabattoni, A., Ferm\u00fcller, C.G.: Herbrand\u2019s Theorem for Prenex G\u00f6del Logic and its Consequences for Theorem Proving. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS, vol.\u00a02250, pp. 201\u2013216. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","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 (to appear)","key":"32_CR5","DOI":"10.1016\/j.tcs.2008.02.043"},{"key":"32_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.apal.2006.02.001","volume":"142","author":"M. Baaz","year":"2006","unstructured":"Baaz, M., Iemhoff, R.: The Skolemization of existential quantifiers in intuitionistic logic. Ann. of Pure and Applied Logics\u00a0142, 269\u2013295 (2006)","journal-title":"Ann. of Pure and Applied Logics"},{"issue":"2","key":"32_CR7","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. J. Symb. Comput.\u00a029(2), 149\u2013177 (2000)","journal-title":"J. Symb. Comput."},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-32275-7_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Baaz","year":"2005","unstructured":"Baaz, M., Leitsch, A.: CERES in Many-Valued Logics. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 1\u201320. Springer, Heidelberg (2005)"},{"issue":"3-4","key":"32_CR9","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. J. Symb. Comput.\u00a041(3-4), 381\u2013410 (2006)","journal-title":"J. Symb. Comput."},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61377-3_28","volume-title":"Computer Science Logic","author":"M. Baaz","year":"1996","unstructured":"Baaz, M., Leitsch, A., Zach, R.: Incompleteness of an infinite-valued first-order G\u00f6del Logic and of some temporal logic of programs. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol.\u00a01092, pp. 1\u201315. Springer, Heidelberg (1996)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-44622-2_12","volume-title":"Computer Science Logic","author":"M. Baaz","year":"2000","unstructured":"Baaz, M., Zach, R.: Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 187\u2013201. Springer, Heidelberg (2000)"},{"key":"32_CR12","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"A. Chagrov","year":"1997","unstructured":"Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997)"},{"key":"32_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-5300-3","volume-title":"Metamathematics of Fuzzy Logic","author":"P. H\u00e1jek","year":"1998","unstructured":"H\u00e1jek, P.: Metamathematics of Fuzzy Logic. Kluwer, Dordrecht (1998)"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"27","DOI":"10.2307\/2964334","volume":"25","author":"R. Harrop","year":"1960","unstructured":"Harrop, R.: Concerning formulas of the types A\u2009\u2283\u2009B\u2009\u2228\u2009C,A\u2009\u2283\u2009(\u2009\u2203\u2009x)B(x) in intuitionistic formal systems. J. Symbolic Logic\u00a025, 27\u201332 (1960)","journal-title":"J. Symbolic Logic"},{"key":"32_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A. Leitsch","year":"1997","unstructured":"Leitsch, A.: The Resolution Calculus. Springer, Heidelberg (1997)"},{"key":"32_CR16","first-page":"73","volume":"121","author":"G. Mints","year":"1974","unstructured":"Mints, G.: The Skolem method in intuitionistic calculi. Proc. Inst. Steklov.\u00a0121, 73\u2013109 (1974)","journal-title":"Proc. Inst. Steklov."},{"doi-asserted-by":"crossref","unstructured":"Orevkov, V.P.: Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. J. Soviet Mathematics, 2337\u20132350 (1982)","key":"32_CR17","DOI":"10.1007\/BF01629444"},{"key":"32_CR18","volume-title":"Beweistheorie","author":"K. Sch\u00fctte","year":"1960","unstructured":"Sch\u00fctte, K.: Beweistheorie. Springer, Heidelberg (1960)"},{"key":"32_CR19","first-page":"104","volume":"75","author":"R. Statman","year":"1979","unstructured":"Statman, R.: Lower bounds on Herbrand\u2019s theorem. Proc. of the Amer. Math. Soc.\u00a075, 104\u2013107 (1979)","journal-title":"Proc. of the Amer. Math. Soc."},{"key":"32_CR20","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/BFb0079691","volume":"LNM 72","author":"W.W. Tait","year":"1968","unstructured":"Tait, W.W.: Normal derivability in classical logic. The Syntax and Semantics of infinitary Languages\u00a0LNM 72, 204\u2013236 (1968)","journal-title":"The Syntax and Semantics of infinitary Languages"},{"doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn., Cambridge (2000)","key":"32_CR21","DOI":"10.1017\/CBO9781139168717"},{"key":"32_CR22","doi-asserted-by":"publisher","first-page":"851","DOI":"10.2307\/2274139","volume":"49","author":"G. Takeuti","year":"1984","unstructured":"Takeuti, G., Titani, T.: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. Symbolic Logic\u00a049, 851\u2013866 (1984)","journal-title":"J. Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T13:54:43Z","timestamp":1709387683000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}