Sign in
Back
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
Book chapter   Peer reviewed

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

Geoff Sutcliffe, Christoph Benzmüller, Chad E Brown and Frank Theiss
Automated Deduction – CADE-22, pp.116-130
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2009
DOI: https://doi.org/10.1007/978-3-642-02959-2_8

Abstract

Ramsey Number Automate Reasoning Proof Assistant Automate Theorem Problem Library
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.

Metrics

5 Record Views

Details