P. B. Andrews, Resolution in type theory, J. Symb. Log, vol.36, issue.3, pp.414-432, 1971.

P. B. Andrews, On connections and higher-order logic, J. Autom. Reason, vol.5, issue.3, pp.257-291, 1989.

P. B. Andrews, Classical type theory, Handbook of Automated Reasoning, vol.II, pp.965-1007, 2001.

P. B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning et al., TPS: A theorem-proving system for classical type theory, J. Autom. Reason, vol.16, issue.3, pp.321-353, 1996.

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994.

J. Backes and C. E. Brown, Analytic tableaux for higher-order logic with choice, J. Autom. Reason, vol.47, issue.4, pp.451-479, 2011.

H. Barbosa, A. Reynolds, P. Fontaine, D. E. Ouraoui, and C. Tinelli, Higher-order SMT solving (work in progress), SMT 2018, 2018.

H. Becker, J. C. Blanchette, U. Waldmann, and D. Wand, A transfinite Knuth-Bendix order for lambda-free higher-order terms, LNCS, vol.10395, pp.432-453, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592186

A. Bentkamp, Formalization of the embedding path order for lambda-free higherorder terms, Archive of Formal Proofs, 2018.

A. Bentkamp, J. Blanchette, S. Tourret, P. Vukmirovi?, and U. Waldmann, Superposition with lambdas (technical report), 2019.

A. Bentkamp, J. C. Blanchette, S. Cruanes, and U. Waldmann, Superposition for lambda-free higher-order logic, IJCAR 2018, vol.10900, pp.28-46, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01904595

C. Benzmüller, Extensional higher-order paramodulation and RUE-resolution, CADE-16, vol.1632, pp.399-413, 1999.

C. Benzmüller and M. Kohlhase, Extensional higher-order resolution, CADE-15, vol.1421, pp.56-71, 1998.

C. Benzmüller and D. Miller, Automation of higher-order logic, Computational Logic, Handbook of the History of Logic, vol.9, pp.215-254, 2014.

C. Benzmüller and L. C. Paulson, Multimodal and intuitionistic logics in simple type theory, Log. J. IGPL, vol.18, issue.6, pp.881-892, 2010.

C. Benzmüller, N. Sultana, L. C. Paulson, and F. Theiss, The higher-order prover Leo-II, J. Autom. Reason, vol.55, issue.4, pp.389-404, 2015.

A. Bhayat and G. Reger, Set of support for higher-order reasoning, PAAR-2018. CEUR Workshop Proceedings, vol.2162, pp.2-16, 2018.

J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding monomorphic and polymorphic types, Log. Meth. Comput. Sci, vol.12, issue.4, 2016.

J. C. Blanchette and A. Paskevich, TFF1: The TPTP typed first-order form with rank-1 polymorphism, CADE-24, vol.7898, pp.414-420, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00825086

J. C. Blanchette, U. Waldmann, and D. Wand, A lambda-free higher-order recursive path order, FoSSaCS 2017, vol.10203, pp.461-479, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592189

F. Blanqui, J. P. Jouannaud, and A. Rubio, The computability path ordering, Log. Meth. Comput. Sci, vol.11, issue.4, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01163091

S. Böhme and T. Nipkow, Sledgehammer: Judgement Day, IJCAR 2010, vol.6173, pp.107-121, 2010.

C. E. Brown, Satallax: An automatic higher-order prover, IJCAR 2012, vol.7364, pp.111-117, 2012.

N. G. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math, vol.75, issue.5, pp.381-392, 1972.

I. Cervesato and F. Pfenning, A linear spine calculus, J. Log. Comput, vol.13, issue.5, pp.639-688, 2003.

S. Cruanes, Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01223502

S. Cruanes, Superposition with structural induction, FroCoS 2017, vol.10483, pp.172-188, 2017.
URL : https://hal.archives-ouvertes.fr/hal-02062459

?. Czajka and C. Kaliszyk, Hammer for Coq: Automation for dependent type theory, 2018.

D. J. Dougherty, Higher-order unification via combinators, Theor. Comput. Sci, vol.114, issue.2, pp.273-298, 1993.

G. Dowek, Higher-order unification and matching, Handbook of Automated Reasoning, vol.II, pp.1009-1062, 2001.

M. Fitting, Types, Tableaus, and Gödel's God, 2002.

H. Ganzinger and J. Stuber, Superposition with equivalence reasoning and delayed clause normal form transformation, Information and Computation, vol.199, issue.1-2, pp.3-23, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00099710

