Verifying an algorithm computing Discrete Vector Fields for digital imaging
Artificial Intelligence
2012-07-16 v1 Logic in Computer Science
Mathematical Software
Algebraic Topology
Abstract
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.
Keywords
Cite
@article{arxiv.1207.3315,
title = {Verifying an algorithm computing Discrete Vector Fields for digital imaging},
author = {Jónathan Heras and María Poza and Julio Rubio},
journal= {arXiv preprint arXiv:1207.3315},
year = {2012}
}
Comments
Published in the Calculemus track of the CICM 2012 congress