{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:20:35Z","timestamp":1758979235978,"version":"3.41.2"},"reference-count":15,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2006,4,3]],"date-time":"2006-04-03T00:00:00Z","timestamp":1144022400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper studies properties of the logic BV, which is an extension of\nmultiplicative linear logic (MLL) with a self-dual non-commutative operator. BV\nis presented in the calculus of structures, a proof theoretic formalism that\nsupports deep inference, in which inference rules can be applied anywhere\ninside logical expressions. The use of deep inference results in a simple\nlogical system for MLL extended with the self-dual non-commutative operator,\nwhich has been to date not known to be expressible in sequent calculus. In this\npaper, deep inference is shown to be crucial for the logic BV, that is, any\nrestriction on the ``depth'' of the inference rules of BV would result in a\nstrictly less expressive logical system.<\/jats:p>","DOI":"10.2168\/lmcs-2(2:4)2006","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:27:20Z","timestamp":1164274040000},"source":"Crossref","is-referenced-by-count":15,"title":["A System of Interaction and Structure II: The Need for Deep Inference"],"prefix":"10.46298","volume":"Volume 2, Issue 2","author":[{"given":"Alwen","family":"Tiu","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2006,4,3]]},"reference":[{"key":"10.2168\/LMCS-2(2:4)2006_BelnapJPL82","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"N. D. Belnap","year":"1982","journal-title":"Journal of Philosophical Logic"},{"key":"10.2168\/LMCS-2(2:4)2006_Bru03phd","unstructured":"Kai Br\u00fcnnler.Deep Inference and Symmetry in Classical Proofs. PhD thesis, TU Dresden, September 2003."},{"key":"10.2168\/LMCS-2(2:4)2006_BruTiu2001","doi-asserted-by":"crossref","unstructured":"Kai Br\u00fcnnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors,LPAR 2001, volume 2250 ofLecture Notes in Artificial Intelligence, pages 347-361. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45653-8_24"},{"key":"10.2168\/LMCS-2(2:4)2006_GenILD35","doi-asserted-by":"crossref","unstructured":"Gerhard Gentzen. Investigations into logical deduction. In M. E. Szabo, editor,The Collected Papers of Gerhard Gentzen, pages 68-131. North-Holland, Amsterdam, 1969.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"10.2168\/LMCS-2(2:4)2006_GirTCS87","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"Jean-Yves Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-2(2:4)2006_GugStr01","doi-asserted-by":"crossref","unstructured":"Alessio Guglielmi and Lutz Stra\\ssburger. Non-commutativity and MELL in the calculus of structures. In L. Fribourg, editor,CSL 2001, volume 2142 ofLecture Notes in Computer Science, pages 54-68. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44802-0_5"},{"key":"10.2168\/LMCS-2(2:4)2006_GugV99","unstructured":"Alessio Guglielmi. A calculus of order and interaction. Technical Report WV-99-04, Dresden University of Technology, 1999."},{"key":"10.2168\/LMCS-2(2:4)2006_GugV02","unstructured":"Alessio Guglielmi. A system of interaction and structure. Technical Report WV-02-10, Technische Universit\u00e4t Dresden, 2002. To appear in ACM Transactions on Computational Logic."},{"key":"10.2168\/LMCS-2(2:4)2006_Moeh89","doi-asserted-by":"crossref","unstructured":"Rolf H. M\u00f6hring. Computationally tractable classes of ordered sets. In I. Rival, editor,Algorithms and Order, pages 105-194. Kluwer Academic Publishers, Dordrecht, 1989.","DOI":"10.1007\/978-94-009-2639-4_4"},{"issue":"2","key":"10.2168\/LMCS-2(2:4)2006_Ohearn99bsl","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. O'Hearn and D. Pym","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.2168\/LMCS-2(2:4)2006_RetTLCA97","doi-asserted-by":"crossref","unstructured":"Christian Retor\u00e9. Pomset logic: A non-com\\-mu\\-ta\\-tive extension of classical linear logic. In Ph. de Groote and J. R. Hindley, editors,TLCA'97, volume 1210 ofLecture Notes in Computer Science, pages 300-318, 1997.","DOI":"10.1007\/3-540-62688-3_43"},{"key":"10.2168\/LMCS-2(2:4)2006_RetINRIA99","unstructured":"Christian Retor\u00e9. Pomset logic as a calculus of directed cographs. In V. M. Abrusci and C. Casadio, editors,Dynamic Perspectives in Logic and Linguistics, pages 221-247. Bulzoni, Roma, 1999. Also available as INRIA Rapport de Recherche RR-3714."},{"key":"10.2168\/LMCS-2(2:4)2006_StraThesis","unstructured":"Lutz Stra\\ssburger.Linear Logic and Noncommutativity in the Calculus of Structures. PhD thesis, Technische Universit\u00e4t Dresden, 2003."},{"key":"10.2168\/LMCS-2(2:4)2006_Tiu01","unstructured":"Alwen Tiu. Properties of a logical system in the calculus of structures. Technical Report WV-01-06, Dresden University of Technology, 2001."},{"key":"10.2168\/LMCS-2(2:4)2006_TrolBasic96","unstructured":"A.S. Troelstra and H. Schwichtenberg.Basic Proof Theory. Cambridge University Press, 1996."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2252\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2252\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:10:40Z","timestamp":1681243840000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2252"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4,3]]},"references-count":15,"URL":"https:\/\/doi.org\/10.2168\/lmcs-2(2:4)2006","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0512036","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0512036","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2006,4,3]]},"article-number":"2252"}}