形式数学中的应用：Coq和Mizar的应用和提取
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
摘要：
提出并比较了从Coq和Mizar系统中提取详细形式依赖的两种方法。这些方法用于从两个大型数学库中提取依赖关系：Nijmegen的Coq库和Mizar数学库。详细的依赖性分析的几个应用程序进行了描述和建议。基于不同的应用，我们讨论了我们感兴趣的各种依赖，以及各种依赖提取方法的适用性。
英文摘要：
Two methods for extracting detailed formal dependencies from the Coq and Mizar system are presented and compared. The methods are used for dependency extraction from two large mathematical repositories: the Coq Repository at Nijmegen and the Mizar Mathematical Library. Several applications of the detailed dependency analysis are described and proposed. Motivated by the different applications, we discuss the various kinds of dependencies that we are interested in,and the suitability of various dependency extraction methods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
