mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library

DOI10.1007/978-3-642-22673-1_19MaRDI QIDQ5200124zbMATH OpenOpenAlexFDO

Authors Jesse Alama

Publication date 29 July 2011

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

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

Mathematics Subject Classification ID

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

Abstract: The Mizar Mathematical Library (MML) is a rich database of formalized mathematical proofs (see http://mizar.org). Owing to its large size (it contains more than 1100 "articles" summing to nearly 2.5 million lines of text, expressing more than 50000 theorems and 10000 definitions using more than 7000 symbols), the nature of its contents (the MML is slanted toward pure mathematics), and its classical foundations (first-order logic, set theory, natural deduction), the MML is an especially attractive target for research on foundations of mathematics. We have implemented a system, mizar-items, on which a variety of such foundational experiements can be based. The heart of mizar-items is a method for decomposing the contents of the MML into fine-grained "items" (e.g., theorem, definition, notation, etc.) and computing dependency relations among these items. mizar-items also comes equipped with a website for exploring these dependencies and interacting with them.

Recommendations

• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Isabelle import infrastructure for the Mizar Mathematical Library
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Extracting Higher-Order Goals from the Mizar Mathematical Library
• Mathematical Knowledge Management
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• A new export of the Mizar mathematical library
• The Mizar Mathematical Library in OMDoc: translation and applications
• Mathematical Knowledge Management
• Mathematical Knowledge Management

Cites work

• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• scientific article; zbMATH DE number 3521895 (Why is no real title available?)
• Premise selection for mathematics by corpus analysis and kernel methods
• Subsystems of second order arithmetic

Cited in

(11)

• mizar-items
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Eliciting implicit assumptions of Mizar proofs by property omission
• Dataset description: formalization of elementary number theory in Mizar
• Accessing the Mizar library with a weakly strict Mizar parser
• Extracting Higher-Order Goals from the Mizar Mathematical Library
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Mizar: state-of-the-art and beyond
• Tools for MML environment analysis
• Licensing the Mizar Mathematical Library (MML)
• An integrated web platform for the Mizar Mathematical Library

Describes a project that uses

Uses Software

• MML
• Mizar

This page was built for publication: mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library

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