Formalization of a Normalization Theorem in Simplicial Topology
- Lambán, L. 1
- Martín-Mateos, F.-J. 2
- Rubio, J. 1
- Ruiz-Reina, J.-L. 2
-
1
Universidad de La Rioja
info
-
2
Universidad de Sevilla
info
ISSN: 1012-2443
Datum der Publikation: 2012
Ausgabe: 64
Nummer: 1
Seiten: 1-37
Art: Artikel
Andere Publikationen in: Annals of Mathematics and Artificial Intelligence
Projekte im Zusammenhang
2009/00207/001
2010/00182/001
Zusammenfassung
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.