swMATH6970MaRDI QIDQ19033FDOQ19033
Author name not available (Why is that?)
Official website: http://mizar.org/library/
Cited In (63)
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- User interaction with the Matita proof assistant
- Presenting and explaining Mizar
- Searching mathematics on the web: state of the art and future developments
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
- A Brief Overview of Mizar
- MPTP 0.1 -- system description
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mining the Archive of Formal Proofs
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- Readable formalization of Euler's partition theorem in Mizar
- Information Retrieval and Rendering with MML Query
- Machine learning guidance for connection tableaux
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- Crystal: Integrating structured queries into a tactic language
- MizarMode
- MPTP 0.2
- MoMM
- Mizar
- LPL software
- Clide
- MathJax
- Tipi
- EgoMath
- Lingva
- SInE
- MizAR 40 for Mizar 40
- System description: E.T. 0.1
- Flexary connectives in Mizar
- Evaluation of automated theorem proving on the Mizar mathematical library
- Sine qua non for large theory reasoning
- Licensing the Mizar Mathematical Library (MML)
- Automated and human proofs in general mathematics: an initial comparison
- Overview and evaluation of premise selection techniques for large theory mathematics
- Dependencies in formal mathematics: applications and extraction for Coq and Mizar
- miz3
- Mathfind
- MMode
- Cauchy
- Logic2CNF
- TGView3D
- Whelp
- WebMIaS
- ATP and presentation service for Mizar formalizations
- Custom automations in Mizar
- mizar-items
- Basic first-order model theory in Mizar
- Types for Proofs and Programs
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- Eliciting implicit assumptions of Mizar proofs by property omission
- Premise selection for mathematics by corpus analysis and kernel methods
- Cauchy mean theorem
- About quotient orders and ordering sequences
- Semantics of Mizar as an Isabelle object logic
- Mathematical knowledge management in MIZAR
- Integrating searching and authoring in Mizar
- MaLeCoP. Machine learning connection prover
- Mizar: state-of-the-art and beyond
- Mathematical Knowledge Management
This page was built for software: MML
