{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:23:53Z","timestamp":1725902633957},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662553855"},{"type":"electronic","value":"9783662553862"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-662-55386-2_5","type":"book-chapter","created":{"date-parts":[[2017,6,28]],"date-time":"2017-06-28T11:24:53Z","timestamp":1498649093000},"page":"68-79","source":"Crossref","is-referenced-by-count":1,"title":["On the Length of Medial-Switch-Mix Derivations"],"prefix":"10.1007","author":[{"given":"Paola","family":"Bruscoli","sequence":"first","affiliation":[]},{"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,29]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-62950-5_74","volume-title":"Rewriting Techniques and Applications","author":"D Bechet","year":"1997","unstructured":"Bechet, D., Groote, P., Retor\u00e9, C.: A complete axiomatisation for the inclusion of series-parallel partial orders. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 230\u2013240. Springer, Heidelberg (1997). doi: 10.1007\/3-540-62950-5_74"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0022-4049(95)00159-X","volume":"113","author":"R Blute","year":"1996","unstructured":"Blute, R., Cockett, R., Seely, R., Trimble, T.: Natural deduction and coherence for weakly distributive categories. J. Pure Appl. Algebra 113, 229\u2013296 (1996)","journal-title":"J. Pure Appl. Algebra"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 2250, pp. 347\u2013361. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45653-8_24"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45619-8_21","volume-title":"Logic Programming","author":"P Bruscoli","year":"2002","unstructured":"Bruscoli, P.: A purely logical account of sequentiality in proof search. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 302\u2013316. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45619-8_21"},{"issue":"2","key":"5_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1462179.1462186","volume":"10","author":"P Bruscoli","year":"2009","unstructured":"Bruscoli, P., Guglielmi, A.: On the proof complexity of deep inference. ACM Trans. Comput. Logic 10(2), 1\u201334 (2009). Article 14","journal-title":"ACM Trans. Comput. Logic"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-17511-4_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Bruscoli","year":"2010","unstructured":"Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 136\u2013153. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_9"},{"issue":"1:5","key":"5_CR7","first-page":"1","volume":"12","author":"P Bruscoli","year":"2016","unstructured":"Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: A quasipolynomial normalisation in deep inference via atomic flows and threshold formulae. Log. Methods Comput. Sci. 12(1:5), 1\u201330 (2016)","journal-title":"Log. Methods Comput. Sci."},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-30870-3_15","volume-title":"How the World Computes","author":"A Das","year":"2012","unstructured":"Das, A.: Complexity of deep inference via atomic flows. In: Cooper, S.B., Dawar, A., L\u00f6we, B. (eds.) CiE 2012. LNCS, vol. 7318, pp. 139\u2013150. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30870-3_15"},{"key":"5_CR9","unstructured":"Das, A.: Rewriting with linear inferences in propositional logic. In: van Raamsdonk, F. (ed) 24th International Conference on Rewriting Techniques and Applications (RTA). Leibniz International Proceedings in Informatics (LIPIcs), vol. 21, pp. 158\u2013173. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"5_CR10","unstructured":"Das, A., Stra\u00dfburger, L.: No complete linear term rewriting system for propositional logic. In: Fernandez, M. (ed) 26th International Conference on Rewriting Techniques and Applications, RTA 2015. LIPIcs, Warsaw, Poland, 29 June to 1 July 2015, vol. 36, pp. 127\u2013142 (2015)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Das, A., Stra\u00dfburger, L.: On linear rewriting systems for boolean logic and some applications to proof theory. Log. Methods Comput. Sci. 12(4) (2016)","DOI":"10.2168\/LMCS-12(4:9)2016"},{"issue":"1","key":"5_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1182613.1182614","volume":"8","author":"A Guglielmi","year":"2007","unstructured":"Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Logic 8(1), 1\u201364 (2007)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"1:9","key":"5_CR13","first-page":"1","volume":"4","author":"A Guglielmi","year":"2008","unstructured":"Guglielmi, A., Gundersen, T.: Normalisation control in deep inference via atomic flows. Log. Methods Comput. Sci. 4(1:9), 1\u201336 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Guglielmi, A., Gundersen, T., Stra\u00dfburger, L.: Breaking paths in atomic flows for classical logic. In: LICS 2010 (2010)","DOI":"10.1109\/LICS.2010.12"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-44802-0_5","volume-title":"Computer Science Logic","author":"A Guglielmi","year":"2001","unstructured":"Guglielmi, A., Stra\u00dfburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 54\u201368. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44802-0_5"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Gundersen, T., Heijltjes, W., Parigot, M.: Atomic lambda calculus: a typed lambda-calculus with explicit sharing. In: 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, 25\u201328 June 2013, pp. 311\u2013320. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.37"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Kahramanogullari, O.: Interaction and depth against nondeterminism in proof search. Log. Methods Comput. Sci. 10(2) (2014)","DOI":"10.2168\/LMCS-10(2:5)2014"},{"issue":"18","key":"5_CR18","first-page":"473","volume":"18","author":"F Lamarche","year":"2007","unstructured":"Lamarche, F.: Exploring the gap between linear and classical logic. Theory Appl. Categ. 18(18), 473\u2013535 (2007)","journal-title":"Theory Appl. Categ."},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-36078-6_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L Stra\u00dfburger","year":"2002","unstructured":"Stra\u00dfburger, L.: A local system for linear logic. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 388\u2013402. Springer, Heidelberg (2002). doi: 10.1007\/3-540-36078-6_26"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-540-73449-9_26","volume-title":"Term Rewriting and Applications","author":"L Stra\u00dfburger","year":"2007","unstructured":"Stra\u00dfburger, L.: A characterization of medial as rewriting rule. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 344\u2013358. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73449-9_26"},{"issue":"18","key":"5_CR21","first-page":"536","volume":"18","author":"L Stra\u00dfburger","year":"2007","unstructured":"Stra\u00dfburger, L.: On the axiomatisation of Boolean categories with and without medial. Theory Appl. Categ. 18(18), 536\u2013601 (2007)","journal-title":"Theory Appl. Categ."},{"key":"5_CR22","unstructured":"Aler Tubella, A.: A study of normalisation through subatomic logic. PhD thesis, University of Bath (2016)"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-55386-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T09:16:28Z","timestamp":1569575788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-55386-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662553855","9783662553862"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-55386-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}