C. Barrett, R. Sebastiani, A. Sanjit, C. Seshia, and . Tinelli, Satisfiability modulo theories, Handbook of Satisfiability, vol.185, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

J. Boudou, A. Fellner, and B. W. Paleo, Skeptik: A proof compression system, Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, International Joint Conference on Automated Reasoning (IJCAR), vol.8562, pp.374-380, 2014.

J. Peter, R. Downey, R. E. Sethi, and . Tarjan, Variations on the common subexpressions problem, Journal of the ACM, vol.27, issue.4, pp.758-771, 1980.

A. Fellner, P. Fontaine, G. Hofferek, and B. W. Paleo, NPcompleteness of small conflict set generation for congruence closure, International Workshop on Satisfiability Modulo Theories (SMT), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01908684

P. Fontaine, Techniques for verification of concurrent systems with invariants, 2004.

P. Fontaine and E. Pascal-gribomont, Using BDDs with combinations of theories, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), vol.2514, pp.190-201, 2002.

G. Nelson and D. C. Oppen, Fast decision procedures based on congruence closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.

R. Nieuwenhuis and A. Oliveras, Union-find and congruence closure algorithms that produce proofs, Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), 2004.

R. Nieuwenhuis and A. Oliveras, Proof-producing congruence closure, Rewriting Techniques and Applications (RTA), vol.3467, pp.453-468, 2005.

R. Nieuwenhuis and A. Oliveras, Fast congruence closure and extensions, formation and Computation, vol.205, pp.557-580, 2007.
DOI : 10.1016/j.ic.2006.08.009
URL : https://doi.org/10.1016/j.ic.2006.08.009