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

H. Clark, J. Gallaire, and . Minker, Negation as Failure, Logic and Databases, 1978.
DOI : 10.1007/978-1-4684-3384-5_11

C. Dershowitz and . Kirchner, Abstract canonical presentations, Theoretical Computer Science, vol.357, issue.1-3, pp.53-69, 2006.
DOI : 10.1016/j.tcs.2006.03.012

URL : https://hal.archives-ouvertes.fr/inria-00121760

Y. Dowek and . Jiang, A logical approach to CTL, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00919467

Y. Dowek and . Jiang, Axiomatizing truth in a finite model, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00919469

E. Frühwirth, M. Shapiro, E. Vardi, and . 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

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

C. Kleene, Introduction to Metamathematics, 1952.

E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebras, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

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

. Sangiorgi, Introduction to Bisimulation and Coinduction, 2011.
DOI : 10.1017/CBO9780511777110

URL : https://hal.archives-ouvertes.fr/hal-00907026