Scifaro

中文

形式数学中的依赖关系：在 Coq 和 Mizar 中的应用与提取

数字图书馆 2015-03-19 v2 计算机科学中的逻辑逻辑

作者: Jesse Alama , Lionel Mamane , Josef Urban

在 arXiv 上查看 ↗ PDF ↗

摘要

本文提出并比较了两种从 Coq 和 Mizar 系统中提取详细形式依赖关系的方法。这些方法被用于从两个大型数学库中提取依赖关系：奈梅亨 Coq 仓库和 Mizar 数学库。文中描述并提出了详细依赖分析的若干应用。受不同应用的驱动，我们讨论了所关注的各类依赖关系，以及各种依赖提取方法的适用性。

关键词

形式依赖 Coq Mizar 依赖提取数学仓库形式数学

引用

@article{arxiv.1109.3687,
  title  = {Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar},
  author = {Jesse Alama and Lionel Mamane and Josef Urban},
  journal= {arXiv preprint arXiv:1109.3687},
  year   = {2015}
}