Defining the meaning of TPTP formatted proofs

Roberto Blanco 1, 2, 3 Tomer Libal 1, 2, 3 Dale Miller 1, 2, 3
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
11th International Workshop on the Implementation of Logics, Nov 2015, Suva, Fiji. 〈http://www.eprover.org/EVENTS/IWIL-2015.html〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01238434
Contributeur : Roberto Blanco <>
Soumis le : vendredi 4 décembre 2015 - 20:43:29
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : samedi 29 avril 2017 - 05:17:47

Fichier

iwil2015_paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01238434, version 1

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. 〈http://www.eprover.org/EVENTS/IWIL-2015.html〉. 〈hal-01238434〉

Partager

Métriques

Consultations de la notice

223

Téléchargements de fichiers

171