A. Atserias, N. Galesi, and P. Pudlák, Monotone simulations of non-monotone proofs, Journal of Computer and System Sciences, vol.65, issue.4, pp.626-638, 2002.
DOI : 10.1016/S0022-0000(02)00020-X

P. Bruscoli and A. Guglielmi, On analytic inference rules in the calculus of structures, 2007.

P. Bruscoli and A. Guglielmi, On the proof complexity of deep inference, ACM Transactions on Computational Logic, vol.10, issue.2, pp.1-34, 2009.
DOI : 10.1145/1462179.1462186
URL : https://hal.archives-ouvertes.fr/inria-00441211

P. Bruscoli, A Purely Logical Account of Sequentiality in Proof Search, Logic Programming, 18th International Conference, pp.302-316, 2002.
DOI : 10.1007/3-540-45619-8_21

K. Brünnler, Atomic Cut Elimination for Classical Logic, Lecture Notes in Computer Science, vol.2803, pp.86-97, 2003.
DOI : 10.1007/978-3-540-45220-1_9

K. Brünnler, Deep Inference and Symmetry in Classical Proofs, Logos Verlag, 2004.

K. Brünnler, Cut Elimination inside a Deep Inference System for Classical Predicate Logic, Studia Logica, vol.11, issue.1, pp.51-71, 2006.
DOI : 10.1007/s11225-006-6605-4

K. Brünnler, Deep Inference and Its Normal Form of Derivations, Computability in Europe, pp.65-74, 2006.
DOI : 10.1007/978-3-642-66473-1

K. Brünnler, Deep sequent systems for modal logic Advances in Modal Logic, pp.107-119, 2006.

K. Brünnler, Locality for Classical Logic, Notre Dame Journal of Formal Logic, vol.47, issue.4, pp.557-580, 2006.
DOI : 10.1305/ndjfl/1168352668

K. Brünnler and A. Tiu, A Local System for Classical Logic, Lecture Notes in Artificial Intelligence, 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.75-102, 1991.

P. Di and G. , Structures for multiplicative cyclic linear logic: Deepness vs cyclicity, Lecture Notes in Computer Science, vol.3210, pp.130-144, 2004.

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

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

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

A. Guglielmi and L. Straßburger, A Non-commutative Extension of MELL, Lecture Notes in Artificial Intelligence, vol.2514, pp.231-246, 2002.
DOI : 10.1007/3-540-36078-6_16

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, 2009.
DOI : 10.1017/S096012951100003X
URL : https://hal.archives-ouvertes.fr/inria-00441254

R. Goré and A. Tiu, Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5, Journal of Logic and Computation, vol.17, issue.4, pp.767-794, 2007.
DOI : 10.1093/logcom/exm026

A. Guglielmi, Deep inference and the calculus of structures

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

A. Guglielmi and . Th, Prolog program, 2009.

R. Hein and C. Stewart, Purity through unravelling, Structures and Deduction/SD05/ SD05-Proc.pdf, pp.126-143, 2005.

E. Je?ábek, Proof Complexity of the Cut-free Calculus of Structures, Journal of Logic and Computation, vol.19, issue.2, pp.323-339, 2009.
DOI : 10.1093/logcom/exn054

O. Kahramano?-gullar?, Reducing nondeterminism in the calculus of structures, Lecture Notes in Artificial Intelligence, vol.4246, pp.272-286, 2006.

O. Kahramano?-gullar?, System BV is NP-complete. Annals of Pure and Applied Logic, pp.107-121, 2007.

L. Straßburger and A. Guglielmi, A system of interaction and structure IV: The exponentials and decomposition. Submitted, 2009.

C. Stewart and P. Stouppa, A systematic proof theory for several modal logics, Advances in Modal Logic, pp.309-333, 2005.

R. Statman, Bounds for proof-search and speed-up in the predicate calculus, Annals of Mathematical Logic, vol.15, issue.3, pp.225-287, 1978.
DOI : 10.1016/0003-4843(78)90011-6

P. Stouppa, A Deep Inference System for the Modal Logic S5, Studia Logica, vol.6, issue.5, pp.199-214, 2007.
DOI : 10.1007/s11225-007-9028-y

L. Straßburger, A local system for linear logic, Lecture Notes in Artificial Intelligence, vol.2514, pp.388-402, 2002.

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

L. Straßburger, MELL in the calculus of structures, Theoretical Computer Science, vol.309, issue.1-3, pp.213-285, 2003.
DOI : 10.1016/S0304-3975(03)00240-8

A. Tiu, A Local System for Intuitionistic Logic, Lecture Notes in Artificial Intelligence, vol.4246, pp.242-256, 2006.
DOI : 10.1007/11916277_17

A. Tiu, A System of Interaction and Structure II: The Need for Deep Inference, Logical Methods in Computer Science, vol.2, issue.2, pp.1-24, 2006.
DOI : 10.2168/LMCS-2(2:4)2006

I. Wegener, The Complexity of Boolean Functions, 1987.