|
 |
- Download Chapter.
- View Chapter.
- Summary.
-
This chapter is devoted to increase the functionality of Kenzo by means of ACL2 certified programs. In addition the new Kenzo programs
will be included in fKenzo. To be more concrete, three new Kenzo modules are presented. The first one
implements a basic notion in Algebraic Topology: simplicial complexes. This module about simplicial complexes is the foundation to develop a setting to analyze monochromatic digital images. A new module with the algorithms for the processing of monochromatic images has also been developed. Eventually, an algorithm
for computing the effective homology of the pushout of simplical sets is defined and implemented as a new Kenzo module.
This chapter is organized in three different parts. The firsr one is devoted to simplicial complexes, the second one to the analysis of
digital images and the last one to the contruction of the effective homology of the pushout of simplicial sets. The structure of all the
parts is similar and consists of a brief introduction, the implementation of the programs as new Kenzo modules, the integration of the
programs in the Kenzo framework, the extension of the graphical user interface of fKenzo to include the new functionality, and finally
the ACl2 verification of the programs.
- Related Papers (preprints):
- Kenzo files:
- ACL2 files:
|
|
|
|
|
