Escape to ATP for Mizar

Abstract : An interactive ATP service is a new feature in the Mizar proof assistant. The functionality of the service is in many respects analogous to the Sledgehammer subsystem of Isabelle/HOL. The ATP service requires minimal user configuration and is accessible via a few keystrokes from within Mizar mode in Emacs. In return, for a given goal formula, the ATP service, when it succeeds, finds premises sufficient to prove the goal. The ''escape'' to ATP uses a sound translation from Mizar's language to that of first-order provers, the same translation that has been used in the more batch oriented Automated Reasoning for Mizar (MizAR) web services presented in [Urban2010]. We briefly present the interactive ATP service followed by an account of initial experiments with the tool. We claim with some confidence that the tool will substantially ease the process of preparing new Mizar articles.
Type de document :
Communication dans un congrès
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Liste complète des métadonnées

https://hal.inria.fr/hal-00677240
Contributeur : Pascal Fontaine <>
Soumis le : mercredi 7 mars 2012 - 15:54:58
Dernière modification le : mercredi 7 mars 2012 - 16:23:54
Document(s) archivé(s) le : vendredi 23 novembre 2012 - 16:01:21

Fichier

paper1.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00677240, version 1

Collections

Citation

Piotr Rudnicki, Josef Urban. Escape to ATP for Mizar. Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011. 〈hal-00677240〉

Partager

Métriques

Consultations de la notice

108

Téléchargements de fichiers

215