A mechanized proof of the Basic Perturbation Lemma
- Aransay, J. 1
- Ballarin, C. 2
- Rubio, J. 1
-
1
Universidad de La Rioja
info
-
2
University of Innsbruck
info
ISSN: 0168-7433
Argitalpen urtea: 2008
Alea: 40
Zenbakia: 4
Orrialdeak: 271-292
Mota: Artikulua
Beste argitalpen batzuk: Journal of Automated Reasoning
Lotura duten proiektuak
Laburpena
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.