Gestión mecanizada del conocimiento matemático en topología algebraica

Resumen

Esta tesis presenta una particularización de la Gestión del Conocimiento Matemático 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, sino que también guía al usuario en la interacción con el sistema. 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. El primero de los módulos permite estudiar el pushout de conjuntos simpliciales, una construcción en Topología Algebraica. El segundo implementa la noción de complejo simplicial. El último módulo permite estudiar propiedades de imágenes 2D y 3D gracias al cálculo de los grupos de homología asociados con las imágenes. 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, 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.