Progress in the Development of
Automated Theorem Proving for
Higher-order Logic
Abstract
The Thousands of Problems for Theorem Provers (TPTP) problem library is the
basis of a well established infrastructure supporting research, development,
and deployment of first-order Automated Theorem Proving (ATP) systems.
Recently, the TPTP has been extended to include problems in higher-order logic, with corresponding infrastructure and resources.
This paper describes the practical progress that has been made towards the
goal of TPTP support for higher-order ATP systems.