Resumen de Gestión mecanizada del conocimiento matemático en topología algebraica
- español
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.
- English
The work presented in this thesis tries to particularize Mathematical Knowledge Management to Algebraic Topology.
Mathematical Knowledge Management is a branch of Computer Science whose main goal consists in developing integral assistants for Mathematics including computation, deduction and powerful user interfaces able to make the daily work of mathematical researchers easier. Our application context is Algebraic Topology using the Kenzo system, a Common Lisp program devoted to Algebraic Topology developed by Francis Sergeraert, as an instrumental tool.
We can split the work presented in this thesis into three main parts which coincide with the main goals of Mathematical Knowledge Management.
Our first task has consisted in developing a system called fKenzo, an acronym of friendly Kenzo. This system not only provides a friendly graphical user interface to interact with the Kenzo system but also guides the interaction of the user with the. Moreover, fKenzo allows one to integrate other symbolic computation systems (such as GAP) and theorem prover tools (for instance, ACL2) by means of a plugin system.
The second part of the thesis is focussed on increasing the computational capabilities of the Kenzo system. Three new Kenzo modules have been developed which in turn extend the fKenzo system. The first one allows us to study the pushout of simplicial sets, an important construction in Algebraic Topology. The second one implements the simplicial complex notion (a generalization of the graph notion to higher dimensions). The last module allows us to analyse properties of 2D and 3D images by means of the Kenzo system thanks to the computation of the homology groups associated with the image.
Finally, since the Kenzo system has obtained some results not confirmed nor refuted by any other means, we are interested in increasing the reliability of the Kenzo system by means of Theorem Proving tools. Namely, in our work we have used the ACL2 Theorem Prover. ACL2 allows us to prove properties of programs implemented in Common Lisp, as in the Kenzo case. Then, in our work we have focussed on the certification of the correctness of some important fragments of the Kenzo system.
