L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217-247, 1994.
H. Barbosa. New techniques for instantiation and proof production in SMT solving. PhD thesis, Université de Lorraine, Universidade Federal do Rio Grande do Norte, 2017.
H. Barbosa, P. Fontaine, and A. Reynolds. Congruence closure with free variables. In A. Legay and T. 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.
H. Barbosa, A. Reynolds, D. E. Ouraoui, C. Tinelli, and C. W. Barrett. Extending SMT solvers to higher-order logic. In P. Fontaine, editor, Proc. Conference on Automated Deduction (CADE), volume 11716 of Lecture Notes in Computer Science, pages 35-54. Springer, 2019.
C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability modulo theories. In A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 185 of FAIA, chapter 26, pages 825-885. IOS Press, 2009.
A. Bentkamp, J. Blanchette, S. Tourret, P. Vukmirović,, and U. Waldmann. Superposition with lambdas. In P. Fontaine, editor, Proc. Conference on Automated Deduction (CADE), Lecture Notes in Computer Science. (Accepted for publication). Springer, 2019.
A. Bentkamp, J. C. Blanchette, S. Cruanes, and U. Waldmann. Superposition for lambda-free higher-order logic. In D. Galmiche, S. Schulz, and R. Sebastiani, editors, Int. Joint Conference on Automated Reasoning (IJCAR), volume 10900 of Lecture Notes in Computer Science, pages 28-46. Springer, 2018.
A. Bhayat and G. Reger. Set of support for higher-order reasoning. In B. Konev, J. Urban, and P. Rümmer, editors, Practical Aspects of Automated Reasoning (PAAR), volume 2162 of CEUR Workshop Proceedings, pages 2-16. CEUR-WS.org, 2018.
A. Bhayat and G. Reger. Restricted combinatory unification. In P. Fontaine, editor, Proc. Conference on Automated Deduction (CADE), volume 11716 of Lecture Notes in Computer Science, pages 74-93. Springer, 2019.
J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101-148, 2016.
T. Bouton, D. C. B. de Oliveira, D. Déharbe, and P. Fontaine. veriT: an open, trustable and efficient SMT-solver. In R. A. Schmidt, editor, CADE-22, volume 5663 of LNCS, pages 151-156. Springer, 2009.
C. E. Brown. Satallax: an automatic higher-order prover. In B. Gramlich, D. Miller, and U. Sattler, editors, Int. Joint Conference on Automated Reasoning (IJCAR), volume 7364 of LNCS, pages 111-117. Springer, 2012.
L. de Moura and N. Bjørner. Efficient e-matching for SMT solvers. In F. Pfenning, editor, CADE-21, volume 4603 of LNCS, pages 183-198. Springer, 2007.
D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52:365-473, 2005.
Y. Ge and L. de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In A. Bouajjani and O. Maler, editors, CAV 2009, volume 5643 of LNCS, pages 306-320. Springer, 2009.
J. Meng and L. C. Paulson. Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning, 40(1):35-60, 2008.
R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of automated reasoning, volume 1, pages 371-443. Elsevier Science, 2001.
A. Reynolds, H. Barbosa, and P. Fontaine. Revisiting enumerative instantiation. In D. Beyer and M. Huisman, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part II, volume 10806 of Lecture Notes in Computer Science, pages 112-131. Springer, 2018.
A. Reynolds, C. Tinelli, and L. de Moura. Finding conflicting instances of quantified formulas in SMT. In FMCAD 2014, pages 195-202. IEEE, 2014.
A. Reynolds, C. Tinelli, A. Goel, S. Krstić, M. Deters, and C. Barrett. Quantifier instantiation techniques for finite model finding in SMT. In M. P. Bonacina, editor, CADE-24, volume 7898 of LNCS, pages 377-391. Springer, 2013.
A. Steen and C. Benzmüller. The higher-order prover Leo-III. In D. Galmiche, S. Schulz, and R. Sebastiani, editors, Int. Joint Conference on Automated Reasoning (IJCAR), volume 10900 of LNCS, pages 108-116. Springer, 2018.
R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 1(2):146-160, 1972.
P. Vukmirovic, J. C. Blanchette, S. Cruanes, and S. Schulz. Extending a brainiac prover to lambda-free higher-order logic. In T. Vojnar and L. Zhang, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part I, volume 11427 of Lecture Notes in Computer Science, pages 192-210. Springer, 2019.
