Élimination des quantificateurs sur les réels pour Coq

Résumé : On présente ici l'implémentation en OCaml d'une tactique Coq qui réalise une procédure d'élimination des quantificateurs pour les réels, basée sur la méthode de Hormander.
Type de document :
Communication dans un congrès
Journées Francophones des Langages Applicatifs, Jan 2002, Anglet, France. 2002
Liste complète des métadonnées

https://hal.inria.fr/hal-00819482
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 1 mai 2013 - 15:49:46
Dernière modification le : samedi 27 janvier 2018 - 01:30:55
Document(s) archivé(s) le : vendredi 2 août 2013 - 04:05:58

Fichiers

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

Identifiants

  • HAL Id : hal-00819482, version 1

Collections

Citation

Assia Mahboubi, Loïc Pottier. Élimination des quantificateurs sur les réels pour Coq. Journées Francophones des Langages Applicatifs, Jan 2002, Anglet, France. 2002. 〈hal-00819482〉

Partager

Métriques

Consultations de la notice

196

Téléchargements de fichiers

100