Salvador Barbarà and Matthew Jackson. Maximin, leximin, and the protective criterion: Characterizations and comparisons. Journal of Economic Theory, 46(1):34-44, 1988.
Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Congruence closure with free variables. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part II, volume 10206 of Lecture Notes in Computer Science, pages 214-230, 2017.
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovíc, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification (CAV), pages 171-177. Springer, 2011.
Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2. 6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www. SMT-LIB. org.
Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking., pages 305-343. Springer, 2018.
David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365-473, 2005.
Yeting Ge and Leonardo Mendonc, a de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification, 21st International Conference, CAV, pages 306-320, 2009.
Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting enumerative instantiation. In Tools and Algorithms for the Construction and Analysis of Systems, volume 10806, pages 112-131, 2018.
Andrew Reynolds, Cesare Tinelli, and Leonardo Mendonc, a de Moura. Finding conflicting instances of quantified formulas in SMT. In Formal Methods In Computer-Aided Design (FMCAD), pages 195-202. IEEE, 2014.
Geoff Sutcliffe. The TPTP problem library and associated infrastructure. J. Autom. Reasoning, 43(4):337-362, 2009.