Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar

TL;DR

This paper presents two methods for extracting detailed formal dependencies from Coq and Mizar systems, applied to large mathematical libraries, with various applications and a discussion on dependency types and extraction methods.

Contribution

It introduces and compares two dependency extraction methods for Coq and Mizar, tailored for large repositories, and explores their applications and dependency types.

Findings

Effective dependency extraction from large repositories

Comparison of two extraction methods

Discussion on dependency types and suitability

Abstract

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.