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

Zeitschrift:
Logic Journal of the IGPL

ISSN: 1367-0751

Datum der Publikation: 2014

Ausgabe: 22

Nummer: 1

Seiten: 39-65

Art: Artikel

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

Andere Publikationen in: Logic Journal of the IGPL

Projekte im Zusammenhang

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

2009/00207/001

Zusammenfassung

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.