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 461 to 480 of 505.
Sorted by year (citations)
- Schwarzweller, Christoph: Designing mathematical libraries based on requirements for theorems (2003)
- Urban, Josef: MPTP 0.1 -- system description (2003)
- Urban, Josef: Translating Mizar for first order theorem provers (2003)
- Bancerek, Grzegorz; Rudnicki, Piotr: A compendium of continuous lattices in MIZAR (2002)
- Wenzel, Markus; Wiedijk, Freek: A comparison of Mizar and Isar (2002)
- Bancerek, Grzegorz: Development of the theory of continuous lattices in MIZAR (2001)
- Bauer, Gertrud; Wenzel, Markus: Calculational reasoning revisited. An Isabelle/Isar experience (2001)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Distributed assertion retrieval (2001)
- Boulton, Richard J. (ed.); Jackson, Paul B. (ed.): Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3--6, 2001. Proceedings (2001)
- Buchberger, Bruno (ed.); Caprotti, Olga (ed.): Mathematical knowledge management: MKM 2001. Electronic proceedings of the 1st international workshop, RISC, Schloß Hagenberg, Austria, September 24--26, 2001 (2001)
- Farmer, William M.: STMM: A set theory for mechanized mathematics (2001)
- Farmer, William M.; von Mohrenschildt, Martin: A formal framework for managing mathematics (2001)
- Grabowski, Adam: Robbins algebras vs. Boolean algebras (2001)
- Grąndzka, Ewa: Towards (\psi)-extension of Rota calculus in Mizar language. (2001)
- Kerber, Manfred (ed.); Kohlhase, Michael (ed.): Symbolic computation and automated reasoning. The CALCULEMUS-2000 symposium. 8th symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, GB, August 6--7, 2000 (2001)
- Rudnicki, Piotr; Schwarzweller, Christoph; Trybulec, Andrzej: Defining power series and polynomials in Mizar (2001)
- Rudnicki, Piotr; Schwarzweller, Christoph; Trybulec, Andrzej: Commutative algebra in the Mizar system (2001)
- Rudnicki, Piotr; Trybulec, Andrzej: Mathematical knowledge management in MIZAR (2001)
- Schwarzweller, Christoph: Designing mathematical libraries based on minimal requirements for theorems (2001)
- Shimizu, Hidetaka; Nakamura, Yatsuka; Fujisawa, Yoshinori; Fuwa, Yasushi: Verification of logic circuits using Mizar and its application to an adder circuit on a radix-(2^k)SD number (2001)