The Mizar Mathematical Library in OMDoc: translation and applications
From MaRDI portal
Publication:1945907
DOI10.1007/S10817-012-9271-4zbMATH Open1260.68375OpenAlexW2087589117WikidataQ57389354 ScholiaQ57389354MaRDI QIDQ1945907FDOQ1945907
Authors: Mihnea Iancu, Michael Kohlhase, Florian Rabe, Josef Urban 
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
Recommendations
Cites Work
- MathWebSearch 0.5: Scaling an Open Formula Search Engine
- Title not available (Why is that?)
- A Search Engine for Mathematical Formulae
- MPTP 0.2: Design, implementation, and initial experiments
- Formalising foundations of mathematics
- A scalable module system
- A framework for defining logics
- Project abstract: logic atlas and integrator (LATIN)
- On equivalents of well-foundedness. An experiment in MIZAR
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- Information Retrieval and Rendering with MML Query
- Mathematical Knowledge Management
- Extending MKM formats at the statement level
- Towards MKM in the large: modular representation and scalable software architecture
- ATP-based cross-verification of Mizar proofs: method, systems, and first 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 the Structure of Mizar Types
- A Wiki for Mizar: motivation, considerations, and initial prototype
Cited In (28)
- Mathematical knowledge representation: semantic models and formalisms
- The future of logic: foundation-independence
- Math Literate Knowledge Management via Induced Material
- A scalable module system
- Towards Knowledge Management for HOL Light
- Title not available (Why is that?)
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- A new export of the Mizar mathematical library
- Information Retrieval and Rendering with MML Query
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- Title not available (Why is that?)
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Title not available (Why is that?)
- Flexary connectives in Mizar
- Licensing the Mizar Mathematical Library (MML)
- Four decades of \textsc{Mizar}. Foreword
- Isabelle import infrastructure for the Mizar Mathematical Library
- System description: XSL-based translator of Mizar to {\LaTeX}
- Translating the IMPS theory library to MMT/OMDoc
- Experiences from exporting major proof assistant libraries
- Title not available (Why is that?)
- Making PVS accessible to generic services by interpretation in a universal format
- Semantics of Mizar as an Isabelle object logic
- Mizar: state-of-the-art and beyond
- System description: MathHub.info
Uses Software
This page was built for publication: The Mizar Mathematical Library in OMDoc: translation and applications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1945907)
