Beagle as a HOL4 external ATP method

Abstract : This paper presents BEAGLE TAC, a HOL4 tactic for using Beagle as an external ATP for discharging HOL4 goals. We implement a translation of the higher-order goals to the TFA format of TPTP and add trace output to Beagle to reconstruct the intermediate steps derived by the ATP in HOL4. Our translation combines the characteristics of existing successful translations from HOL to FOL and SMT-LIB; however, we needed to adapt certain stages of the translation in order to benefit form the expressiveness of the TFA format and the power of Beagle. In our initial experiments, we demonstrate that our system can prove, without any arithmetic lemmas, 81% of the goals solved by Metis.
Type de document :
Communication dans un congrès
PAAR - Fourth Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienne, Austria. 2014
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01089316
Contributeur : Chantal Keller <>
Soumis le : lundi 1 décembre 2014 - 15:07:53
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : lundi 2 mars 2015 - 13:33:47

Fichier

beagle-hol4.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01089316, version 1

Collections

Citation

Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish. Beagle as a HOL4 external ATP method. PAAR - Fourth Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienne, Austria. 2014. 〈hal-01089316〉

Partager

Métriques

Consultations de la notice

149

Téléchargements de fichiers

344