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

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

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)

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

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

Mathematics Subject Classification ID

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

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
• Title not available (Why is that?)
• Mizar: state-of-the-art and beyond
• Tools for MML environment analysis
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)

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)