The Bibliography of the Mizar Project

• Bonarska, E., An Introduction to PC Mizar, Fondation Ph. le Hodey, Brussels, 1990.
• Muzalewski, M., An Outline of PC Mizar, Fondation Philippe le Hodey, Brussels, 1993.
• Mizar Users Guide in Japaneese, Shinshu University, Nagano, 1994. (English translation available)
• Mizar Lecture Notes, 4th Edition, Shinshu University, Nagano, 2001.
• Wiedijk, F., Mizar: An Impression.
• Wiedijk, F., Writing a Mizar article in nine easy steps - nice tutorial (nearly up-to-date).

• Trybulec, A., Informationslogische Sprache Mizar, Dokumentation-Information, Heft 33, Ilmenau, 1977.
• Trybulec, A., The Mizar-QC/6000 Logic Information Language, ALLC Bulletin, Vol.6, No 2, 1978.
• Trybulec, A., The Mizar Logic Information Language, Studies in Logic, Grammar and Rhetoric, Vol.1, Bialystok, 1980.
• Rudnicki, P., Drabent, W., Proving Properties of Pascal Programs in Mizar 2, Acta Informatica 22, 1985, pp.311-331 (Errata).
• Trybulec, A., Blair, H., Computer Aided Reasoning, Proceedings of the Conference "Logic of Programs", LNCS Series, No193, Springer Verlag, 1985.
• Trybulec, A., Rudnicki, P., A Collection of TeXed Mizar Abstracts, University of Alberta, Canada, 1989.
• Bancerek, G., Tarski-Grothendieck Set Theory as a Basis of Knowledge Management System for Mathematics, 1990, 36th Conference of History of Logic.
• Rudnicki, P., An Overview of the Mizar Project, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad, 1992.
• Trybulec, A., Some Features of the Mizar Language, ESPRIT Workshop, Torino, 1993.
• Karno, Z., The Lattice of Topological Domains: an Example of Mizar Development, ESPRIT Workshop, Torino, 1993.
• Bancerek, G., Carlson, P., Semi-automatic translation for mathematics, Sprache - Kommunikation - Informatik, Max Niemeyer Verlag, Tubingen, 1993.
• Trybulec, A., Rudnicki, P., Using Mizar in Computer Aided Instruction of Mathematics, Norvegian-French Conference of CAI in Mathematics, Oslo, 1993.
• Matuszewski, R. (ed.), Formalized Mathematics, Vol. 1, 2, 3, Universite Catholique de Louvain - Fondation Philippe le Hodey, Brussels, 1990, 91, 92.
• Rudnicki, P., Trybulec, A., A Note on "How to Write a Proof", University of Alberta, Department of Computing Science, Tech. Rep. 96-08, 1996.
• Rudnicki, P., The Mutilated Checkerboard Problem in Mizar, University of Alberta, Department of Computing Science, Tech. Rep. 96-09, 1996.
• Schwarzweller, Ch., Mizar Verification of Generic Algebraic Algorithms. PhD thesis, Wilhelm-Schickard-Institute for Computer Science, University of Tuebingen, 1997.
• Schwarzweller, Ch., Using Mizar to Prove Generic Algebraic Algorithms Correct. TR University of Tuebingen, 1997.
• Rudnicki, P., Trybulec, A., On Equivalents of Well-foundedness. An experiment in Mizar, Journal of Automated Reasoning, vol. 23, pp. 197-234, 1999.
• Bancerek, G., Development of the theory of continuous lattices in Mizar, in: Kerber, M., Kohlhase, M. (eds.), Symbolic Computation and Automated Reasoning, The Calculemus-2000 Symposium, A K Peters 2000, pp. 65-80.
• Rudnicki, P., Schwarzweller, C., Trybulec, A., Commutative Algebra in the Mizar System, Journal of Symbolic Computation, vol. 32, pp. 143-169, 2001.
• Naumowicz, A., Bylinski, C. Basic Elements of Computer Algebra in MIZAR, Mechanized Mathematics and Its Applications, ISSN 1345-8272, Vol. 2: 9-16, 2002.
• Bancerek, G, Rudnicki, P., A Compendium of Continuous Lattices in Mizar: Formalizing recent mathematics, Journal of Automated Reasoning, vol. 29(3-4) pp. 189-224, 2002.
• Bancerek, G., Rudnicki, P., Information retrieval in MML, in: Asperti, A., Buchberger, B., Davenport, J. H (eds.), Proceedings of MKM-2003, Springer, LNCS 2594, pp. 119-132, 2003.
• Rudnicki, P., Trybulec, A., On the integrity of a repository of formal mathematics in: Asperti, A., Buchberger, B., Davenport, J. H (eds.), Proceedings of MKM-2003, Springer, LNCS 2594, pp. 162-174, 2003.
• Naumowicz, A., Bylinski, C. Improving Mizar Texts with Properties and Requirements, In A. Asperti et al. (Eds.), MKM 2004, LNCS 3119, pp. 290-301, Springer-Verlag Berlin Heidelberg, 2004.

