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

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.

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

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

M. Beeson, Lambda logic, IJCAR 2004, vol.3097, pp.460-474, 2004.

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 and M. Kohlhase, System description: LEO-a higher-order theorem prover, CADE-15, vol.1421, pp.139-144, 1998.

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.

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.

S. Cruanes, Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, École polytechnique, 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

J. Filliâtre and A. Paskevich, Why3-where programs meet provers, ESOP 2013, vol.7792, pp.125-128, 2013.

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

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.

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

B. Löchner, Things to know when implementing KBO, J. Autom. Reason, vol.36, issue.4, pp.289-310, 2006.

W. Mccune, Experiments with discrimination-tree indexing and path indexing for term retrieval, J. Autom. Reason, vol.9, issue.2, pp.147-167, 1992.

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.

S. Schulz, Fingerprint indexing for paramodulation and rewriting, IJCAR 2012, vol.7364, pp.477-483, 2012.

S. Schulz, Simple and efficient clause subsumption with feature vector indexing, Automated Reasoning and MathematicsEssays in Memory of William W. McCune, vol.7788, pp.45-67, 2013.

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

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

A. Stump, G. Sutcliffe, and C. Tinelli, StarExec: A cross-community infrastructure for logic solving, IJCAR 2014, vol.8562, pp.367-373, 2014.

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, The CADE-26 automated theorem proving system competition-CASC-26, AI Commun, vol.30, issue.6, pp.419-432, 2017.

P. Vukmirovi?, Implementation of Lambda-Free Higher-Order Superposition, 2018.

P. Vukmirovi?, J. C. Blanchette, S. Cruanes, and S. Schulz, Extending a brainiac prover to lambda-free higher-order logic (technical report), 2019.

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