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

https://hal.inria.fr/hal-01238434
Contributor : Roberto Blanco <>
Submitted on : Friday, December 4, 2015 - 8:43:29 PM
Last modification on : Friday, April 30, 2021 - 10:02:40 AM
Long-term archiving on: : Saturday, April 29, 2017 - 5:17:47 AM

File

iwil2015_paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01238434, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

491

Files downloads

573