Mizar
The Mizar System is the only implementation of the Mizar Language. Originally, the Mizar system was implemented on an IBM-PC x86 compatibles under MS DOS. Now we distribute releases for MS Windows, Intel-based Linux, Solaris and FreeBSD, and also Darwin/Mac OS X and Linux on PowerPC. The whole Mizar system (including verifier) is coded in Pascal using the Free Pascal compiler.
Keywords for this software
References in zbMATH (referenced in 505 articles , 4 standard articles )
Showing results 41 to 60 of 505.
Sorted by year (citations)
- Koch, Sebastian: About graph complements (2020)
- Korniłowicz, Artur: Partial correctness of a Fibonacci algorithm (2020)
- Kulesza, Dominik; Grabowski, Adam: Formalization of quasilattices (2020)
- Li, Wenda; Paulson, Lawrence C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (2020)
- Naumowicz, Adam: Dataset description: formalization of elementary number theory in Mizar (2020)
- Naumowicz, Adam: Elementary number theory problems. I (2020)
- Pąk, Karol: Grothendieck universes (2020)
- Schwarzweller, Christoph: Field extensions and Kronecker’s construction (2020)
- Schwarzweller, Christoph: Renamings and a condition-free formalization of Kronecker’s construction (2020)
- Schwarzweller, Christoph: On the intersection of fields (F) with (F[X]) (2020)
- Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
- Urban, Josef; Jakubův, Jan: First neural conjecturing datasets and experiments (2020)
- van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y.: Maintaining a library of formal mathematics (2020)
- Wasaki, Katsumi: Stability of the 7-3 compressor circuit for Wallace tree. I (2020)
- Watase, Yasushige: Rings of fractions and localization (2020)
- Brown, Chad E.; Pąk, Karol: A tale of two set theories (2019)
- Chan, Hing-Lun; Norrish, Michael: Classification of finite fields with applications (2019)
- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- Coghetto, Roland: Cross-ratio in real vector space (2019)
- Coghetto, Roland; Grabowski, Adam: Tarski geometry axioms. IV: Right angle (2019)