The Mizar Mathematical Library in OMDoc: translation and applications
From MaRDI portal
(Redirected from Publication:1945907)
Recommendations
Cites work
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- A Search Engine for Mathematical Formulae
- A Wiki for Mizar: motivation, considerations, and initial prototype
- A framework for defining logics
- A scalable module system
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- Extending MKM formats at the statement level
- Formalising foundations of mathematics
- Information Retrieval and Rendering with MML Query
- 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
- MPTP 0.2: Design, implementation, and initial experiments
- MathWebSearch 0.5: Scaling an Open Formula Search Engine
- Mathematical Knowledge Management
- On equivalents of well-foundedness. An experiment in MIZAR
- On the Structure of Mizar Types
- Project abstract: logic atlas and integrator (LATIN)
- Towards MKM in the large: modular representation and scalable software architecture
Cited in
(28)- Mathematical knowledge representation: semantic models and formalisms
- The future of logic: foundation-independence
- A scalable module system
- Math Literate Knowledge Management via Induced Material
- Towards Knowledge Management for HOL Light
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
- scientific article; zbMATH DE number 1951640 (Why is no real title available?)
- A new export of the Mizar mathematical library
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Information Retrieval and Rendering with MML Query
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- scientific article; zbMATH DE number 7756106 (Why is no real title available?)
- The role of the Mizar mathematical library for interactive proof development in Mizar
- scientific article; zbMATH DE number 2079831 (Why is no real title available?)
- Flexary connectives in Mizar
- Four decades of \textsc{Mizar}. Foreword
- Licensing the Mizar Mathematical Library (MML)
- 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
- Making PVS accessible to generic services by interpretation in a universal format
- scientific article; zbMATH DE number 2078371 (Why is no real title available?)
- Semantics of Mizar as an Isabelle object logic
- Mizar: state-of-the-art and beyond
- System description: MathHub.info
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)
