Sciweavers

LPAR
2012
Springer

The TPTP Typed First-Order Form with Arithmetic

12 years 2 months ago
The TPTP Typed First-Order Form with Arithmetic
Abstract. The TPTP World is a well established infrastructure supporting research, development, and deployment of Automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. This paper describes these developments. 1 Motivation and History The TPTP World [32] is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP World is based on the Thousands of Problems for Theorem Provers (TPTP) problem library [30], and includes the TPTP language, the SZS ontologies, the Thousands of Solutions from Theorem Provers (TSTP) solution library, various tools associated with the libraries, and the CADE ATP System Competition (CASC). This infrastructure has been central to the progress that has been made in the development of high performance first-order ATP systems – most state of the art systems nativel...
Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Pe
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where LPAR
Authors Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Peter Baumgartner
Comments (0)