D. Basin and H. Ganzinger, Automated complexity analysis based on ordered resolution, Journal of the ACM, vol.48, issue.1, pp.70-109, 2001.
DOI : 10.1145/363647.363681

A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, Concurrency theory, pp.1243-135, 1997.
DOI : 10.1007/3-540-63141-0_10

N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Communications of the ACM, vol.22, issue.8, p.465476, 1979.
DOI : 10.1145/359138.359142

G. Dowek and Y. Jiang, Cut-elimination and the decidability of reachability in alternating pushdown systems, arXiv:1410, p.2014

R. Dyckhoff, Contraction-Free Sequent Calculi for Intuitionistic Logic, The Journal of Symbolic Logic, pp.795-807, 1992.

R. Dyckhoff and S. Lengrand, LJQ: A Strongly Focused Calculus for Intuitionistic Logic, Computability in Europe, pp.173-185, 2006.
DOI : 10.1090/trans2/094/02
URL : https://hal.archives-ouvertes.fr/hal-00150287

R. Dyckhoff and S. Negri, Admissibility of structural rules for contraction-free systems of intuitionistic logic The Journal of Symbolic Logic, pp.1499-1518, 2000.

T. Frühwirth, E. Shapiro, M. Vardi, and E. Yardeni, Logic programs as types for logic programs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.300-309, 1991.
DOI : 10.1109/LICS.1991.151654

J. Goubault-larrecq, Deciding by resolution, Information Processing Letters, vol.95, issue.3, pp.401-408, 2005.
DOI : 10.1016/j.ipl.2005.04.007

J. Hudelmaier, -Space Decision Procedure for Intuitionistic Propositional Logic, Journal of Logic and Computation, vol.3, issue.1, pp.63-76, 1993.
DOI : 10.1093/logcom/3.1.63

S. C. Kleene, Introduction to Metamathematics, 1952.

D. A. Mcallester, Automatic recognition of tractability in inference relations, Journal of the ACM, vol.40, issue.2, pp.284-303, 1993.
DOI : 10.1145/151261.151265

D. Prawitz, Natural Deduction, Almqvist & Wiksell, 1965.