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 246 articles , 3 standard articles )

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

1 2 3 ... 11 12 13 next

  1. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  2. Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
  3. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  4. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  5. Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
  6. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  7. Coghetto, Roland; Grabowski, Adam: Tarski geometry axioms. II (2016)
  8. Jan Jakubuv, Josef Urban: BliStrTune: Hierarchical Invention of Theorem Proving Strategies (2016) arXiv
  9. Korniłowicz, Artur: Enhancement of Mizar texts with transitivity property of predicates (2016)
  10. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  11. 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)
  12. Naumowicz, Adam; Piliszek, Radosław: Accessing the Mizar library with a weakly strict Mizar parser (2016)
  13. Rabe, Florian: The future of logic: foundation-independence (2016)
  14. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: A user-friendly library of real analysis for Coq (2015)
  15. Coghetto, Roland: Summable family in a commutative group (2015)
  16. Coghetto, Roland: Groups -- additive notation. (2015)
  17. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  18. Giero, Mariusz: Propositional linear temporal logic with initial validity semantics (2015)
  19. Grabowski, Adam: Two axiomatizations of Nelson algebras. (2015)
  20. Grabowski, Adam: Mechanizing complemented lattices within Mizar type system (2015)

1 2 3 ... 11 12 13 next