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!
|
| id |
oai-TES0000002603 |
|---|---|
| record_format |
dspace |
| institution |
DialNet |
| collection |
DialNet |
| language |
eng |
| topic |
Topología algebráica cálculo simbólico demostradores automatizados Algebraic topology Computer Algebra systems Theorem Provers |
| spellingShingle |
Topología algebráica cálculo simbólico demostradores automatizados Algebraic topology Computer Algebra systems Theorem Provers Heras Vicente, Jónathan Gestión mecanizada del conocimiento matemático en topología algebraica |
| description |
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. |
| author2 |
Pascual Martínez-Losa, María Vico (Universidad de La Rioja) |
| author_facet |
Pascual Martínez-Losa, María Vico (Universidad de La Rioja) Heras Vicente, Jónathan |
| format |
text (thesis) |
| author |
Heras Vicente, Jónathan |
| author_sort |
Heras Vicente, Jónathan |
| title |
Gestión mecanizada del conocimiento matemático en topología algebraica |
| title_short |
Gestión mecanizada del conocimiento matemático en topología algebraica |
| title_full |
Gestión mecanizada del conocimiento matemático en topología algebraica |
| title_fullStr |
Gestión mecanizada del conocimiento matemático en topología algebraica |
| title_full_unstemmed |
Gestión mecanizada del conocimiento matemático en topología algebraica |
| title_sort |
gestión mecanizada del conocimiento matemático en topología algebraica |
| publisher |
Universidad de La Rioja (España) |
| publishDate |
2011 |
| url |
https://dialnet.unirioja.es/servlet/oaites?codigo=22488 |
| work_keys_str_mv |
AT herasvicentejonathan gestionmecanizadadelconocimientomatematicoentopologiaalgebraica |
| _version_ |
1718346596037427200 |
| spelling |
oai-TES00000026032019-05-25Gestión mecanizada del conocimiento matemático en topología algebraicaHeras Vicente, JónathanTopología algebráicacálculo simbólicodemostradores automatizadosAlgebraic topologyComputer Algebra systemsTheorem ProversThe 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.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.Universidad de La Rioja (España)Pascual Martínez-Losa, María Vico (Universidad de La Rioja)Rubio García, Julio (Universidad de La Rioja)2011text (thesis)application/pdfhttps://dialnet.unirioja.es/servlet/oaites?codigo=22488engLICENCIA 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 |