Incidence simplicial matrices formalized in Coq/SSReflect - Archive ouverte HAL Access content directly
Conference Papers Lecture Notes in Artificial Intelligence Year : 2011

Incidence simplicial matrices formalized in Coq/SSReflect

(1) , (1) , (2) , (2)
1
2
Jónathan Heras
  • Function : Author
  • PersonId : 904378
María Poza
  • Function : Author
  • PersonId : 904379
Maxime Denes
  • Function : Author
  • PersonId : 904380
Laurence Rideau

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.
Fichier principal
Vignette du fichier
ismfis.pdf (146.93 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

Cite

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
180 View
326 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More