A Certified Module to Study Digital Images with the Kenzo System

  1. Heras, J. 1
  2. Pascual, V. 1
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Buch:
Lecture Notes in Computer Science, Computer Aided Systems Theory &- EUROCAST 2011

Verlag: SPRINGER-VERLAG

ISBN: 978-3-642-27548-7

Datum der Publikation: 2012

Ausgabe: 6927 LNCS

Nummer: 1

Seiten: 113-120

Art: Buch-Kapitel

DOI: 10.1007/978-3-642-27549-4_15 SCOPUS: 2-s2.0-84856863632 WoS: WOS:000314461400015 GOOGLE SCHOLAR lock_openOpen Access editor

Zusammenfassung

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.