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

DOI10.1007/978-3-642-31374-5_1zbMath1335.68221arXiv1109.3687OpenAlexW3103563805MaRDI QIDQ2907308

Lionel Elie Mamane, Jesse Alama, 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)

Related Items

Mizar: State-of-the-art and Beyond, Tools for MML Environment Analysis, The role of the Mizar mathematical library for interactive proof development in Mizar, An integrated web platform for the Mizar Mathematical Library, Large Formal Wikis: Issues and Solutions, mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library, CoqPIE: An IDE Aimed at Improving Proof Development Productivity, Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

• Coq
• MoMM
• Mizar
• MML