作者: 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