S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, The Journal of Symbolic Logic, vol.87, issue.01, pp.36-50, 1979.
DOI : 10.1007/BF01475439

A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2000.
DOI : 10.1017/CBO9781139168717

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1934.
DOI : 10.1007/BF01201353

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

A. Haken, The intractability of resolution, Theoretical Computer Science, vol.39, pp.297-308, 1985.
DOI : 10.1016/0304-3975(85)90144-6

M. Baaz and A. Leitsch, Towards a clausal analysis of cut-elimination, Journal of Symbolic Computation, vol.41, issue.3-4, pp.3-4, 2006.
DOI : 10.1016/j.jsc.2003.10.005

A. Ciabattoni and A. Leitsch, Towards an algorithmic construction of cut-elimination procedures, Mathematical Structures in Computer Science, vol.2381, issue.01, pp.81-105, 2008.
DOI : 10.1007/BF01201353

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-00441254

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

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

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

A. Das, On the Proof Complexity of Cut-Free Bounded Deep Inference, Automated Reasoning with Analytic Tableaux and Related Methods -20th International Conference, pp.134-148, 2011.
DOI : 10.2307/2273702

K. Brünnler, Deep inference and symmetry for classical proofs, 2003.

L. Straßburger, Linear logic and noncommutativity in the calculus of structures, 2003.

D. Hilbert, Die logischen Grundlagen der Mathematik, Mathematische Annalen, vol.88, issue.1-2, pp.151-165, 1922.
DOI : 10.1007/BF01448445

G. S. Tseitin, On the complexity of derivation in propositional calculus, Zapiski Nauchnykh Seminarou LOMI, vol.8, pp.234-259, 1968.

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

J. Krajícek and P. Pudlák, Abstract, The Journal of Symbolic Logic, vol.1130, issue.03, pp.1063-1079, 1989.
DOI : 10.1016/0304-3975(85)90144-6

S. R. Buss, Abstract, The Journal of Symbolic Logic, vol.22, issue.04, pp.916-927, 1987.
DOI : 10.1016/0304-3975(85)90144-6

F. Lamarche, Exploring the gap between linear and classical logic, Theory and Applications of Categories, vol.18, issue.18, pp.473-535, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00113785

L. Straßburger, On the axiomatisation of Boolean categories with and without medial, Theory and Applications of Categories, vol.18, issue.18, pp.536-601, 2007.

G. Japaridze, Cirquent Calculus Deepened, Journal of Logic and Computation, vol.18, issue.6, pp.983-1028, 2008.
DOI : 10.1093/logcom/exn019

P. Bruscoli, A. Guglielmi, T. Gundersen, and M. Parigot, A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae, LNCS, vol.6355, pp.16-136, 2010.
DOI : 10.1007/978-3-642-17511-4_9
URL : https://hal.archives-ouvertes.fr/hal-00529320

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