A. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

D. Marcello, M. Agostino, and . Mondadori, The taming of the cut. Classical refutations with analytic cut, J. Log. Comput, vol.4, issue.3, pp.285-319, 1994.

A. Felty and D. Miller, Specifying theorem provers in a higher-order logic programming language, Ninth International Conference on Automated Deduction, pp.61-80, 1988.
DOI : 10.1007/BFb0012823

G. and G. Gentzen, Investigations into logical deductions The Collected Papers of Gerhard Gentzen, pp.68-131, 1969.

G. Girard, Le Point Aveugle: Cours de logique: Tome 1, Vers la perfection, 2006.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

J. Hodas and D. Miller, Logic Programming in a Fragment of Intuitionistic Linear Logic, Information and Computation, vol.110, issue.2, pp.327-365, 1994.
DOI : 10.1006/inco.1994.1036

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, Computer Science Logic LNCS, vol.4646, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231

D. Mil96 and . Miller, Forum: A multiple-conclusion specification logic, Theoretical Computer Science, vol.165, issue.1, pp.201-232, 1996.

M. , D. Miller, and V. Nigam, Incorporating tables into proofs, Computer Science Logic LNCS, vol.4646, pp.466-480, 2007.

M. , D. Miller, and E. Pimentel, Using linear logic to reason about sequent systems, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp.2-23, 2002.

M. , D. Miller, and E. Pimentel, Linear logic as a framework for specifying sequent calculus, Logic Colloquium '99: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, pp.111-135, 2004.

V. Nigam and D. Miller, Focusing in Linear Meta-logic
DOI : 10.1007/978-3-540-71070-7_42
URL : https://hal.archives-ouvertes.fr/inria-00281631

S. Negri and J. V. Plato, Structural Proof Theory, 2001.
DOI : 10.1017/CBO9780511527340
URL : https://hal.archives-ouvertes.fr/hal-01251230

M. Parigot, Free deduction: An analysis of ???Computations??? in classical logic, Proceedings of the First Russian Conference on Logic Programming, pp.361-380, 1992.
DOI : 10.1007/3-540-55460-2_27

F. Pfe89 and . Pfenning, Elf: A language for logic definition and verified metaprogramming, Fourth Annual Symposium on Logic in Computer Science, pp.313-321, 1989.

F. Pfe00 and . Pfenning, Structural cut elimination I. intuitionistic and classical logic, Information and Computation, vol.157, issue.12, pp.84-141, 2000.

E. Gouvêa-pimentel and M. G. Brasil, Lógica linear e a especificação de sistemas computacionais, 2001.

E. Pimentel and D. Miller, On the Specification of Sequent Systems, LPAR 2005: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, number 3835 in LNAI, pp.352-366, 2005.
DOI : 10.1007/11591191_25

D. Prawitz, Natural Deduction Normal natural deduction proofs (in classical logic), Almqvist & Wiksell Studia Logica, vol.60, issue.1, pp.67-106, 1965.

P. Schroeder-heister, A natural extension of natural deduction, The Journal of Symbolic Logic, vol.36, issue.04, pp.1284-1300, 1984.
DOI : 10.1007/978-94-009-9825-4_2

R. M. Smullyan, Analytic cut, The Journal of Symbolic Logic, vol.1, issue.04, pp.560-564, 1968.
DOI : 10.2307/2271362

A. S. Troelstra, H. Schwichtenberg, and V. Plato, Basic Proof Theory Natural deduction with general elimination rules, Archive for Mathematical Logic, vol.40, issue.vP017, pp.541-567, 1996.