Title
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.
Year
DOI
Venue
2011
10.1007/978-3-642-22673-1_3
Calculemus/MKM
Keywords
Field
DocType
combinatorial description,incidence simplicial,coq theorem prover,digital image analysis,abstract object,homology group,whole theory,computational algebraic topology,main theorem,coding theory,simplicial complex
Discrete mathematics,Betti number,Simplicial approximation theorem,Simplicial set,Simplicial homology,Simplicial complex,n-skeleton,Combinatorial topology,Mathematics,Abstract simplicial complex
Conference
Volume
ISSN
Citations 
6824
0302-9743
4
PageRank 
References 
Authors
0.45
12
4
Name
Order
Citations
PageRank
Jónathan Heras19423.31
María Poza2202.29
Maxime Dénès3644.91
Laurence Rideau425316.08