Term Rewriting and All That, 1998. ,
Unification Theory, Handbook of Automated Reasoning, pp.445-532, 2001. ,
Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994. ,
DOI : 10.1093/logcom/4.3.217
Efficient Algorithms for Bounded Rigid E-unification, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), pp.70-85, 2015. ,
DOI : 10.1007/10721959_17
Theorem Proving with Bounded Rigid E-Unification, Proc. Conference on Automated Deduction (CADE), volume 9195 of Lecture Notes in Computer Science, 2015. ,
DOI : 10.1007/978-3-319-21401-6_39
Congruence Closure with Free Variables ,
DOI : 10.1007/10721959_17
URL : https://hal.archives-ouvertes.fr/hal-01442691
Satisfiability Modulo Theories, Handbook of Satisfiability, pp.825-885, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
The SMT-LIB Standard: Version 2.0, International Workshop on Satisfiability Modulo Theories (SMT), 2010. ,
DOI : 10.1007/978-3-642-19583-9_2
Ridig E-Unification Automated Deduction: A Basis for Applications, Foundations: Calculi and Methods, vol.1, 1998. ,
veriT: An Open, Trustable and Efficient SMT-Solver, Proc. Conference on Automated Deduction (CADE), pp.151-156, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634
Efficient E-Matching for SMT Solvers, Proc. Conference on Automated Deduction, pp.183-198, 2007. ,
DOI : 10.1007/978-3-540-73595-3_13
Engineering DPLL(T) + Saturation, International Joint Conference on Automated Reasoning (IJCAR), pp.475-490, 2008. ,
DOI : 10.1007/978-3-540-71070-7_40
Z3: An Efficient SMT Solver, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.337-340, 2008. ,
DOI : 10.1007/978-3-540-78800-3_24
Equality Reasoning in Sequent-Based Calculi, Handbook of Automated Reasoning, pp.611-706, 2001. ,
DOI : 10.1016/B978-044450813-3/50012-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.5202
Computing prime implicants, 2013 Formal Methods in Computer-Aided Design, pp.46-52, 2013. ,
DOI : 10.1109/FMCAD.2013.6679390
Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005. ,
DOI : 10.1145/1066100.1066102
URL : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.70.1745&rep=rep1&type=pdf
First-Order Logic and Automated Theorem Proving, 1990. ,
DOI : 10.1007/978-1-4612-2360-3
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV), pp.306-320, 2009. ,
DOI : 10.1007/978-3-540-78800-3_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.833
A rule-based algorithm for rigid E-unification, Computational Logic and Proof Theory: Third Kurt Gödel Colloquium, KGC'93, pp.202-210, 1993. ,
DOI : 10.1007/BFb0022569
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.5053
Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980. ,
DOI : 10.1145/322186.322198
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.125.3226
Fast congruence closure and extensions. Information and Computation, Special Issue: 16th International Conference on Rewriting Techniques and Applications, pp.557-580, 2007. ,
DOI : 10.1016/j.ic.2006.08.009
URL : http://doi.org/10.1016/j.ic.2006.08.009
GRASShopper, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.124-139, 2014. ,
DOI : 10.1007/978-3-642-54862-8_9
Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014. ,
DOI : 10.1109/FMCAD.2014.6987613
Quantifier Instantiation Techniques for Finite Model Finding in SMT, Proc. Conference on Automated Deduction (CADE), pp.377-391, 2013. ,
DOI : 10.1007/978-3-642-38574-2_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.567.7320
E-Matching with Free Variables, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp.359-374, 2012. ,
DOI : 10.1007/978-3-642-28717-6_28
Rigid E-Unification Revisited, Proc. Conference on Automated Deduction (CADE), volume 1831 of Lecture Notes in Computer Science, pp.220-234, 2000. ,
DOI : 10.1007/10721959_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7046