A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, Extensional crisis and proving identity, ATVA 2014, vol.8837, pp.185-200, 2014.

L. Henkin, Completeness in the theory of types, J. Symb. Log, vol.15, issue.2, pp.81-91, 1950.

G. P. Huet, A mechanization of type theory, IJCAI-73, pp.139-146, 1973.

G. P. Huet, A unification algorithm for typed lambda-calculus, Theor. Comput. Sci, vol.1, issue.1, pp.27-57, 1975.

D. C. Jensen and T. Pietrzykowski, Mechanizing ?-order type theory through unification, Theor. Comput. Sci, vol.3, issue.2, pp.123-171, 1976.

J. P. Jouannaud and A. Rubio, Rewrite orderings for higher-order terms in eta-long beta-normal form and recursive path ordering, Theor. Comput. Sci, vol.208, issue.1-2, pp.33-58, 1998.

J. P. Jouannaud and A. Rubio, Polymorphic higher-order recursive path orderings, J. ACM, vol.54, issue.1, pp.1-2, 2007.

C. Kaliszyk, G. Sutcliffe, and F. Rabe, TH1: The TPTP typed higher-order form with rank-1 polymorphism, PAAR-2016. CEUR Workshop Proceedings, vol.1635, pp.41-55, 2016.

C. Kaliszyk and J. Urban, HOL(y)Hammer: Online ATP service for HOL Light, Math. Comput. Sci, vol.9, issue.1, pp.5-22, 2015.

M. Kohlhase, Higher-order tableaux, TABLEAUX '95, vol.918, pp.294-309, 1995.

K. Konrad, HOT: A concurrent automated theorem prover based on higher-order tableaux, TPHOLs '98, vol.1479, pp.245-261, 1998.

L. Kovács and A. Voronkov, First-order theorem proving and Vampire, CAV 2013, vol.8044, pp.1-35, 2013.

T. Libal, Regular patterns in second-order unification, CADE-25, vol.9195, pp.557-571, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01242215

F. Lindblad, A focused sequent calculus for higher-order logic, IJCAR 2014, vol.8562, pp.61-75, 2014.

R. Mayr and T. Nipkow, Higher-order rewrite systems and their confluence, Theor. Comput. Sci, vol.192, issue.1, pp.3-29, 1998.

J. Meng and L. C. Paulson, Translating higher-order clauses to first-order clauses, J. Autom. Reason, vol.40, issue.1, pp.35-60, 2008.

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, J. Log. Comput, vol.1, issue.4, pp.497-536, 1991.

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving, Handbook of Automated Reasoning, vol.I, pp.371-443, 2001.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, IWIL-2010. EPiC, vol.2, pp.1-11, 2012.

J. Robinson, Mechanizing higher order logic, Machine Intelligence, vol.4, pp.151-170, 1969.

J. Robinson, A note on mechanizing higher order logic, Machine Intelligence, vol.5, pp.121-135, 1970.

A. Schlichtkrull, J. C. Blanchette, D. Traytel, and U. Waldmann, Formalizing Bachmair and Ganzinger's ordered resolution prover, IJCAR 2018, vol.10900, pp.89-107, 2018.

S. Schulz, System description: E 1.8, vol.8312, pp.735-743, 2013.

W. Snyder, Higher order E-unification, CADE-10, vol.449, pp.573-587, 1990.

W. Snyder and J. H. Gallier, Higher-order unification revisited: Complete sets of transformations, J. Symb. Comput, vol.8, issue.1/2, pp.101-140, 1989.

A. Steen and C. Benzmüller, The higher-order prover Leo-III, IJCAR 2018, vol.10900, pp.108-116, 2018.

G. Sutcliffe, The TPTP problem library and associated infrastructure-from CNF to TH0, J. Autom. Reason, vol.59, issue.4, pp.483-502, 2017.

G. Sutcliffe, C. Benzmüller, C. E. Brown, and F. Theiss, Progress in the development of automated theorem proving for higher-order logic, LNCS, vol.5663, pp.116-130, 2009.

J. Urban, P. Rudnicki, and G. Sutcliffe, ATP and presentation service for Mizar formalizations, J. Autom. Reason, vol.50, issue.2, pp.229-241, 2013.

P. Vukmirovi?, J. C. Blanchette, S. Cruanes, and S. Schulz, Extending a brainiac prover to lambda-free higher-order logic, TACAS 2019, pp.192-210, 2019.

U. Waldmann, Automated reasoning II. Lecture notes, 2016.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS version 3.5, vol.5663, pp.140-145, 2009.