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

作者: Jónathan Heras Vicente

DOI:

关键词:

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

参考文章(98)
Jacek Chrząszcz, Implementing modules in the Coq system theorem proving in higher order logics. pp. 270- 286 ,(2003) , 10.1007/10930755_18
James Clark, XSL Transformations (XSLT) Version 1.0 W3C Recommendation. ,(1999)
J. L. Ruiz-Reina, F. J. Mart ´ in-Mateos, M. J. Hidalgo, J. A. Alonso, A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. University of Texas. ,(2002)
Russell J. Bradford, An implementation of Telos in Common Lisp. Object Oriented Systems. ,vol. 3, pp. 31- 49 ,(1996)
Gunnar Carlsson, R. James Milgram, Stable Homotopy and Iterated Loop Spaces Handbook of Algebraic Topology. pp. 505- 583 ,(1995) , 10.1016/B978-044481779-2/50014-6
Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J. Strother Moore, Functional instantiation in first-order logic Artificial intelligence and mathematical theory of computation. pp. 7- 26 ,(1991) , 10.1016/B978-0-12-450010-5.50007-4
Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau, Incidence simplicial matrices formalized in Coq/SSReflect MKM'11 Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics. pp. 30- 44 ,(2011) , 10.1007/978-3-642-22673-1_3
David Orden, Francisco Santos, Asymptotically efficient triangulations of the d-cube Discrete and Computational Geometry. ,vol. 30, pp. 509- 528 ,(2003) , 10.1007/S00454-003-2845-5
Eduardo Saenz-de-Cabezon, Combinatorial Koszul Homology: Computations and Applications arXiv: Commutative Algebra. ,(2008)