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

Libro:
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

Editorial: SPRINGER-VERLAG

ISBN: 978-3-642-22673-1

Año de publicación: 2011

Volumen: 6824 LNAI

Páginas: 30-44

Tipo: Capítulo de Libro

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

Proyectos relacionados

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

2009/00207/001

Resumen

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.