Incidence Simplicial Matrices Formalized in Coq/SSReflect

  1. Heras, J. 1
  2. Poza, M. 1
  3. Dénès, Maxime. 2
  4. Rideau, L. 2
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 Research Centre Inria Sophia Antipolis - Méditerranée
    info

    Research Centre Inria Sophia Antipolis - Méditerranée

    Valbonne, Francia

    ROR https://ror.org/01nzkaw91

Liburua:
Lectures Notes in Computer Science: Intelligent Computer Mathematics 18th Symposium, Calculemus 2011, 10th International Conference, MKM 2011, Held as Part of CICM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings

Argitaletxea: SPRINGER-VERLAG

ISBN: 978-3-642-22673-1

Argitalpen urtea: 2011

Alea: 6824 LNAI

Orrialdeak: 30-44

Mota: Liburuko kapitulua

DOI: 10.1007/978-3-642-22673-1_3 SCOPUS: 2-s2.0-79961175000 WoS: WOS:000306294200003 GOOGLE SCHOLAR lock_openSarbide irekia editor

Lotura duten proiektuak

Gestión Mecanizada del Conocimiento Matemático. Aplicaciones en Topología Algebraica y en Lógica.

2009/00207/001

Laburpena

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. © 2011 Springer-Verlag.