Ponencia
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
Autor/es | Lambán Pardo, Laureano
Martín Mateos, Francisco Jesús Rubio, Julio Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2011 |
Fecha de depósito | 2019-05-20 |
Publicado en |
|
ISBN/ISSN | 978-3-642-22862-9 0302-9743 |
Resumen | 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 ... 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. |
Identificador del proyecto | MTM2009-13842
243847 (ForMath) |
Cita | Lambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2011). Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. En ITP 2011: 2nd International Conference on Interactive Theorem Proving (200-215), Berg en Dal, The Netherlands: Springer. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Applying ACL2.pdf | 304.5Kb | [PDF] | Ver/ | |