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

DOI10.1007/978-3-642-31374-5_1zbMATH Open1335.68221arXiv1109.3687OpenAlexW3103563805MaRDI QIDQ2907308FDOQ2907308

Lionel Elie Mamane, Jesse Alama, Josef Urban

Publication date: 7 September 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1109.3687

Mathematics Subject Classification ID

Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Cited In (10)

• An integrated web platform for the Mizar Mathematical Library
• Extracting Higher-Order Goals from the Mizar Mathematical Library
• CoqPIE: An IDE Aimed at Improving Proof Development Productivity
• Large Formal Wikis: Issues and Solutions
• Mizar: State-of-the-art and Beyond
• Tools for MML Environment Analysis
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

• Coq
• MoMM
• Mizar
• MML

This page was built for publication: Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907308)