1. Razonamiento mecanizado en álgebra homológica - Aransay Azofra, Jesús María
We face the problem of obtaining a certified version of a crucial algorithm in the field of 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 main motivations are to increase the knowledge in the algorithmic nature of this mathematical result, as well as to evaluate different possibilities offered by Isabelle in order to prove theorems in Homological Algebra. The memoir is divided into five chapters. In the first one, an introduction to some tools in Homological...
(application/pdf) - 25-abr-2008

2. Razonamiento mecanizado en álgebra homológica - Aransay Azofra, Jesús María
We face the problem of obtaining a certified version of a crucial algorithm in the field of 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 main motivations are to increase the knowledge in the algorithmic nature of this mathematical result, as well as to evaluate different possibilities offered by Isabelle in order to prove theorems in Homological Algebra. The memoir is divided into five chapters. In the first one, an introduction to some tools in Homological...
(application/pdf) - 25-abr-2008