System komputerowy Mizar narzędziem do komputerowego wspomagania nauczania w szkole wyższej

Ewa Borak

Abstract


The MIZAR system is a computer system for representing mathematical proofs in such a way that the computer checks their correctness. The texts written in the MIZAR language are called Mizar articles and are organized into the Mizar Mathematical Library (MML). Since the very beginnig of the development of the MIZAR system, experiments using MIZAR as a tool for teaching mathematics have been conducted. Numerous courses were organized which were based on different versions of the system: starting from the first implementation of its processor, through MIZAR-MSE, MIZAR-4 and PC-MIZAR, up till its current version. The first MIZAR-aided classes were introduced in 1975. In this paper we present the MIZAR system and the Mizar language and discusse courses conducted in the Institute of Informatics at the Univesity of Białystok. These courses employ MIZAR as the main tool of instruction.

References


Borak, E., Zalewska, A.: 2007, Mizar course in logic and set theory, w: M. Kauers (red.), Towards Mechanized Mathematical Assistants, Proceedings of 14th Symposium Calculemus 2007 and 6th International Conference MKM 2007, LNCS 4573, 191-204.

Fitch, F. B.: 1952, Symbolic Logic. An Introduction, The Ronald Press Company, New York.

Grądzka, E.: 2000, On the Order-consistent Topology of Complete and Uncomplete Lattices, M. Sc. thesis, Białystok University, Białystok.

Hoover, H. J., Rudnicki, P.: 1994, Introduction to Logic in Computing Science, CMPUT 172, University of Alberta, Edmonton.

Jaśkowski, S.: 1934, On the rules of supposition in formal logic, Studia Logica 1, 5-32.

Kordos, M., Szczerba, L.: 1976, Geometria dla nauczycieli, PWN, Warszawa.

Korniłowicz, A.: 2001, A Formal Theory of Abstract Computers, PhD thesis, Shinshu University, Nagano.

Moszner, P.: 1989, Mizar as tool of CAT, Bulletin of the Association for Computerised Logic Teaching 2(2), 16-18.

Muzalewski, M.: 1993, An Outline of PC Mizar, Fondation Philippe le Hodey, Brusseles.

Nakamura, Y., Watanabe, T., Tanaka, Y., Kawamoto, P.: 2002, Mizar Lecture Notes (4th Edition), Shinshu University, Departament of Information Engineering, Kiso Lab., Nagano.

Naumowicz, A.: 2005, Mizar Codification of the Theory of Partial Linear Spaces as an Example of Formalizing Recent Mathematical Results, PhD thesis, Shinshu University, Nagano.

Naumowicz, A., Korniłowicz, A.: 2009, A brief overview of Mizar, w: S. Berghofer (red.), TPHOLs 2009, LNCS 5674, Springer-Verlag Berlin Heidelberg, 67-72.

Ono, K.: 1962, On practical way of describing formal deduction, Nagoya Mathematical Journal 21, 115-121.

Prażmowski, K., Rudnicki, P.: 1983a, Kurs logiki w Mizarze-MSE (1), Delta 9, 8-9.

Prażmowski, K., Rudnicki, P.: 1983b, Kurs logiki w Mizarze-MSE (2), Delta 10, 13-14.

Prażmowski, K., Rudnicki, P.: 1983c, Kurs logiki w Mizarze-MSE (3), Delta 11, 7.

Prażmowski, K., Rudnicki, P.: 1983d, Kurs logiki w Mizarze-MSE (4), Delta 12, 6.

Prażmowski, K., Rudnicki, P.: 1984a, Kurs logiki w Mizarze-MSE (10), Delta 6, 4.

Prażmowski, K., Rudnicki, P.: 1984b, Kurs logiki w Mizarze-MSE (5), Delta 1, 15-16.

Prażmowski, K., Rudnicki, P.: 1984c, Kurs logiki w Mizarze-MSE (6), Delta 2, 12.

Prażmowski, K., Rudnicki, P.: 1984d, Kurs logiki w Mizarze-MSE (7), Delta 3, 13.

Prażmowski, K., Rudnicki, P.: 1984e, Kurs logiki w Mizarze-MSE (8), Delta 4, 15.

Prażmowski, K., Rudnicki, P.: 1984f, Kurs logiki w Mizarze-MSE (9), Delta 5, 13.

Retel, K., Zalewska, A.: 2005, Mizar as a tool for teaching mathematics, Mechanized Mathematics and Its Applications 4, 25-33.

Schwarzweller, C.: 2005, Mizar Verification of Generic Algebraic Algorithms, PhD thesis, Wilhelm-Schicard-Institute for Computer Science, Tubingem.

Suszko, R.: 1968, Ontology in the tractatus of L. Wittgenstein, Notre Dame Journal of Formal Logic 9, 7-33.

Szczerba, L. W.: 1987, The use of Mizar-MSE in a course in foundations of geometry, w: J. Srzednicki (red.), Initiatives in Logic, Nijhoff Publishers, Dordrecht, 231-232.

Trybulec, A.: 1982, Logic Information Language MIZAR-MSE, ICS PAS Reports, nr 465, Institute of Computer Science Polish Academy of Sciences, Warsaw.

Trybulec, A.: 1990, Tarski Grothendieck set theory, Formalized Mathematics 1(1), 9-11.

Urban, J.: 2010, Mizar Mode for Emacs, http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MizarMode, data dostępu: 1 XII 2010 r.

Zalewska, A.: 1987, Application of Mizar-MSE in a course in logic, w: J. Srzednicki (red.), Initiatives in Logic, Nijhoff Publishers, Dordrecht, 224-230.


Full Text: PDF (Polski)

e-ISSN: 2450-341X, ISSN: 2080-9751

AUPC SDMP is on the List of the Ministry’s scored journals (part B) with 5 points for 2016