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

Showing results 1 to 20 of 249.
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; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  3. Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
  4. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  5. Korniłowicz, Artur: Enhancement of Mizar texts with transitivity property of predicates (2016)
  6. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  7. 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)
  8. Naumowicz, Adam; Piliszek, Radosław: Accessing the Mizar library with a weakly strict Mizar parser (2016)
  9. Rabe, Florian: The future of logic: foundation-independence (2016)
  10. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: A user-friendly library of real analysis for Coq (2015)
  11. Coghetto, Roland: Summable family in a commutative group (2015)
  12. Coghetto, Roland: Groups -- additive notation. (2015)
  13. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  14. Giero, Mariusz: Propositional linear temporal logic with initial validity semantics (2015)
  15. Grabowski, Adam: Mechanizing complemented lattices within Mizar type system (2015)
  16. Grabowski, Adam: Two axiomatizations of Nelson algebras. (2015)
  17. Grabowski, Adam (ed.); Korniłowicz, Artur (ed.); Naumowicz, Adam (ed.): Four decades of Mizar. Foreword (2015)
  18. Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
  19. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  20. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)

1 2 3 ... 11 12 13 next