Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials

  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:
Lecture Notes in Computer Science

ISSN: 0302-9743

Any de publicació: 2011

Volum: 6898 LNCS

Pàgines: 200-215

Tipus: Article

DOI: 10.1007/978-3-642-22863-6_16 SCOPUS: 2-s2.0-80052162979 GOOGLE SCHOLAR lock_openAccés obert editor

Altres publicacions en: Lecture Notes in Computer Science

Projectes relacionats

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

2009/00207/001

Resum

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.