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

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Aransay Azofra, Jesús María
Otros Autores:	Rubio García, Julio (Universidad de La Rioja)
Formato:	text (thesis)
Lenguaje:	spa
Publicado:	Universidad de La Rioja (España) 2006
Materias:	software verification homological algebra mechanized reasoning program extraction computer science
Acceso en línea:	https://dialnet.unirioja.es/servlet/oaites?codigo=403
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

id	oai-TES0000000132
record_format	dspace
institution	DialNet
collection	DialNet
language	spa
topic	software verification homological algebra mechanized reasoning program extraction computer science
spellingShingle	software verification homological algebra mechanized reasoning program extraction computer science Aransay Azofra, Jesús María Razonamiento mecanizado en álgebra homológica
description	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.
author2	Rubio García, Julio (Universidad de La Rioja)
author_facet	Rubio García, Julio (Universidad de La Rioja) Aransay Azofra, Jesús María
format	text (thesis)
author	Aransay Azofra, Jesús María
author_sort	Aransay Azofra, Jesús María
title	Razonamiento mecanizado en álgebra homológica
title_short	Razonamiento mecanizado en álgebra homológica
title_full	Razonamiento mecanizado en álgebra homológica
title_fullStr	Razonamiento mecanizado en álgebra homológica
title_full_unstemmed	Razonamiento mecanizado en álgebra homológica
title_sort	razonamiento mecanizado en álgebra homológica
publisher	Universidad de La Rioja (España)
publishDate	2006
url	https://dialnet.unirioja.es/servlet/oaites?codigo=403
work_keys_str_mv	AT aransayazofrajesusmaria razonamientomecanizadoenalgebrahomologica
_version_	1718346564250894336
spelling	oai-TES00000001322016-04-13Razonamiento mecanizado en álgebra homológicaAransay Azofra, Jesús Maríasoftware verificationhomological algebramechanized reasoningprogram extractioncomputer scienceWe 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.En la tesis se aborda el problema de obtener una versión certificada de un resultado fundamental en Álgebra Homológica, conocido como "Lema de Perturbación Básico". Dicho resultado es una pieza central del sistema "Kenzo", software dedicado al cálculo simbólico en Álgebra Homológica. Para tal fin, se utiliza el asistente de demostración "Isabelle". Las principales motivaciones de nuestro trabajo consisten en aumentar nuestro conocimiento sobre la naturaleza algorítmica de dicho resultado matemático, así como evaluar las distintas posibilidades que ofrece Isabelle para demostrar teoremas en Álgebra Homológica. El contenido de la tesis está dividido en cinco capítulos. En el primero se realiza una breve introducción a las herramientas de trabajo utilizadas. En particular, se presentan definiciones de estructuras algebraicas y resultados previos necesarios para enunciar el Lema de Perturbación; también se aporta información relevante para nuestro trabajo sobre la codificación de estructuras algebraicas en Kenzo e Isabelle. En el segundo capítulo se enuncia el Lema de Perturbación Básico y se da una demostración formal del mismo, basada en una demostración de F. Sergeraert. El tercer capítulo contiene resultados que tratan de la modelización, especificación y verificación de enunciados matemáticos en el demostrador de teoremas Isabelle. Más concretamente, cuatro representaciones distintas de los objetos matemáticos necesarios en las demostraciones son presentadas y analizadas desde distintos puntos de vista, que abarcan desde la especificación formal hasta la automatización de resultados. Una de estas representaciones, basada en el sistema modular de Isabelle, es escogida por su expresividad, grado de automatización, legibilidad en los enunciados y facilidad de extensión a nuevos problemas. Además, la adecuación de esta representación es mostrada por medio de su aplicación a diversos ejemplos. En el cuarto capítulo se hace una propuesta de extracción de programas certificados usando Isabelle. El interés de esta propuesta es doble: en primer lugar, su originalidad, ya que evita restringir las demostraciones matemáticas a lógicas constructivas. En segundo lugar, la aplicabilidad al tipo de enunciados que hemos abordado, que la hace especialmente atractiva para los algoritmos y enunciados en los que se basa Kenzo. En el quinto capítulo se presentan las conclusiones y las líneas de trabajo futuro. Nota: la memoria está redactada en inglés. También contiene un resumen en castellano al final de la misma.Universidad de La Rioja (España)Rubio García, Julio (Universidad de La Rioja)2006text (thesis)application/pdfhttps://dialnet.unirioja.es/servlet/oaites?codigo=403spaLICENCIA 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

Razonamiento mecanizado en álgebra homológica

Ejemplares similares