Progress in the Development of Automated Theorem Proving for Higher-Order Logic

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. 1 Motivation and History There is a well established infrastructure that supports research, development, and deployment of first-order Automated Theorem Proving (ATP) systems, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library [38]. This infrastructure includes the problem library itself, the TPTP language [36], the SZS ontologies [35], the Thousands of Solutions from Theorem Provers (TSTP) solution library, various tools associated with the libraries [34], and the CADE ATP System Com...

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Chad E. Brown, Christoph Benzmüller, Frank Theiss, Geoff Sutcliffe
• Keywords: Automated Reasoning, CADE 2009, First-order Atp Systems, First-order Automated Theorem, Theorem Provers