验证一种用于数字成像的离散向量场计算算法
人工智能
2012-07-16 v1 计算机科学中的逻辑
数学软件
代数拓扑
摘要
本文利用 SSReflect 库，在 Coq 定理证明器中对一种构建容许离散向量场的算法进行了形式化。离散向量场是一种在数字图像的同调分析中备受欢迎的工具，因为它提供了一种减少信息量同时保留同调性质的过程。特别是，借助离散向量场，我们能够在 Coq 内部计算生物医学图像的同调性质，而这些否则是该系统无法企及的。
引用
@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}
}
备注
Published in the Calculemus track of the CICM 2012 congress