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 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.

Grantor dc:publisher

Universidad de La Rioja (España)

Year dc:date

2011

Author dc:creator

• Heras Vicente, Jónathan

Contributors dc:contributor

• Pascual Martínez-Losa, María Vico (Universidad de La Rioja)
• Rubio García, Julio (Universidad de La Rioja)

• Topología algebráica
• cálculo simbólico
• demostradores automatizados
• Algebraic topology
• Computer Algebra systems
• Theorem Provers

Statement dc:rights

• LICENCIA DE USO: Los documentos a texto completo incluidos en Dialnet son de acceso libre y propiedad de sus autores y/o editores. Por tanto, cualquier acto de reproducción, distribución, comunicación pública y/o transformación total o parcial requiere el consentimiento expreso y escrito de aquéllos. Cualquier enlace al texto completo de estos documentos deberá hacerse a través de la URL oficial de éstos en Dialnet. Más información: https://dialnet.unirioja.es/info/derechosOAI | INTELLECTUAL PROPERTY RIGHTS STATEMENT: Full text documents hosted by Dialnet are protected by copyright and/or related rights. This digital object is accessible without charge, but its use is subject to the licensing conditions set by its authors or editors. Unless expressly stated otherwise in the licensing conditions, you are free to linking, browsing, printing and making a copy for your own personal purposes. All other acts of reproduction and communication to the public are subject to the licensing conditions expressed by editors and authors and require consent from them. Any link to this document should be made using its official URL in Dialnet. More info: https://dialnet.unirioja.es/info/derechosOAI

Language dc:language

eng

Repository record dc:identifier

https://dialnet.unirioja.es/servlet/oaites?codigo=22488

OAI identifier oai:identifier

oai:dialnet.unirioja.es:TES0000002603