A Certified Module to Study Digital Images with the Kenzo System
- Heras, J. 1
- Pascual, V. 1
- Rubio, J. 1
-
1
Universidad de La Rioja
info
Editorial: SPRINGER-VERLAG
ISBN: 978-3-642-27548-7
Any de publicació: 2012
Volum: 6927 LNCS
Número: 1
Pàgines: 113-120
Tipus: Capítol de llibre
Resum
Kenzo is a Computer Algebra system devoted to Algebraic Topology, written in the Common Lisp programming language. In this paper, programs which allow us to analyze monochromatic digital images with the Kenzo system are presented. Besides a complete automated proof of the correctness of our programs is provided. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp. © 2012 Springer-Verlag.