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.


References in zbMATH (referenced in 253 articles , 3 standard articles )

Showing results 1 to 20 of 253.
Sorted by year (citations)

1 2 3 ... 11 12 13 next

  1. Coghetto, Roland: Group of homography in real projective plane (2017)
  2. Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
  3. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  4. Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
  5. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  6. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  7. Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
  8. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  9. Coghetto, Roland; Grabowski, Adam: Tarski geometry axioms. II (2016)
  10. Jan Jakubuv, Josef Urban: BliStrTune: Hierarchical Invention of Theorem Proving Strategies (2016) arXiv
  11. Korniłowicz, Artur: Enhancement of Mizar texts with transitivity property of predicates (2016)
  12. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  13. Matsuzaki, Takuya; Iwane, Hidenao; Kobayashi, Munehiro; Zhan, Yiyang; Fukasaku, Ryoya; Kudo, Jumma; Anai, Hirokazu; Arai, Noriko H.: Race against the teens -- benchmarking mechanized math on pre-university problems (2016)
  14. Naumowicz, Adam; Piliszek, Radosław: Accessing the Mizar library with a weakly strict Mizar parser (2016)
  15. Rabe, Florian: The future of logic: foundation-independence (2016)
  16. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: a user-friendly library of real analysis for Coq (2015)
  17. Coghetto, Roland: Summable family in a commutative group (2015)
  18. Coghetto, Roland: Groups -- additive notation. (2015)
  19. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  20. Giero, Mariusz: Propositional linear temporal logic with initial validity semantics (2015)

1 2 3 ... 11 12 13 next