|
 |
- Download Chapter.
- View Chapter.
- Summary.
-
The last chapter of the memoir is devoted to prove the correctness of some programs implemented in the
Kenzo system by means of ACL2. In the first part of this chapter, a set of ACL2 tools
which will be fundamental onwards are presented. The second part is focussed on proving
the correctness of the constant Kenzo simplicial set constructors. Subsequently, an
infrastructure for modeling mathematical structures in ACL2 is introduced. Eventually,
a methodology to verify the correctness of the construction of Kenzo spaces from other
ones applying topological constructors is presented in the last section of this chapter.
- Related Papers (preprints):
- ACL2 files:
|
|
|
|
|
