D. Bechet, P. De-groote, and C. Retoré, A complete axiomatisation for the inclusion of series-parallel partial orders, Rewriting Techniques and Applications, pp.230-240, 1997.
DOI : 10.1007/3-540-62950-5_74

K. Brünnler and A. F. Tiu, A Local System for Classical Logic, No complete linear term rewriting system for propositional logic 3, 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

M. Chein, Algorithmes d'écriture de fonctions booléennes croissantes en sommes et produits, pp.97-105, 1967.

S. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing , STOC '71, pp.151-158, 1971.
DOI : 10.1145/800157.805047

S. Cook and R. Reckhow, On the lengths of proofs in the propositional calculus (preliminary version), Proceedings of the 6th annual ACM Symposium on Theory of Computing, pp.135-148, 1974.

Y. Crama, L. Peter, and . Hammer, Boolean functions: Theory, algorithms, and applications, 2011.
DOI : 10.1017/CBO9780511852008

A. Das, On the Proof Complexity of Cut-Free Bounded Deep Inference, LNAI, vol.4, issue.1:9, pp.134-148, 2011.
DOI : 10.2307/2273702

A. Das, Rewriting with linear inferences in propositional logic, LIPIcs, vol.21, issue.13, pp.158-173, 2013.

N. Dershowitz and J. Hsiang, Rewrite methods for clausal and non-clausal theorem proving, Automata, Languages and Programming, pp.331-346, 1983.

M. Dubiner and U. Zwick, Amplification by Read-Once Formulas, SIAM Journal on Computing, vol.26, issue.1, pp.15-38, 1997.
DOI : 10.1137/S009753979223633X

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

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. Gurvich, Repetition-free boolean functions, Uspekhi Matematicheskikh Nauk, vol.32, issue.1, pp.183-184, 1977.

A. Gurvich, On the normal form of positional games, Soviet math. dokl, pp.572-574, 1982.

R. Heiman, I. Newman, and A. Wigderson, On read-once threshold formulae and their randomized decision tree complexity, Theoret. Comp. Science, pp.78-87, 1994.

L. Hellerstein and M. Karpinski, Computational complexity of learning read-once formulas over different bases, 1990.

J. Hsiang, Refutational theorem proving using term-rewriting systems, Artificial Intelligence, vol.25, issue.3, pp.255-300, 1985.
DOI : 10.1016/0004-3702(85)90074-8

A. Vasilevich and K. , Non-repeating contact schemes and non-repeating superpositions of functions of algebra of logic. Trudy Matematicheskogo Instituta im, VA Steklova, vol.51, pp.186-225, 1958.

L. A. Levin, Universal sequential search problems, Problemy Peredachi Informatsii, vol.9, issue.3, pp.115-116, 1973.

R. H. Möhring, Computationally Tractable Classes of Ordered Sets, Algorithms and Order, pp.105-194, 1989.
DOI : 10.1007/978-94-009-2639-4_4

C. Retoré, Réseaux et Séquents Ordonnés, p.23, 1993.

L. Straßburger, A characterisation of medial as rewriting rule, LNCS, vol.4533, pp.344-358, 2007.

L. Straßburger, Extension without cut, Annals of Pure and Applied Logic, vol.163, issue.12, 1925.
DOI : 10.1016/j.apal.2012.07.004

G. Valiant, Short monotone formulae for the majority function, Journal of Algorithms, vol.5, issue.3, pp.363-366, 1984.
DOI : 10.1016/0196-6774(84)90016-6