J. 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

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.1-31, 1994.
DOI : 10.1093/logcom/4.3.217

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

R. Bonichon and O. Hermant, A Semantic Completeness Proof for TaMeD, pp.167-181, 2006.
DOI : 10.1007/11916277_12
URL : https://hal.archives-ouvertes.fr/hal-01337086

P. Brauner, C. Houtmann, and C. Kirchner, Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.41-50, 2007.
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557

G. Burel, Embedding Deduction Modulo into a Prover, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15
URL : http://www.ensiie.fr/~guillaume.burel/download/burel10embedding.pdf

G. Burel, Experimenting with Deduction Modulo, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

G. Burel, From Axioms to Rewriting Rules Available on author's web page, 2013.

G. Burel, Cut Admissibility by Saturation, pp.124-138, 2014.
DOI : 10.1007/978-3-319-08918-8_9
URL : https://hal.archives-ouvertes.fr/hal-01097428

G. Burel and G. Dowek, How can we prove that a proof search method is not an instance of another?, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice, LFMTP '09, 2009.
DOI : 10.1145/1577824.1577838

G. Burel and C. Kirchner, Regaining cut admissibility in deduction modulo using abstract completion, Information and Computation, vol.208, issue.2, pp.140-164, 2010.
DOI : 10.1016/j.ic.2009.10.005
URL : https://hal.archives-ouvertes.fr/inria-00132964

R. Samuel and . Buss, Handbook of proof theory, 1998.

K. Chaudhuri and F. Pfenning, A Focusing Inverse Method Theorem Prover for First-Order Linear Logic, pp.69-83, 2005.
DOI : 10.1007/11532231_6
URL : http://www.cs.cmu.edu/afs/cs/user/fp/www/papers/cade05.ps

K. Chaudhuri, F. Pfenning, and G. Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method, Journal of Automated Reasoning, vol.40, pp.2-3, 2008.

Z. Chihani, T. Libal, and G. Reis, The Proof Certifier Checkers, TABLEAUX (LNCS), pp.201-210, 2015.
DOI : 10.1007/978-3-642-45221-5_49
URL : https://hal.archives-ouvertes.fr/hal-01208333

Z. Chihani, D. Miller, and F. Renaud, Foundational Proof Certificates in First-Order Logic, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

E. Deplagne and C. Kirchner, Induction as Deduction Modulo Rapport de recherche. LORIA. http://www.loria.fr/ publications, 2004.

G. Dowek, What Is a Theory?, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

G. Dowek, Truth Values Algebras and Proof Normalization, pp.110-124, 2006.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek, Polarized Resolution Modulo, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/inria-00077199

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

G. Dowek and B. Werner, Arithmetic as a Theory Modulo, pp.423-437, 2005.
DOI : 10.1007/978-3-540-32033-3_31
URL : http://pauillac.inria.fr/~werner/publis/rta05.pdf

M. Farooque, S. Graham-lengrand, and A. Mahboubi, ) and a proof-search strategy for the focused sequent calculus, Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, LFMTP '13, pp.3-14, 2013.
DOI : 10.1145/2503887.2503892

J. Goubault-larrecq, A Note on the Completeness of Certain Refinements of Resolution, 2002.

O. Hermant, Méthodes Sémantiques en Déduction Modulo, 2005.

C. Houtmann, Axiom Directed Focusing, Types for Proofs and Programs, pp.169-185, 2008.
DOI : 10.1016/S0168-0072(00)00032-4
URL : https://hal.archives-ouvertes.fr/inria-00212059

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041
URL : https://doi.org/10.1016/j.tcs.2009.07.041

S. Mclaughlin and F. Pfenning, Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic, LPAR (Lecture Notes in Computer Science), Iliano Cervesato, pp.174-181, 2008.
DOI : 10.1007/978-3-540-89439-1_12

D. Miller and M. Volpe, Focused Labeled Proof Systems for Modal Logic, LPAR (LNCS), pp.266-280, 2015.
DOI : 10.1007/978-3-662-48899-7_19
URL : https://hal.archives-ouvertes.fr/hal-01213858

J. A. Robinson, Automatic Deduction with Hyper-Resolution, International Journal of Computer Mathematics, vol.1, pp.227-234, 1965.
DOI : 10.1007/978-3-642-81952-0_27

P. Schroeder-heister, Cut-elimination in logics with definitional reflection, Nonclassical Logics and Information Processing, pp.146-171, 1990.
DOI : 10.1007/BFb0031929

J. R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM, vol.14, issue.4, pp.687-697, 1967.
DOI : 10.1145/321420.321428

L. Wos, G. A. Robinson, and D. F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM, vol.12, issue.4, pp.536-541, 1965.
DOI : 10.1145/321296.321302