This chapter is devoted to explain the integration of different tools, such as Computer Algebra systems and Theorem Provers, in
the Kenzo framework. From the Computer Algebra side, we have chosen GAP, a system well-known for its contributions, in particular,
in the area of Computational Group Theory. From the theorem proving side, we have integrated ACL2. It is worth noting that our final
aim has consisted not only in having several Computer Algebra systems and Theorem Prover tools, and use them individually by means
of a common GUI, but also in making them work in a coordinate and collaborative way to obtain new tools and results not reachable
if we use severally each system.
The chapter is split in two different parts. The former one is devoted to the integration of GAP, and the latter one to the
integration of ACL2. The structure of both parts is similar and consists of a brief introduction, the integration of the system in
the Kenzo framework, the extension of the graphical user interface of fKenzo to include the new
functionality, and finally the interoperability among systems to produce new tools.
We'll begin with a brief introduction to some fairly recent work of
Gunnar Carlsson, Herbert Edelsbrunner and others which uses the
efficient computation of low-dimensional homology
of spaces as an effective technique for investigating large data sets
arising in applied problems
from biology and physics. Their work is based on the notion of a
persistent homology module.
We'll then explain how the notion of persistent homology can also be
applied to group homology. It provides a strong group invariant and
we'll suggest that it might be of use in the coclass study of finite
p-groups. We'll also outline one approach to computing the persistent
homology of a finite p-group.
