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 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.

Grantor dc:publisher

Universidad de La Rioja (España)

Year dc:date

2006

Author dc:creator

• Aransay Azofra, Jesús María

Contributors dc:contributor

• Rubio García, Julio (Universidad de La Rioja)

• software verification
• homological algebra
• mechanized reasoning
• program extraction
• computer science

Statement dc:rights

• LICENCIA DE USO: Los documentos a texto completo incluidos en Dialnet son de acceso libre y propiedad de sus autores y/o editores. Por tanto, cualquier acto de reproducción, distribución, comunicación pública y/o transformación total o parcial requiere el consentimiento expreso y escrito de aquéllos. Cualquier enlace al texto completo de estos documentos deberá hacerse a través de la URL oficial de éstos en Dialnet. Más información: https://dialnet.unirioja.es/info/derechosOAI | INTELLECTUAL PROPERTY RIGHTS STATEMENT: Full text documents hosted by Dialnet are protected by copyright and/or related rights. This digital object is accessible without charge, but its use is subject to the licensing conditions set by its authors or editors. Unless expressly stated otherwise in the licensing conditions, you are free to linking, browsing, printing and making a copy for your own personal purposes. All other acts of reproduction and communication to the public are subject to the licensing conditions expressed by editors and authors and require consent from them. Any link to this document should be made using its official URL in Dialnet. More info: https://dialnet.unirioja.es/info/derechosOAI

Language dc:language

spa

Repository record dc:identifier

https://dialnet.unirioja.es/servlet/oaites?codigo=403

OAI identifier oai:identifier

oai:dialnet.unirioja.es:TES0000000132