Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs

Yves Bertot 1 Olivier Pons Loïc Pottier
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : On propose ici des outils pour visualiser de grandes preuves sous forme de graphes de théorèmes et de définitions, où les arrêtes dénotent les dépendances entre deux théorèmes. En particulier, on étudie les moyens de limiter la taille de ces graphes. On a mené les expérimentations à l'aide des systèmes Coq [DFH+93] GraphViz [EGKN] et daVinci [FW98].
Type de document :
Rapport
RR-4052, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072585
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:20:38
Dernière modification le : samedi 27 janvier 2018 - 01:30:58
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:14:25

Fichiers

Identifiants

  • HAL Id : inria-00072585, version 1

Collections

Citation

Yves Bertot, Olivier Pons, Loïc Pottier. Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs. RR-4052, INRIA. 2000. 〈inria-00072585〉

Partager

Métriques

Consultations de la notice

81

Téléchargements de fichiers

169