Gestión mecanizada del conocimiento matemático en topología algebraica
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 powerfu...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | text (thesis) |
| Lenguaje: | eng |
| Publicado: |
Universidad de La Rioja (España)
2011
|
| Materias: | |
| Acceso en línea: | https://dialnet.unirioja.es/servlet/oaites?codigo=22488 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| Sumario: | 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. |
|---|