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 Heras | 1 | 94 | 23.31 |
María Poza | 2 | 20 | 2.29 |
Maxime Dénès | 3 | 64 | 4.91 |
Laurence Rideau | 4 | 253 | 16.08 |