L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder, Basic paramodulation. Research Report MPI-I-93-236
DOI : 10.1006/inco.1995.1131
URL : http://doi.org/10.1006/inco.1995.1131

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB standard version 2.0, 2010.

F. Bobot, S. Conchon, E. Contejean, and S. Lescuyer, Implementing polymorphism in SMT solvers, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, pp.1-5, 2008.
DOI : 10.1145/1512464.1512466

L. De-moura and N. Bjørner, Engineering dpll (t)+ saturation. Automated Reasoning, pp.475-490, 2008.

L. De, M. , and N. Bjørner, Efficient E-matching for SMT solvers, p.7, 2007.

L. De, M. , and N. Bjørner, Z3: An efficient SMT solver, TACAS, 2008.

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

Y. Ge and L. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_25

Y. Ge, C. Barrett, and C. Tinelli, Solving quantified verification conditions using satisfiability modulo theories, 2007.
DOI : 10.1007/978-3-540-73595-3_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.192.6628

S. Jacobs and V. Kuncak, Towards Complete Reasoning about Axiomatic Specifications, Proceedings of VMCAI, pp.278-293, 2011.
DOI : 10.1007/978-3-540-25984-8_9

S. Lahiri and S. Qadeer, Back to the future, ACM SIGPLAN Notices, vol.43, issue.1, pp.171-182, 2008.
DOI : 10.1145/1328897.1328461

M. Moskal, Programming with triggers, Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT '09, pp.20-29, 2009.
DOI : 10.1145/1670412.1670416

G. Nelson, Techniques for program verification, 1981.

P. Rümmer, E-Matching with Free Variables, 2012.
DOI : 10.1007/978-3-642-28717-6_28