A mechanized proof of the Basic Perturbation Lemma

  1. Aransay, J. 1
  2. Ballarin, C. 2
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 University of Innsbruck
    info

    University of Innsbruck

    Innsbruck, Austria

    ROR https://ror.org/054pv6659

Revista:
Journal of Automated Reasoning

ISSN: 0168-7433

Año de publicación: 2008

Volumen: 40

Número: 4

Páginas: 271-292

Tipo: Artículo

DOI: 10.1007/S10817-007-9094-X SCOPUS: 2-s2.0-42649114070 WoS: WOS:000255114200002 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Journal of Automated Reasoning

Proyectos relacionados

Sistemas de cálculo simbólico: nuevos desarrollos en topología algebráica y fiabilidad

2006/00092/001

Resumen

We present a complete mechanized proof of the result in homological algebra known as basic perturbation lemma. The proof has been carried out in the proof assistant Isabelle, more concretely, in the implementation of higher-order logic (HOL) available in the system. We report on the difficulties found when dealing with abstract algebra in HOL, and also on the ongoing stages of our project to give a certified version of some of the algorithms present in the Kenzo symbolic computation system. © 2007 Springer Science+Business Media B.V.