The Mizar Mathematical Library in OMDoc: translation and applications
From MaRDI portal
Publication:1945907
DOI10.1007/s10817-012-9271-4zbMath1260.68375OpenAlexW2087589117WikidataQ57389354 ScholiaQ57389354MaRDI QIDQ1945907
Mihnea Iancu, Josef Urban, Michael Kohlhase, Florian Rabe
Publication date: 17 April 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-012-9271-4
Related Items
A new export of the Mizar mathematical library ⋮ Four decades of {\textsc{Mizar}}. Foreword ⋮ Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization ⋮ Math Literate Knowledge Management via Induced Material ⋮ Mizar: State-of-the-art and Beyond ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ A scalable module system ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Unnamed Item ⋮ Flexary connectives in Mizar ⋮ Mathematical knowledge representation: semantic models and formalisms ⋮ Experiences from exporting major proof assistant libraries ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Towards Knowledge Management for HOL Light ⋮ System Description: MathHub.info ⋮ The future of logic: foundation-independence
Uses Software
Cites Work
- Unnamed Item
- A scalable module system
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- MPTP 0.2: Design, implementation, and initial experiments
- Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5--10, 2010. Proceedings
- On equivalents of well-foundedness. An experiment in MIZAR
- Extending MKM Formats at the Statement Level
- MathWebSearch 0.5: Scaling an Open Formula Search Engine
- Formalising foundations of mathematics
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
- Towards MKM in the Large: Modular Representation and Scalable Software Architecture
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
- A framework for defining logics
- On the Structure of Mizar Types
- Project Abstract: Logic Atlas and Integrator (LATIN)
- A Search Engine for Mathematical Formulae
- Information Retrieval and Rendering with MML Query
- Mathematical Knowledge Management
This page was built for publication: The Mizar Mathematical Library in OMDoc: translation and applications
