Verifying an algorithm computing Discrete Vector Fields for digital imaging

  1. Heras, J. 1
  2. Poza, M. 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

Liburua:
Lecture Notes in Computer Science, Proceedings CICM 2012

ISBN: 978-3-642-35139-6

Argitalpen urtea: 2012

Alea: 7362 LNAI

Orrialdeak: 216-230

Mota: Liburuko kapitulua

DOI: 10.1007/978-3-642-31374-5_15 SCOPUS: 2-s2.0-84864947455 arXiv: 1207.3315 GOOGLE SCHOLAR lock_openSarbide irekia editor

Lotura duten proiektuak

Gestión Mecanizada del Conocimiento Matemático. Aplicaciones en Topología Algebraica y en Lógica.

2009/00207/001

Laburpena

In this paper, we present a formalization of an algorithm to construct admissible discrete vector fields in the Coq theorem prover taking advantage of the SSReflect library. Discrete vector fields are a tool which has been welcomed in the homological analysis of digital images since it provides a procedure to reduce the amount of information but preserving the homological properties. In particular, thanks to discrete vector fields, we are able to compute, inside Coq, homological properties of biomedical images which otherwise are out of the reach of this system. © 2012 Springer-Verlag.