TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism

Jasmin Blanchette 1 Andrei Paskevich 2, 3
3 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : The TPTP World is a well-established infrastructure for automatic theorem provers. It defines several concrete syntaxes, notably an untyped first-order form (FOF) and a typed first-order form (TFF0), that have become de facto standards. This paper introduces the TFF1 format, an extension of TFF0 with rank-1 polymorphism. The format is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. It opens the door to useful middleware, such as monomorphizers and other translation tools that encode polymorphism in FOF or TFF0. Ultimately, the hope is that TFF1 will be implemented in popular automatic theorem provers.
Type de document :
Communication dans un congrès
M.P. Bonacina. CADE - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.414-420, 2013, LNCS
Liste complète des métadonnées

https://hal.inria.fr/hal-00825086
Contributeur : Andrei Paskevich <>
Soumis le : mercredi 22 mai 2013 - 22:08:54
Dernière modification le : jeudi 9 février 2017 - 15:55:07

Fichier

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

Identifiants

  • HAL Id : hal-00825086, version 1

Citation

Jasmin Blanchette, Andrei Paskevich. TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. M.P. Bonacina. CADE - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.414-420, 2013, LNCS. <hal-00825086>

Partager

Métriques

Consultations de
la notice

181

Téléchargements du document

156