Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
- 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: 0302-9743
Datum der Publikation: 2011
Ausgabe: 6898 LNCS
Seiten: 200-215
Art: Artikel
beta Ver similares en nube de resultadosAndere Publikationen in: Lecture Notes in Computer Science
Projekte im Zusammenhang
Zusammenfassung
In this paper we present a complete formalization, using the ACL2 theorem prover, 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. The interest of this work stems from three sources. First, the normalization theorem is the basis for some design decisions in the Kenzo computer algebra system, a program for computing in Algebraic Topology. Second, our proof of the theorem is new and shows the correctness of some formulas found experimentally, giving explicit expressions for the above-mentioned homotopy equivalence. And third, it demonstrates that the ACL2 theorem prover can be effectively used to formalize mathematics, even in areas where higher-order tools could be thought to be more appropriate. © 2011 Springer-Verlag.