Razonamiento mecanizado en álgebra homológica stars

Resumen

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.