Formalization of a Normalization Theorem in Simplicial Topology

  1. Lambán, L. 1
  2. Martín-Mateos, F.-J. 2
  3. Rubio, J. 1
  4. Ruiz-Reina, J.-L. 2
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 Universidad de Sevilla
    info

    Universidad de Sevilla

    Sevilla, España

    ROR https://ror.org/03yxnpp24

Revista:
Annals of Mathematics and Artificial Intelligence

ISSN: 1012-2443

Año de publicación: 2012

Volumen: 64

Número: 1

Páginas: 1-37

Tipo: Artículo

DOI: 10.1007/S10472-011-9274-6 SCOPUS: 2-s2.0-84855374495 WoS: WOS:000303801500001 GOOGLE SCHOLAR

Otras publicaciones en: Annals of Mathematics and Artificial Intelligence

Proyectos relacionados

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

2009/00207/001

Formalization of Mathematics (FORMATH)

2010/00182/001

Resumen

In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain complex of a simplicial set, and a smaller chain complex for the same simplicial set, called the normalized chain complex. Even if the Normalization Theorem is usually stated as a higher-order result (with a Category Theory flavor) we manage to give a first-order proof of it. To this aim it is instrumental the introduction of an algebraic data structure called simplicial polynomial. As a demonstration of the validity of our techniques we developed a formal proof in the ACL2 theorem prover. © 2012 Springer Science+Business Media B.V.