Razonamiento mecanizado en álgebra homológica
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 u...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | text (thesis) |
| Lenguaje: | spa |
| Publicado: |
Universidad de La Rioja (España)
2006
|
| Materias: | |
| Acceso en línea: | https://dialnet.unirioja.es/servlet/oaites?codigo=403 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| Sumario: | 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 Algebra, Symbolic Computation and Theorem Proving is given. More concretely, some definitions of algebraic structures and results needed to state the Perturbation Lemma are given; relevant information for our work about encoding algebraic structures in Kenzo and Isabelle is also presented. In the second chapter the Perturbation Lemma is stated, as well as a formal proof of it, based on a proof by F. Sergeraert. The third chapter contains results about modeling, formal specification and verification of mathematical results in the theorem prover Isabelle. Four different approaches to produce formal proofs of results in Homological Algebra are proposed and also analysed from different points of view, ranging from the formal specification of each of them, to the automation of proofs obtained. One of the approaches, based on the modular system of Isabelle, is chosen and shown to be appropriate due to its expresiveness, degree of automation, readability and extensibility to new problems, by means of illustrative examples. In the fourth chapter a technique for obtaining certified programs using Isabelle is introduced. The relevance of this technique is twofold: firstly, its originality, as far as it avoids restricting proofs to a constructive logic; secondly, the feasability of applying it to the kind of mathematical statements we deal with. The fifth chapter contains the conclusions and explores some possibilities for further work.
Note: the dissertation has been written in English; it also includes a resume in Spanish at the end. |
|---|