Incidence simplicial matrices formalized in Coq/SSReflect

Abstract : Simplicial complexes are at the heart of Computational Algebraic Topology, since they give a concrete, combinatorial description of otherwise rather abstract objects which makes many important topological computations possible. The whole theory has many applications such as coding theory, robotics or digital image analysis. In this paper we present a formalization in the COQ theorem prover of simplicial complexes and their incidence matrices as well as the main theorem that gives meaning to the definition of homology groups and is a first step towards their computation.
Type de document :
Communication dans un congrès
Conference on Intelligent Computer Mathematics, Jul 2011, Bertinoro, Italy. 2011, 〈10.1007/978-3-642-22673-1_3〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00603208
Contributeur : Maxime Dénès <>
Soumis le : vendredi 24 juin 2011 - 14:18:35
Dernière modification le : jeudi 11 janvier 2018 - 16:45:00
Document(s) archivé(s) le : dimanche 25 septembre 2011 - 02:23:18

Fichiers

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

Identifiants

Collections

Citation

Jónathan Heras, María Poza, Maxime Denes, Laurence Rideau. Incidence simplicial matrices formalized in Coq/SSReflect. Conference on Intelligent Computer Mathematics, Jul 2011, Bertinoro, Italy. 2011, 〈10.1007/978-3-642-22673-1_3〉. 〈inria-00603208〉

Partager

Métriques

Consultations de la notice

324

Téléchargements de fichiers

285