Tesis doctoral de Jesús María Aransay Azofra
En la tesis se aborda el problema de obtener una versión certificada de un algoritmo fundamental en topología algebraica, conocido como «lema básico de perturbación». Dicho resultado es una pieza central del sistema kenzo, software dedicado al cálculo simbólico en topología algebraica. Para tal fin, se utiliza el asistente de demostración isabelle. 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 este caso, se dan algunas definiciones y resultados en el área del álgebra homológica, así como informaciones relevantes sobre el sistema de cálculo simbólico kenzo y sobre el demostrador de teoremas 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 presenta la mayor parte de los resultados que se han obtenido de la investigación realizada. Dichos resultados van en la dirección de la modelización, especificación y verificación de enunciados matemáticos en el demostrador de teoremas isabelle. Más concretamente, se proponen y analizan desde distintos puntos de vista (que abarcan desde la especificación formal hasta la automatización de resultados), cuatro representaciones distintas de los objetos matemáticos necesarios en las demostraciones. Una de estas representaciones es escogida finalmente por satisfacer los requisitos demandados. En el cuarto capítulo se hace una una propuesta de extracción de programas certificados desde 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 se pretende abordar, que la hace especialmente atractiva para los programas y enunciados en los que se basa kenzo. En el quinto capítulo se enuncian las conclusi
Datos académicos de la tesis doctoral «Razonamiento mecanizado en álgebra homológica«
- Título de la tesis: Razonamiento mecanizado en álgebra homológica
- Autor: Jesús María Aransay Azofra
- Universidad: Rioja
- Fecha de lectura de la tesis: 04/04/2006
Dirección y tribunal
- Director de la tesis
- Julio Jesús Rubio García
- Tribunal
- Presidente del tribunal: eladio Domínguez murillo
- renaud Rioboo (vocal)
- Luis Español gonzález (vocal)
- francis Sergeraert (vocal)