Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Defining the meaning of TPTP formatted proofs

Roberto Blanco 1, 2 Tomer Libal 1, 2 Dale Miller 1, 2 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : The TPTP library is one of the leading problem libraries in the automated theorem proving community. Over time, support was added for problems beyond those in first-order clausal form. TPTP has also been augmented with support for various proof formats output by theorem provers. Such proofs can also be maintained in the TSTP proof library. In this paper we propose an extension of this framework to support the semantic specification of the inference rules used in proofs.
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Roberto Blanco Connect in order to contact the contributor
Submitted on : Friday, December 4, 2015 - 8:43:29 PM
Last modification on : Wednesday, February 2, 2022 - 3:55:21 PM
Long-term archiving on: : Saturday, April 29, 2017 - 5:17:47 AM


Files produced by the author(s)


  • HAL Id : hal-01238434, version 1


Roberto Blanco, Tomer Libal, Dale Miller. Defining the meaning of TPTP formatted proofs. 11th International Workshop on the Implementation of Logics, Nov 2015, Suva, Fiji. ⟨hal-01238434⟩



Record views


Files downloads