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

DOI10.1007/978-3-642-22673-1_19zbMATH Open1335.68255arXiv1107.4721OpenAlexW1595902028MaRDI QIDQ5200124FDOQ5200124

Authors: Jesse Alama 

Publication date: 29 July 2011

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Subsystems of second order arithmetic
• Premise selection for mathematics by corpus analysis and kernel methods
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Title not available (Why is that?)

Cited In (11)

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

Uses Software

• Mizar
• MML

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)