Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-31374-5_15 | CICM'12 Proceedings of the 11th international conference on Intelligent Computer Mathematics |
Keywords | DocType | Volume |
admissible discrete vector field,ssreflect library,coq theorem prover,digital image,homological analysis,biomedical image,homological property,digital imaging,algorithm computing,discrete vector field | Conference | abs/1207.3315 |
ISSN | Citations | PageRank |
Calculemus 2012, Lecture Notes in Computer Science, 7362, pages
215--229, 2012 | 5 | 0.76 |
References | Authors | |
14 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jónathan Heras | 1 | 94 | 23.31 |
| María Poza | 2 | 20 | 2.29 |
| J. Rubio | 3 | 202 | 31.12 |