Verifying the bridge between simplicial topology and algebra: The Eilenberg-Zilber algorithm

  1. Lambán, L. 1
  2. Rubio, J. 1
  3. Martín-Mateos, F.J. 2
  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

Revue:
Logic Journal of the IGPL

ISSN: 1367-0751

Année de publication: 2014

Volumen: 22

Número: 1

Pages: 39-65

Type: Article

DOI: 10.1093/JIGPAL/JZT034 SCOPUS: 2-s2.0-84892993588 WoS: WOS:000330845300003 GOOGLE SCHOLAR

D'autres publications dans: Logic Journal of the IGPL

Projets liés

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

2009/00207/001

Résumé

The Eilenberg-Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted to computing in Algebraic Topology. In this article we report on a complete formal proof of the underlying Eilenberg-Zilber theorem, using the ACL2 theorem prover. As our formalization is executable, we are able to compare the results of the certified programme with those of Kenzo on some universal examples. Since the results coincide, the reliability of Kenzo is reinforced. This is a new step in our long-term project towards certified programming for Algebraic Topology. © The Author 2013. Published by Oxford University Press. All rights reserved.