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

• Type: Journal
• Year: 2012
• Where: LPAR
• Authors: Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Peter Baumgartner
• Keywords: Arithmetic Problems, Atp System, Automated Reasoning, LPAR 2012, Problem Library