{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T16:38:53Z","timestamp":1781282333220,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439295","type":"print"},{"value":"9783540456162","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_3","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T00:26:55Z","timestamp":1179361615000},"page":"24-37","source":"Crossref","is-referenced-by-count":10,"title":["A Sch\u00fctte-Tait Style Cut-Elimination Proof for First-Order G\u00f6del Logic"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Agata","family":"Ciabattoni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"939","DOI":"10.2307\/2273828","volume":"52","author":"A. Avron","year":"1987","unstructured":"A. Avron: A constructive analysis of RM. J. Symbolic Logic, 52: 939\u2013951, 1987.","journal-title":"J. Symbolic Logic"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/BF01531058","volume":"4","author":"A. Avron","year":"1991","unstructured":"A. Avron: Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artificial Intelligence, 4: 225\u2013248, 1991.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"3_CR3","first-page":"1","volume-title":"Logic: from Foundations to Applications, European Logic Colloquium","author":"A. Avron","year":"1996","unstructured":"A. Avron: The Method of Hypersequents in the Proof Theory of Propositional Nonclassical Logics. In W. Hodges, M. Hyland, C. Steinhorn and J. Truss editors, Logic: from Foundations to Applications, European Logic Colloquium Oxford Science Publications. Clarendon Press. Oxford. 1\u201332. 1996."},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Ciabattoni, C. Ferm\u00fcller: Cut-Elimination in a Sequents-of-Relations Calculus for G\u00f6del Logic. In International Symposium on Multiple Valued Logic (ISMVL\u20192001), 181\u2013186. IEEE. 2001.","DOI":"10.1109\/ISMVL.2001.924570"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Ciabattoni, C. Ferm\u00fcller: Herbrand\u2019s Theorem for Prenex G\u00f6del Logic and its Consequences for Theorem Proving. In Proceedings of Logic for Programming and Automated Reasoning (LPAR\u20192001), LNAI 2250, 201\u2013216. 2001.","DOI":"10.1007\/3-540-45653-8_14"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Ciabattoni, C. Ferm\u00fcller: Sequent of Relations Calculi: a Framework for Analytic Deduction in Many-Valued Logics. In M. Fitting and E. Orlowska editors, Theory and applications of Multiple-Valued Logics. To appear.","DOI":"10.1007\/978-3-7908-1769-0_6"},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45504-3_4","volume-title":"Proceedings of Proof Theory in Computer Science","author":"M. Baaz","year":"2001","unstructured":"M. Baaz, A. Leitsch: Comparing the complexity of cut-elimination methods. In Proceedings of Proof Theory in Computer Science, LNCS 2183, 49\u201367. 2001."},{"key":"3_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-44622-2_12","volume-title":"Proceedings of Computer Science Logic (CSL\u20192000)","author":"M. Baaz","year":"2000","unstructured":"M. Baaz, R. Zach: Hypersequents and the proof theory of intuitionistic fuzzy logic. In Proceedings of Computer Science Logic (CSL\u20192000), LNCS 1862, 187\u2013201. 2000."},{"key":"3_CR9","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1017\/S0022481200125848","volume":"24","author":"M. Dummett","year":"1959","unstructured":"M. Dummett: A Propositional Logic with Denumerable Matrix. J. of Symbolic Logic, 24: 96\u2013107. 1959.","journal-title":"J. of Symbolic Logic"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen: Untersuchungen \u00fcber das logische Schliessen I, II. Mathematische Zeitschrift, 39: 176\u2013210, 405\u2013431. 1934.","journal-title":"Mathematische Zeitschrift"},{"key":"3_CR11","first-page":"34","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"K. G\u00f6del: Zum Intuitionistischen Aussagenkalkul. Ergebnisse eines mathematischen Kolloquiums, 4: 34\u201338. 1933.","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"P. H\u00e1jek: Metamathematics of Fuzzy Logic. Kluwer. 1998.","DOI":"10.1007\/978-94-011-5300-3"},{"key":"3_CR13","unstructured":"K. Sch\u00fctte: Beweistheorie. Springer Verlag. 1960."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"W.W. Tait: Normal derivability in classical logic. In The Sintax and Semantics of infinitary Languages, LNM 72, 204\u2013236. 1968.","DOI":"10.1007\/BFb0079691"},{"key":"3_CR15","unstructured":"G. Takeuti: Proof Theory. North-Holland. 1987."},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"851","DOI":"10.2307\/2274139","volume":"49","author":"G. Takeuti","year":"1984","unstructured":"G. Takeuti, T. Titani: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. of Symbolic Logic, 49: 851\u2013866. 1984.","journal-title":"J. of Symbolic Logic"},{"key":"3_CR17","unstructured":"A.S. Troelstra and H. Schwichtenberg: Basic Proof Theory. Cambridge University Press. 1996"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45616-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T14:08:24Z","timestamp":1550326104000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}