Resolution in type theory, J. Symb. Log, vol.36, issue.3, pp.414-432, 1971. ,
On connections and higher-order logic, J. Autom. Reason, vol.5, issue.3, pp.257-291, 1989. ,
Classical type theory, Handbook of Automated Reasoning, vol.II, pp.965-1007, 2001. ,
TPS: A theorem-proving system for classical type theory, J. Autom. Reason, vol.16, issue.3, pp.321-353, 1996. ,
Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994. ,
Analytic tableaux for higher-order logic with choice, J. Autom. Reason, vol.47, issue.4, pp.451-479, 2011. ,
Higher-order SMT solving (work in progress), SMT 2018, 2018. ,
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
Formalization of the embedding path order for lambda-free higherorder terms, Archive of Formal Proofs, 2018. ,
Superposition with lambdas (technical report), 2019. ,
Superposition for lambda-free higher-order logic, IJCAR 2018, vol.10900, pp.28-46, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01904595
Extensional higher-order paramodulation and RUE-resolution, CADE-16, vol.1632, pp.399-413, 1999. ,
Extensional higher-order resolution, CADE-15, vol.1421, pp.56-71, 1998. ,
Automation of higher-order logic, Computational Logic, Handbook of the History of Logic, vol.9, pp.215-254, 2014. ,
Multimodal and intuitionistic logics in simple type theory, Log. J. IGPL, vol.18, issue.6, pp.881-892, 2010. ,
The higher-order prover Leo-II, J. Autom. Reason, vol.55, issue.4, pp.389-404, 2015. ,
Set of support for higher-order reasoning, PAAR-2018. CEUR Workshop Proceedings, vol.2162, pp.2-16, 2018. ,
Encoding monomorphic and polymorphic types, Log. Meth. Comput. Sci, vol.12, issue.4, 2016. ,
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
A lambda-free higher-order recursive path order, FoSSaCS 2017, vol.10203, pp.461-479, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01592189
The computability path ordering, Log. Meth. Comput. Sci, vol.11, issue.4, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01163091
Sledgehammer: Judgement Day, IJCAR 2010, vol.6173, pp.107-121, 2010. ,
Satallax: An automatic higher-order prover, IJCAR 2012, vol.7364, pp.111-117, 2012. ,
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. ,
A linear spine calculus, J. Log. Comput, vol.13, issue.5, pp.639-688, 2003. ,
Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01223502
Superposition with structural induction, FroCoS 2017, vol.10483, pp.172-188, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-02062459
Hammer for Coq: Automation for dependent type theory, 2018. ,
Higher-order unification via combinators, Theor. Comput. Sci, vol.114, issue.2, pp.273-298, 1993. ,
Higher-order unification and matching, Handbook of Automated Reasoning, vol.II, pp.1009-1062, 2001. ,
, Types, Tableaus, and Gödel's God, 2002.
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
Extensional crisis and proving identity, ATVA 2014, vol.8837, pp.185-200, 2014. ,
Completeness in the theory of types, J. Symb. Log, vol.15, issue.2, pp.81-91, 1950. ,
A mechanization of type theory, IJCAI-73, pp.139-146, 1973. ,
A unification algorithm for typed lambda-calculus, Theor. Comput. Sci, vol.1, issue.1, pp.27-57, 1975. ,
Mechanizing ?-order type theory through unification, Theor. Comput. Sci, vol.3, issue.2, pp.123-171, 1976. ,
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. ,
Polymorphic higher-order recursive path orderings, J. ACM, vol.54, issue.1, pp.1-2, 2007. ,
TH1: The TPTP typed higher-order form with rank-1 polymorphism, PAAR-2016. CEUR Workshop Proceedings, vol.1635, pp.41-55, 2016. ,
HOL(y)Hammer: Online ATP service for HOL Light, Math. Comput. Sci, vol.9, issue.1, pp.5-22, 2015. ,
Higher-order tableaux, TABLEAUX '95, vol.918, pp.294-309, 1995. ,
HOT: A concurrent automated theorem prover based on higher-order tableaux, TPHOLs '98, vol.1479, pp.245-261, 1998. ,
First-order theorem proving and Vampire, CAV 2013, vol.8044, pp.1-35, 2013. ,
Regular patterns in second-order unification, CADE-25, vol.9195, pp.557-571, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01242215
A focused sequent calculus for higher-order logic, IJCAR 2014, vol.8562, pp.61-75, 2014. ,
Higher-order rewrite systems and their confluence, Theor. Comput. Sci, vol.192, issue.1, pp.3-29, 1998. ,
Translating higher-order clauses to first-order clauses, J. Autom. Reason, vol.40, issue.1, pp.35-60, 2008. ,
A logic programming language with lambda-abstraction, function variables, and simple unification, J. Log. Comput, vol.1, issue.4, pp.497-536, 1991. ,
Paramodulation-based theorem proving, Handbook of Automated Reasoning, vol.I, pp.371-443, 2001. ,
Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, IWIL-2010. EPiC, vol.2, pp.1-11, 2012. ,
Mechanizing higher order logic, Machine Intelligence, vol.4, pp.151-170, 1969. ,
A note on mechanizing higher order logic, Machine Intelligence, vol.5, pp.121-135, 1970. ,
Formalizing Bachmair and Ganzinger's ordered resolution prover, IJCAR 2018, vol.10900, pp.89-107, 2018. ,
, System description: E 1.8, vol.8312, pp.735-743, 2013.
Higher order E-unification, CADE-10, vol.449, pp.573-587, 1990. ,
Higher-order unification revisited: Complete sets of transformations, J. Symb. Comput, vol.8, issue.1/2, pp.101-140, 1989. ,
The higher-order prover Leo-III, IJCAR 2018, vol.10900, pp.108-116, 2018. ,
The TPTP problem library and associated infrastructure-from CNF to TH0, J. Autom. Reason, vol.59, issue.4, pp.483-502, 2017. ,
Progress in the development of automated theorem proving for higher-order logic, LNCS, vol.5663, pp.116-130, 2009. ,
ATP and presentation service for Mizar formalizations, J. Autom. Reason, vol.50, issue.2, pp.229-241, 2013. ,
Extending a brainiac prover to lambda-free higher-order logic, TACAS 2019, pp.192-210, 2019. ,
Automated reasoning II. Lecture notes, 2016. ,
, SPASS version 3.5, vol.5663, pp.140-145, 2009.