Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CADE

2009

Springer

2009

Springer

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...

Related Content

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)