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 441 to 460 of 505.
Sorted by year (citations)
- Grabowski, Adam; Moschner, Markus: Managing heterogeneous theories within a mathematical knowledge repository (2004)
- Grabowski, Adam; Schwarzweller, Christoph: Rough concept analysis -- theory development in the Mizar system (2004)
- Jojgov, Gueorgui; Nederpelt, Rob: A path to faithful formalizations of mathematics (2004)
- Kamareddine, Fairouz; Nederpelt, Rob: A refinement of de Bruijn’s formal language of mathematics (2004)
- Kamareddine, F. (ed.): Proceedings of the mathematical knowledge management symposium, Edinburgh, UK November 25--29, 2003 (2004)
- Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: Theorem proving and proof verification in the system SAD (2004)
- Nakagawa, Koji; Nomura, Akihiro; Suzuki, Masakazu: Extraction of logical structure from articles in mathematics (2004)
- Naumowicz, Adam; Byliński, Czesław: Improving Mizar texts with properties and requirements (2004)
- Pollet, Martin; Sorge, Volker; Kerber, Manfred: Intuitive and formal representations: The case of matrices (2004)
- Richter, Stefan: Formalizing integration theory with an application to probabilistic algorithms (2004)
- Simpson, Carlos: Computer theorem proving in mathematics (2004)
- Urban, Josef: MPTP-motivation, implementation, first experiments (2004)
- Wells, Benjamin: Applying, extending, and specializing pseudorecursiveness (2004)
- Asperti, Andrea (ed.); Buchberger, Bruno (ed.); Davenport, James H. (ed.): Mathematical knowledge management. Second international conference, MKM 2003, Bertinoro, Italy, February 16--18, 2003. Proceedings (2003)
- Bancerek, Grzegorz: On the structure of Mizar types (2003)
- Bancerek, Grzegorz; Rudnicki, Piotr: Information retrieval in MML (2003)
- Barendregt, Henk: Towards an interactive mathematical proof mode (2003)
- Dahn, Ingo (ed.); Vigneron, Laurent (ed.): Proceedings of the workshop on mathematics, logic and computation (satellite event of ICALP 2003), Valencia, Spain, June 12--14, 2003 (2003)
- Farmer, William M.; von Mohrenschildt, Martin: An overview of a formal framework for managing mathematics (2003)
- Rudnicki, Piotr; Trybulec, Andrzej: On the integrity of a repository of formalized mathematics (2003)