{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:47:30Z","timestamp":1725472050451},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540482819"},{"type":"electronic","value":"9783540482826"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11916277_17","type":"book-chapter","created":{"date-parts":[[2006,10,17]],"date-time":"2006-10-17T18:32:59Z","timestamp":1161109979000},"page":"242-256","source":"Crossref","is-referenced-by-count":13,"title":["A Local System for Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Alwen","family":"Tiu","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_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. Ann. Math. Artif. Intell.\u00a04, 225\u2013248 (1991)","journal-title":"Ann. Math. Artif. Intell."},{"key":"17_CR2","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\u201337. Springer, Heidelberg (2002)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Balat, V., Galmiche, D.: Labelled proof systems for intuitionistic provability, pp. 1\u201332 (2000)","DOI":"10.1007\/978-94-011-4040-9_1"},{"key":"17_CR4","unstructured":"Br\u00fcnnler, K.: Deep Inference and Symmetry in Classical Proofs. PhD thesis, TU Dresden (September 2003)"},{"issue":"5","key":"17_CR5","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1093\/jigpal\/11.5.525","volume":"11","author":"K. Br\u00fcnnler","year":"2003","unstructured":"Br\u00fcnnler, K.: Two restrictions on contraction. Logic Journal of the IGPL\u00a011(5), 525\u2013529 (2003)","journal-title":"Logic Journal of the IGPL"},{"key":"17_CR6","unstructured":"Br\u00fcnnler, K.: Intuitionistic logic in the calculus of structures (unpublished notes) (2004)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45653-8_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Br\u00fcnnler","year":"2001","unstructured":"Br\u00fcnnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS, vol.\u00a02250, pp. 347\u2013361. Springer, Heidelberg (2001)"},{"issue":"2","key":"17_CR8","doi-asserted-by":"publisher","first-page":"97","DOI":"10.2307\/2964753","volume":"24","author":"M. Dummett","year":"1959","unstructured":"Dummett, M.: A propositional calculus with denumerable matrix. J. Symbolic Logic\u00a024(2), 97\u2013106 (1959)","journal-title":"J. Symbolic Logic"},{"key":"17_CR9","volume-title":"Element of Intuitionism","author":"M. Dummett","year":"1977","unstructured":"Dummett, M.: Element of Intuitionism. Oxford University Press, Oxford (1977)"},{"issue":"3","key":"17_CR10","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic\u00a057(3), 795\u2013807 (1992)","journal-title":"Journal of Symbolic Logic"},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"17_CR12","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1093\/jigpal\/6.3.451","volume":"6","author":"R. Gor\u00e9","year":"1998","unstructured":"Gor\u00e9, R.: Substructural logics on display. Logic Journal of the IGPL\u00a06(3), 451\u2013504 (1998)","journal-title":"Logic Journal of the IGPL"},{"key":"17_CR13","unstructured":"Guglielmi, A.: A system of interaction and structure. Technical Report WV-02-10, TU Dresden. ACM Transactions on Computational Logic (accepted, 2002)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Guiraud, Y.: The three dimensions of proofs. Annals of Pure and Applied Logic (to appear, 2006)","DOI":"10.1016\/j.apal.2005.12.012"},{"key":"17_CR15","unstructured":"Horsfall, B.: Towards BI in the calculus of structures. In: ESSLLI 2006 (accepted, 2006)"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF01627506","volume":"31","author":"J. Hudelmaier","year":"1992","unstructured":"Hudelmaier, J.: Bounds on cut-elimination in intuitionistic propositional logic. Archive for Mathematical Logic\u00a031, 331\u2013354 (1992)","journal-title":"Archive for Mathematical Logic"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11916277_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kahramano\u011fullar\u0131","year":"2006","unstructured":"Kahramano\u011fullar\u0131, O.: Reducing Nondeterminism in the Calculus of Structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol.\u00a04246, pp. 272\u2013286. Springer, Heidelberg (2006) (accepted at)"},{"key":"17_CR18","unstructured":"McKinley, R.: Classical Categories and Deep Inference. PhD thesis, University of Bath (2006)"},{"issue":"2","key":"17_CR19","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P., Pym, D.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05(2), 215\u2013243 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"key":"17_CR20","unstructured":"Stewart, C., Stouppa, P.: A systematic proof theory for several modal logics. In: Schmidt, R., Pratt-Hartmann, I., Reynolds, M., Wansing, H. (eds.) Advances in Modal Logic, vol.\u00a05, pp. 309\u2013333. King\u2019s College Publications (2005)"},{"key":"17_CR21","unstructured":"Stra\u00dfburger, L.: Linear Logic and Noncommutativity in the Calculus of Structures. PhD thesis, Technische Universit\u00e4t Dresden (2003)"},{"issue":"3","key":"17_CR22","doi-asserted-by":"publisher","first-page":"851","DOI":"10.2307\/2274139","volume":"49","author":"G. Takeuti","year":"1984","unstructured":"Takeuti, G., Titani, S.: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. Symbolic Logic\u00a049(3), 851\u2013866 (1984)","journal-title":"J. Symbolic Logic"},{"key":"17_CR23","unstructured":"Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press (1996)"}],"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\/11916277_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:58:15Z","timestamp":1605643095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11916277_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540482819","9783540482826"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11916277_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}