Tesis doctoral de Jónatan Heras Vicente
Esta tesis presenta una particularización de la gestión del conocimiento matemático (mathematical knowledge management) al caso de la topología algebraica. la gestión del conocimiento matemático es una rama de las ciencias de la computación cuyo principal objetivo consiste en desarrollar asistentes para las matemáticas que incorporen cálculo, deducción e interfaces de usuario potentes que puedan mejorar el trabajo cotidiano de los investigadores en matemáticas. Nuestra área de aplicación particular es la topología algebraica utilizando el sistema kenzo como herramienta fundamental. Kenzo es un programa common lisp para la topología algebraica que fue desarollado por francis sergeraert. podemos dividir en tres grandes bloques el trabajo presentado en la tesis que coinciden con los grandes objetivos de la gestión del conocimiento matemático. nuestra primera labor ha consistido en el desarrollo de un sistema llamado fkenzo, del inglés friendly kenzo. Dicho sistema no sólo proporciona una intefaz de usuario agradable y cómoda para utilizar el sistema kenzo (que es el núcleo de nuestra aplicación), sino que también guía al usuario en la interacción con el sistema (evitando de este modo errores). El sistema fkenzo permite también la integración de otros sistemas de cálculo simbólico (como gap) y demostradores de teoremas (por ejemplo, acl2) mediante un sistema de módulos. la segunda parte de la tesis se centra en incrementar las capacidades computacionales del sistema kenzo. Se han desarrollado tres nuevos módulos para kenzo que a su vez han sido también incluidos en el sistema fkenzo. El primero de los módulos permite estudiar el pushout de conjuntos simpliciales, una construcción relevante ya que aparece involucrada en una gran cantidad de los constructores habituales en topología algebraica. El segundo implementa la noción de complejo simplicial (una generalización de la noción de grafo a dimensiones superiores). El último módulo permite estudiar propiedades de imágenes 2d y 3d por medio del sistema kenzo gracias al cálculo de los grupos de homología asociados con la imagen. por último, debido a que el sistema kenzo ha obtenido resultados que no han sido ni confirmados ni refutados por ningún otro medio queremos incrementar la confianza en la fiabilidad del sistema kenzo mediante el uso de demostradores de teoremas. En concreto, en nuestro trabajo hemos utilizado el demostrador de teoremas acl2. Acl2 permite demostrar propiedades sobre sistemas implementados en el lenguaje common lisp, como es el caso de kenzo. En nuestro trabajo nos hemos centrado en la certificación de la corrección de algunos fragmentos importantes del sistema kenzo así como de los nuevos módulos desarrollados en la segunda parte de la tesis.
Datos académicos de la tesis doctoral «Gestión mecanizada del conocimiento matemático en topología algebraica«
- Título de la tesis: Gestión mecanizada del conocimiento matemático en topología algebraica
- Autor: Jónatan Heras Vicente
- Universidad: Rioja
- Fecha de lectura de la tesis: 31/05/2011
Dirección y tribunal
- Director de la tesis
- Julio Jesús Rubio García
- Tribunal
- Presidente del tribunal: eladio Domínguez murillo
- laurence Rideau (vocal)
- Francisco Jesús Martín mateos (vocal)
- francis Sergeraert (vocal)
