Mechanized Reasoning in Homological Algebra

  1. Aransay, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
AI Communications

ISSN: 0921-7126

Año de publicación: 2008

Volumen: 21

Número: 4

Páginas: 265-267

Tipo: Artículo

DOI: 10.3233/AIC-2008-0427 SCOPUS: 2-s2.0-58149504107 WoS: WOS:000262452100005 GOOGLE SCHOLAR

Otras publicaciones en: AI Communications

Resumen

In this work we face the problem of obtaining a certified version of a crucial algorithm in Homological Algebra, known as Perturbation Lemma. This lemma is intensively used in the software system Kenzo, devoted to symbolic computation in Homological Algebra. To this end we use the proof assistant Isabelle. Our motivations are to increase the knowledge in the algorithmic nature of this mathematical result and to test different possibilities offered by Isabelle to formally prove theorems in Homological Algebra. A detailed mathematical proof of the Perturbation Lemma, a methodology to obtain certified software in Homological Algebra, a suitable infrastructure to formalize the proof, a complete Isabelle formal proof, and a discussion on the constructiveness of the mathematical results introduced are presented. © 2008 - IOS Press and the authors. All rights reserved.