fKenzo
fKenzo is an integral assistant for research in (a subset of) Algebraic Topology. The "integral" adjective means that this assistant not only provides a graphical interface for using a computational kernel (Kenzo), but also guides the user in his interaction with the system, and as far as possible, produces certificates about the correctness of the computations per- formed.
Algebraic Topology
Algebraic Topology consists in trying to use as much as possible "algebraic" methods to attack topological problems; in the simplest cases, it consists in associating to topological spaces some algebraic invariants which describe their essential properties. For instance, one can define some special groups associated with a topological space, in a way that respects the relation of homeomorphism of spaces. This allows one to study some interesting properties about topological spaces by means of statements about groups, which are often easier to prove. More generally, ther exist several functors which assign to some topological spaces some algebraic objects. Very frequently, if this functor works on a topological space of "finite type", then the result is also an algebraic object of finite type. But in general there do not exist algorithms capable of comptuing these algebraic objects of finite type according to the different functors of Algebraic Topology.
Kenzo
Kenzo is a 16000 lines program written in Common Lisp, which is devoted to Symbolic Computation in Algebraic Topology. It was developed by Francis Sergeraert and some coworkers. It works with rich and complex algebraic structures and has obtained some results which had never been determined before.
Motivation
Few Algebraic Topology students and researchers knows the language Common Lisp, for this we have detected the usability and the accesibility of Kenzo as two weak points. Our challenge is now to increase the number of users and to improve the usability of Kenzo. Instead of designing simply a friendly front-end, we have undertaken the task of devising a mediated access to the system, constraining its functionality, but providing guidance to the user in his navigation on the system. This objective is reached by constructing an intermediary layer, allowing us an intelligent access to some features of the system. This intermediary layer is supported by XML technology and interplays between a graphical user interface and the pure Common Lisp Kenzo system.