. Finally, -node in the linking P and an a.-node at each door of the box in ? (except the ?-door)

M. Abadi, L. Cardelli, P. Curien, and J. Lévy, Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991.
DOI : 10.1016/0304-3975(86)90035-6

B. Peter and . Andrews, Refutations by matings, IEEE Transactions on Computers, issue.25, pp.801-807, 1976.

R. Blute, R. Cockett, R. Seely, and T. Trimble, Natural deduction and coherence for weakly distributive categories, Journal of Pure and Applied Algebra, vol.113, issue.3, pp.229-296, 1996.
DOI : 10.1016/0022-4049(95)00159-X
URL : http://doi.org/10.1016/0022-4049(95)00159-x

K. Brünnler, Deep Inference and Symmetry for Classical Proofs, 2003.

K. Brünnler and A. Tiu, A Local System for Classical Logic, LNAI, vol.2250, pp.347-361, 2001.
DOI : 10.1007/3-540-45653-8_24

R. Samuel and . Buss, The undecidability of k-provability. Annals of Pure and Applied Logic, pp.72-102, 1991.

G. Bellin and J. Van-de-wiele, Subnets of proof-nets in MLL ?, Advances in Linear Logic, pp.249-270, 1995.

K. Chaudhuri and N. Guenot, Equality and fixpoints in the calculus of structures, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, 2014.
DOI : 10.1145/2603088.2603140
URL : https://hal.archives-ouvertes.fr/hal-01091570

K. Chaudhuri, N. Guenot, and L. Straßburger, The focused calculus of structures, Schloss Dagstuhl ? Leibniz-Zentrum fuer Informatik, pp.159-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772420

. Govert-de-bruijn, Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, Indag. Math, vol.34, pp.381-392, 1972.

D. [. Devarajan, G. Hughes, V. R. Plotkin, and . Pratt, Full completeness of the multiplicative linear logic of Chu spaces, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782619

V. Danos and L. Regnier, The structure of multiplicatives, Archive for Mathematical Logic, vol.28, issue.3, pp.181-203, 1989.
DOI : 10.1007/BF01622878

A. Guglielmi and T. Gundersen, Normalisation Control in Deep Inference via Atomic Flows, Logical Methods in Computer Science, vol.4, issue.1, pp.1-36, 2008.
DOI : 10.2168/LMCS-4(1:9)2008
URL : http://arxiv.org/pdf/0709.1205

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, Quantifiers in linear logic II, p.19, 1990.

A. Guglielmi and L. Straßburger, Non-commutativity and MELL in the Calculus of Structures, Computer Science Logic LNCS, vol.2142, pp.54-68, 2001.
DOI : 10.1007/3-540-44802-0_5

A. Guglielmi and L. Straßburger, A system of interaction and structure V: the exponentials and splitting, Mathematical Structures in Computer Science, vol.21, issue.03, pp.563-584, 2011.
DOI : 10.1017/S096012951100003X
URL : https://hal.archives-ouvertes.fr/inria-00441254

A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, pp.1-64, 2007.
DOI : 10.1145/1182613.1182614
URL : https://hal.archives-ouvertes.fr/inria-00441214

W. Heijltjes and R. Houston, No proof nets for MLL with units, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.501-5010, 2014.
DOI : 10.1145/2603088.2603126

W. Heijltjes and D. J. Hughes, Complexity Bounds for Sum-Product Logic via Additive Proof Nets and Petri Nets, 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.80-91, 2015.
DOI : 10.1109/LICS.2015.18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.717.8920

D. Hughes, Simple free star-autonomous categories and full coherence, Journal of Pure and Applied Algebra, vol.216, issue.11, 2005.
DOI : 10.1016/j.jpaa.2012.03.020
URL : http://arxiv.org/abs/math/0506521

D. Hughes, Simple multiplicative proof nets with units, 2005.

D. Hughes and R. Van-glabbeek, Proof nets for unit-free multiplicative-additive linear logic, 18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp.1-10, 2003.
DOI : 10.1145/1094622.1094629
URL : http://boole.stanford.edu/pub/mall-monochrome.pdf

[. Lafont, Logique, Catégories et Machines, 1988.

Y. Lafont, From proof nets to interaction nets, Advances in Linear Logic, pp.225-247, 1995.
DOI : 10.1017/CBO9780511629150.012
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.2755

A. Lyaletski and B. Konev, On Herbrand???s Theorem for Intuitionistic Logic, Logics in Artificial Intelligence: 10th European Conference, pp.293-305, 2006.
DOI : 10.1007/11853886_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.7022

[. Lamarche and L. Straßburger, From Proof Nets to the Free *-Autonomous Category, Logical Methods in Computer Science, vol.2, issue.4, pp.1-44, 2006.
DOI : 10.2168/LMCS-2(4:3)2006
URL : http://arxiv.org/pdf/cs.LO/0605054

R. Mckinley, On Herbrand's theorem and cut elimination (extended abstract). preprint, 2008. [Mil87] Dale Miller. A compact representation of proofs, Studia Logica, vol.46, issue.4, pp.347-370, 1987.

[. Retoré, Réseaux et Séquents Ordonnés, 1993.

L. Straßburger and A. Guglielmi, A system of interaction and structure IV: The exponentials and decomposition, ACM Trans. Comput. Log, vol.12, issue.4, p.23, 2011.

L. Straßburger and F. Lamarche, On Proof Nets for Multiplicative Linear Logic with Units, Computer Science Logic, pp.145-159, 2004.
DOI : 10.1007/978-3-540-30124-0_14

L. Straßburger, Linear Logic and Noncommutativity in the Calculus of Structures, 2003.

L. Straßburger, Some Observations on the Proof Theory of Second Order Propositional Multiplicative??Linear??Logic, Typed Lambda Calculi and Applications, TLCA'09, pp.309-324, 2009.
DOI : 10.1007/BF01622878

L. Straßburger, From Deep Inference to Proof Nets via Cut Elimination, Journal of Logic and Computation, vol.21, issue.4, pp.589-624, 2011.
DOI : 10.1093/logcom/exp047

A. Tubella, A study of normalisation through subatomic logic, 2016.