Dependencies in formal mathematics: applications and extraction for Coq and Mizar

DOI10.1007/978-3-642-31374-5_1MaRDI QIDQ2907308zbMATH OpenOpenAlexFDO

Authors Jesse Alama, Lionel Elie Mamane, Josef Urban

Publication date 7 September 2012

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

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)

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.

Recommendations

• mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
• Proof mining with dependent types
• scientific article; zbMATH DE number 1951627
• scientific article; zbMATH DE number 1951637
• Mathematical Knowledge Management

Cited in

(12)

• An integrated web platform for the Mizar Mathematical Library
• Extracting Higher-Order Goals from the Mizar Mathematical Library
• 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
• Proof mining with dependent types
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Large formal wikis: issues and solutions
• Premise selection for mathematics by corpus analysis and kernel methods
• scientific article; zbMATH DE number 1951627 (Why is no real title available?)
• Mizar: state-of-the-art and beyond
• Tools for MML environment analysis
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)

Describes a project that uses

Uses Software

• MML
• Mizar
• MoMM
• Coq

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)