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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00603208
Contributor : Maxime Dénès <>
Submitted on : Friday, June 24, 2011 - 2:18:35 PM
Last modification on : Thursday, January 11, 2018 - 4:45:00 PM
Document(s) archivé(s) le : Sunday, September 25, 2011 - 2:23:18 AM

Files

ismfis.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

336

Files downloads

304