Presentation
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
Author/s | Martín Mateos, Francisco Jesús
![]() ![]() ![]() ![]() ![]() ![]() ![]() Rubio, Julio Ruiz Reina, José Luis ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Department | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Publication Date | 2009 |
Deposit Date | 2019-05-03 |
Published in |
|
ISBN/ISSN | 978-3-642-02613-3 0302-9743 |
Abstract | Kenzo is a Computer Algebra system devoted to Algebraic
Topology, and written in the Common Lisp programming language. It is
a descendant of a previous system called EAT (for Effective Algebraic
Topology). Kenzo shows ... Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows a much better performance than EAT due, among other reasons, to a smart encoding of degeneracy lists as integers. In this paper, we give a complete automated proof of the correctness of this encoding used in Kenzo. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp. The most interesting idea, from a methodological point of view, is our use of EAT to build a model on which the verification is carried out. Thus, EAT, which is logically simpler but less efficient than Kenzo, acts as a mathematical model and then Kenzo is formally verified against it. |
Project ID. | MTM2006-06513
![]() |
Citation | Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2009). ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. En CICM 2009: International Conference on Intelligent Computer Mathematics (106-121), Grand Bend, Canada: Springer. |
Files | Size | Format | View | Description |
---|---|---|---|---|
ACL2 Verification of Simplicial ... | 292.5Kb | ![]() | View/ | |