The Bibliography of the Mizar Project

• Grabowski, A., Kornilowicz, A., Naumowicz, A., Mizar in a Nutshell, in: A. Asperti, J. Harrison and C. Munoz (Eds.) User Tutorials I, Journal of Formalized Reasoning 3(2), pp. 153-245, 2010.
• Wiedijk, F., Writing a Mizar article in nine easy steps - a nice tutorial (nearly up-to-date).
• Wiedijk, F., Mizar: An Impression.
• Mizar Lecture Notes, 4th Edition, Shinshu University, Nagano, 2001.
• Mizar Users Guide in Japaneese, Shinshu University, Nagano, 1994. (English translation available)
• Muzalewski, M., An Outline of PC Mizar, Fondation Philippe le Hodey, Brussels, 1993.
• Bonarska, E., An Introduction to PC Mizar, Fondation Ph. le Hodey, Brussels, 1990.
• Kornilowicz, A., Skeletons of Mizar proofs.

• Nice, concise and up-to-date introduction to the repository of mathematical knowledge encoded in Mizar by Sebastian Koch

• Bancerek G., Bylinski C., Grabowski A., Kornilowicz A., Matuszewski R., Naumowicz A., Pak K., Urban J., Mizar: State-of-the-Art and Beyond. In M. Kerber et al. (Eds.), Intelligent Computer Mathematics, CICM 2015, LNAI 9150, pp. 261-279, 2015
• Trybulec A., Kornilowicz A., Naumowicz A., Kuperberg K., Formal Mathematics for Mathematicians, Journal of Automated Reasoning, Volume 50, Issue 2, pp. 119-121, DOI: 10.1007/s10817-012-9268-z, Springer Netherlands, 2013.
• Kornilowicz A., On Rewriting Rules in Mizar, Journal of Automated Reasoning, Volume 50, Issue 2, pp. 203-210, DOI: 10.1007/s10817-012-9261-6, Springer Netherlands, 2013.
• Pak K., Methods of Lemma Extraction in Natural Deduction Proofs, Journal of Automated Reasoning, Volume 50, Issue 2, pp. 217-228, DOI: 10.1007/s10817-012-9267-0, Springer Netherlands, 2013.
• Kornilowicz A., Tentative Experiments with Ellipsis in Mizar, In "Jeuring, Johan and Campbell, John A. and Carette, Jacques and Dos Reis, Gabriel and Sojka, Petr and Wenzel, Makarius and Sorge, Volker, Intelligent Computer Mathematics 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects", Bremen, Germany, July 8-13, 2012, Proceedings, LNAI 7362 © Springer Verlag, pp. 453-457, 2012.
• Naumowicz, A., Kornilowicz, A., A Brief Overview of Mizar, in: S. Berghofer et al. (Eds.), TPHOLs 2009, LNCS 5674, Springer-Verlag Berlin Heidelberg, 2009.
• 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.
• 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.
• 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.
• 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.
• Rudnicki, P., Schwarzweller, C., Trybulec, A., Commutative Algebra in the Mizar System, Journal of Symbolic Computation, vol. 32, pp. 143-169, 2001.
• 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., Trybulec, A.,On Equivalents of Well-foundedness. An experiment in Mizar, Journal of Automated Reasoning, vol. 23, pp. 197-234, 1999.
• Schwarzweller, Ch., Using Mizar to Prove Generic Algebraic Algorithms Correct. TR University of Tuebingen, 1997.
• Schwarzweller, Ch., Mizar Verification of Generic Algebraic Algorithms. PhD thesis, Wilhelm-Schickard-Institute for Computer Science, University of Tuebingen, 1997.
• Rudnicki, P., The Mutilated Checkerboard Problem in Mizar, University of Alberta, Department of Computing Science, Tech. Rep. 96-09, 1996.
• Rudnicki, P., Trybulec, A., A Note on "How to Write a Proof", University of Alberta, Department of Computing Science, Tech. Rep. 96-08, 1996.
• Matuszewski, R. (ed.), Formalized Mathematics, Vol. 1, 2, 3, Universite Catholique de Louvain - Fondation Philippe le Hodey, Brussels, 1990, 91, 92.
• Trybulec, A., Rudnicki, P., Using Mizar in Computer Aided Instruction of Mathematics, Norvegian-French Conference of CAI in Mathematics, Oslo, 1993.
• Bancerek, G., Carlson, P., Semi-automatic translation for mathematics, Sprache - Kommunikation - Informatik, Max Niemeyer Verlag, Tubingen, 1993.
• Karno, Z., The Lattice of Topological Domains: an Example of Mizar Development, ESPRIT Workshop, Torino, 1993.
• Trybulec, A., Some Features of the Mizar Language, ESPRIT Workshop, Torino, 1993.
• 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.
• Bancerek, G., Tarski-Grothendieck Set Theory as a Basis of Knowledge Management System for Mathematics, 1990, 36th Conference of History of Logic.
• Trybulec, A., Rudnicki, P., A Collection of TeXed Mizar Abstracts, University of Alberta, Canada, 1989.
• Trybulec, A., Blair, H., Computer Aided Reasoning, Proceedings of the Conference "Logic of Programs", LNCS Series, No193, Springer Verlag, 1985.
• Rudnicki, P., Drabent, W., Proving Properties of Pascal Programs in Mizar 2, Acta Informatica 22, 1985, pp.311-331 (Errata).
• Trybulec, A., The Mizar Logic Information Language, Studies in Logic, Grammar and Rhetoric, Vol.1, Bialystok, 1980.
• Trybulec, A., The Mizar-QC/6000 Logic Information Language, ALLC Bulletin, Vol.6, No 2, 1978.
• Trybulec, A., Informationslogische Sprache Mizar, Dokumentation-Information, Heft 33, Ilmenau, 1977.

Works devoted to Mizar-MSE

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

Works devoted to pedagogical and philosophical aspects of Mizar-MSE

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

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.