Sciweavers

CADE
2009
Springer

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

14 years 4 months ago
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...
Chad E. Brown, Christoph Benzmüller, Frank Th
Added 23 Nov 2009
Updated 23 Nov 2009
Type Conference
Year 2009
Where CADE
Authors Chad E. Brown, Christoph Benzmüller, Frank Theiss, Geoff Sutcliffe
Comments (0)