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

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.4450

M. P. Bonacina, C. Lynch, and L. M. De-moura, On Deciding Satisfiability by Theorem Proving with Speculative Inferences, Journal of Automated Reasoning, vol.13, issue.4???6, pp.161-189, 2011.
DOI : 10.1007/s10817-010-9213-y

K. Chaudhuri, The Focused Inverse Method for Linear Logic, 2006.

K. Chaudhuri, Magically Constraining the Inverse Method Using Dynamic Polarity Assignment, Proc. 17th Int. Conf. on Logic for Programming, Artificial Intelligence , and Reasoning (LPAR), pp.202-216, 2010.
DOI : 10.1007/978-3-642-16242-8_15
URL : https://hal.archives-ouvertes.fr/inria-00535948

K. Chaudhuri, F. Pfenning, and G. Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method, Journal of Automated Reasoning, vol.2, issue.5, pp.133-177, 2008.
DOI : 10.1007/s10817-007-9091-0

Z. Chihani, D. Miller, and F. Renaud, Foundational Proof Certificates in First-Order Logic, Conference on Automated Deduction 2013, number 7898 in Lecture Notes in Artificial Intelligence, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

K. Claessen and N. Sorensson, New techniques that improve MACE-style finite model finding, Proceedings of the CADE-19 Workshop: Model Computation -Principles, 2003.

A. Degtyarev and A. Voronkov, The Inverse Method, Handbook of Automated Reasoning (in 2 volumes), pp.179-272, 2001.
DOI : 10.1016/B978-044450813-3/50006-0

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

C. Lynch, Unsound Theorem Proving, Procedings of the 13th Annual EACS Conference on Computer Science Logic, pp.473-487, 2004.
DOI : 10.1007/978-3-540-30124-0_36

W. Mccune, Mace4 reference manual and guide, 2003.
DOI : 10.2172/822574

S. Mclaughlin and F. Pfenning, Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic, 15th International Conference on Logic, Programming, pp.174-181, 2008.
DOI : 10.1007/978-3-540-89439-1_12

S. Mclaughlin and F. Pfenning, Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method, Proceedings of the 22nd International Conference on Automated Deduction, pp.230-244, 2009.
DOI : 10.1007/3-540-61511-3_65

T. Raths, J. Otten, and C. Kreitz, The ILTP Problem Library for Intuitionistic Logic, Journal of Automated Reasoning, vol.2, issue.2, pp.261-271, 2007.
DOI : 10.1007/s10817-006-9060-z