Works devoted to Mizar-MSE

• Trybulec, A., Jezyk Informacyjno Logiczny Mizar-MSE, ICS PAS Reports, Nr 465, Warsaw, 1982.
• Prazmowski, K., Rudnicki, P. Kurs Logiki w Mizarze-MSE, Monthly DELTA, No 9 and next ones, Warsaw, 1983, 1984.
• Trybulec, A., Mizar-MSE Declaration, Polish Computer Society, ICM'83, Warsaw, 1983, manuscript.
• Prazmowski, K., Rudnicki, P., A Draft of Mizar-MSE Primer, ICS PAS Reports, No 529, Warsaw, 1983.
• Matuszewski, R., Mizar-MSE (CMS), Mode d'emploi, Centre de Calcul UCL, Louvain-la-Neuve, 1984.
• Trybulec, A., On a System of Computer-Aided Instruction of Logic, Bulletin of the Section of Logic PAS, Vol.12, No 4, Warsaw-Lodz, 1984.
• Mostowski, M., Trybulec, Z., A Certain Experimental Computer Aided Course of Logic in Poland, Proceedings of World Conference on Computer in Education, IFIP/AFIPS, Norfolk, North Holland, 1985.
• Matuszewski, R., Mizar-MSE, Enseignement des Fondements de la Mathematique Appuye par Ordinateurs, Symposium International IFIP/ICOMIDC, Monastir, 1986.
• MacKellar, B., An Introduction to Mizar-MSE, Summer Mizar Workshop, Fondation Philippe le Hodey, Fourdrain, 1985.
• Gainer, P., Kalantar, M., Kruszewski, P., Mah, G., MacMizar-MSE, University of Alberta, Edmonton, 1987, manuscript.
• Artalejo, M.R., Computerised Logic Teaching with Mizar, Computerised Logic Teaching Bulletin, Vol.1, No 1, Scotland, 1988.
• Bylinski, C., Coolsaet, K., Mizar-MSE on the MAID-machine, Computerised Logic Teaching Bulletin, Vol.1, No 2, Scotland, 1988.
• Nieva Soto, S., The Reasoner of Mizar/LOG, Computerised Logic Teaching Bulletin, Vol.2, No 1, Scotland, 1989.

Works devoted to pedagogical and philosophical aspects of Mizar-MSE

• Bujnowska, I., Mostowski, M., Zalewska, A., Justifications by analogy in mathematical proofs, Studies in Logic, Grammar and Rhetoric, Bialystok, 1986.
• Marciszewski, W., Systems of Computer-Aided Reasoning for Mathematics and Natural Language, Initiatives in Logic, Nijhoff Publishers, Dordrecht, 1987.
• Zalewska, A., An Application of Mizar-MSE in a Course in Logic, Initiatives in Logic, Nijhoff Publishers, Dordrecht, 1987.
• Szczerba, L.W., The Use of Mizar-MSE in a Course in Foundations of Geometry, Initiatives in Logic, Nijhoff Publishers, Dordrecht, 1987.
• Rudnicki, P., Obvious Inferences, Journal of Automated Reasoning, No 3, Reidel, 1987.
• Swieczkowska, H., Trybulec, Z., The Form of Mathematical Theorems and the Ways of Their Formulation in Mathematical Texts, Studies in Logic, Grammar and Rhetoric, Bialystok, 1989.
• Moszner, P., Mizar as a Tool of Computer Aided Teaching, Computerised Logic Teaching Bulletin, Vol.2, No 2, Scotland, 1989.
• Malinowski, G., Elements of Logic, Edition Fondation Philippe le Hodey, 1990.
• Malinowski, G., Elements de logique, Edition Fondation Philippe le Hodey, 1993.
• Mostowski, M., An Introduction to Elementary Logic of Quantifiers-Computer Aided Course, Fondation Philippe le Hodey, Brussels, 1993.
• Hoover, H.J., Rudnicki, P., Introduction to Logic in Computing Science, University of Alberta, CMPUT 172, Edmonton, 1994.

Works devoted to natural deduction systems in Jaskowski style

• Mostowski, M., Quantifiers Definable by Second Order Means, in Quantifiers: Logics, Models and Computations, vol. 2 (ed. M. Krynicki, M. Mostowski, L. W. Szczerba), Kluwer Academic Publishers, 1995, pp. 181-214.
• Marciszewski, W., A Jaskowski-Style System of Computer-Assisted Reasoning, Philosophical Logic in Poland, Kluwer Academic Publishers, 1994,   pp. 85-101.