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].
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072585
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:20:38 AM
Last modification on : Tuesday, October 22, 2019 - 3:10:09 PM
Long-term archiving on: Sunday, April 4, 2010 - 11:14:25 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

102

Files downloads

200