Incidence simplicial matrices formalized in Coq/SSReflect - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Lecture Notes in Artificial Intelligence Année : 2011

Incidence simplicial matrices formalized in Coq/SSReflect

Jónathan Heras
  • Fonction : Auteur
  • PersonId : 904378
María Poza
  • Fonction : Auteur
  • PersonId : 904379
Maxime Denes
  • Fonction : Auteur
  • PersonId : 904380
Laurence Rideau

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
ismfis.pdf (146.93 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00603208 , version 1 (24-06-2011)

Identifiants

Citer

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. ⟨10.1007/978-3-642-22673-1_3⟩. ⟨inria-00603208⟩

Collections

INRIA INRIA2
198 Consultations
375 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More