swMATH4655MaRDI QIDQ16825FDOQ16825
Author name not available (Why is that?)
Official website: http://wiki.mizar.org/twiki/bin/view/Mizar/MoMM
Cited In (57)
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- On duplication in mathematical repositories
- JEFL: joint embedding of formal proof libraries
- Enabling collaboration on semiformal mathematical knowledge by semantic web integration
- Presenting and explaining Mizar
- Lemma Mining over HOL Light
- Aligning concepts across proof assistant libraries
- Methods to access and retrieve mathematical content in ActiveMath
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Matching concepts across HOL libraries
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- A query language for formal mathematical libraries
- Information Retrieval and Rendering with MML Query
- The Mizar Mathematical Library in OMDoc: translation and applications
- Crystal: Integrating structured queries into a tactic language
- The role of the Mizar mathematical library for interactive proof development in Mizar
- MizarMode
- MPTP 0.2
- foaf
- Mizar
- GtkMathView
- jsMath
- MML
- QMT
- MaLeCoP
- NNexus
- TNTBase
- Polar
- STEX+
- Formulator MathML
- PRocH
- MaLARea
- BliStr
- A learning-based fact selector for Isabelle/HOL
- Dependencies in formal mathematics: applications and extraction for Coq and Mizar
- miz3
- SRASS
- Logic2CNF
- Jinja not Java
- Automated reasoning service for HOL Light
- Regular_Algebras
- Lemmatization for stronger reasoning in large theories
- Custom automations in Mizar
- MPTP-motivation, implementation, first experiments
- RapidXml
- HOL(y)Hammer: online ATP service for HOL Light
- mizar-items
- Learning-assisted theorem proving with millions of lemmas
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Semantics of Mizar as an Isabelle object logic
- Integrating searching and authoring in Mizar
- MaLeCoP. Machine learning connection prover
- Mizar: state-of-the-art and beyond
- Hammering towards QED
This page was built for software: MoMM
