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

Ewa Borak

Annales Universitatis Paedagogicae Cracoviensis | Studia ad Didacticam Mathematicae Pertinentia (2010)

  • Volume: 3, page 21-40
  • ISSN: 2080-9751

Abstract

top
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.

How to cite

top

Ewa Borak. "System komputerowy Mizar narzędziem do komputerowego wspomagania nauczania w szkole wyższej." Annales Universitatis Paedagogicae Cracoviensis | Studia ad Didacticam Mathematicae Pertinentia 3 (2010): 21-40. <http://eudml.org/doc/296395>.

@article{EwaBorak2010,
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.},
author = {Ewa Borak},
journal = {Annales Universitatis Paedagogicae Cracoviensis | Studia ad Didacticam Mathematicae Pertinentia},
language = {pol},
pages = {21-40},
title = {System komputerowy Mizar narzędziem do komputerowego wspomagania nauczania w szkole wyższej},
url = {http://eudml.org/doc/296395},
volume = {3},
year = {2010},
}

TY - JOUR
AU - Ewa Borak
TI - System komputerowy Mizar narzędziem do komputerowego wspomagania nauczania w szkole wyższej
JO - Annales Universitatis Paedagogicae Cracoviensis | Studia ad Didacticam Mathematicae Pertinentia
PY - 2010
VL - 3
SP - 21
EP - 40
AB - 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.
LA - pol
UR - http://eudml.org/doc/296395
ER -

References

top
  1. 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. 
  2.  
  3. Fitch, F. B.: 1952, Symbolic Logic. An Introduction, The Ronald Press Company, New York. 
  4.  
  5. Grądzka, E.: 2000, On the Order-consistent Topology of Complete and Uncomplete Lattices, M. Sc. thesis, Białystok University, Białystok. 
  6.  
  7. Hoover, H. J., Rudnicki, P.: 1994, Introduction to Logic in Computing Science, CMPUT 172, University of Alberta, Edmonton. 
  8.  
  9. Jaśkowski, S.: 1934, On the rules of supposition in formal logic, Studia Logica 1, 5-32. 
  10.  
  11. Kordos, M., Szczerba, L.: 1976, Geometria dla nauczycieli, PWN, Warszawa. 
  12.  
  13. Korniłowicz, A.: 2001, A Formal Theory of Abstract Computers, PhD thesis, Shinshu University, Nagano. 
  14.  
  15. Moszner, P.: 1989, Mizar as tool of CAT, Bulletin of the Association for Computerised Logic Teaching 2(2), 16-18. 
  16.  
  17. Muzalewski, M.: 1993, An Outline of PC Mizar, Fondation Philippe le Hodey, Brusseles. 
  18.  
  19. Nakamura, Y., Watanabe, T., Tanaka, Y., Kawamoto, P.: 2002, Mizar Lecture Notes (4th Edition), Shinshu University, Departament of Information Engineering, Kiso Lab., Nagano. 
  20.  
  21. 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. 
  22.  
  23. 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. 
  24.  
  25. Ono, K.: 1962, On practical way of describing formal deduction, Nagoya Mathematical Journal 21, 115-121. 
  26.  
  27. Prażmowski, K., Rudnicki, P.: 1983a, Kurs logiki w Mizarze-MSE (1), Delta 9, 8-9. 
  28.  
  29. Prażmowski, K., Rudnicki, P.: 1983b, Kurs logiki w Mizarze-MSE (2), Delta 10, 13-14. 
  30.  
  31. Prażmowski, K., Rudnicki, P.: 1983c, Kurs logiki w Mizarze-MSE (3), Delta 11, 7. 
  32.  
  33. Prażmowski, K., Rudnicki, P.: 1983d, Kurs logiki w Mizarze-MSE (4), Delta 12, 6. 
  34.  
  35. Prażmowski, K., Rudnicki, P.: 1984a, Kurs logiki w Mizarze-MSE (10), Delta 6, 4. 
  36.  
  37. Prażmowski, K., Rudnicki, P.: 1984b, Kurs logiki w Mizarze-MSE (5), Delta 1, 15-16. 
  38.  
  39. Prażmowski, K., Rudnicki, P.: 1984c, Kurs logiki w Mizarze-MSE (6), Delta 2, 12. 
  40.  
  41. Prażmowski, K., Rudnicki, P.: 1984d, Kurs logiki w Mizarze-MSE (7), Delta 3, 13. 
  42.  
  43. Prażmowski, K., Rudnicki, P.: 1984e, Kurs logiki w Mizarze-MSE (8), Delta 4, 15. 
  44.  
  45. Prażmowski, K., Rudnicki, P.: 1984f, Kurs logiki w Mizarze-MSE (9), Delta 5, 13. 
  46.  
  47. Retel, K., Zalewska, A.: 2005, Mizar as a tool for teaching mathematics, Mechanized Mathematics and Its Applications 4, 25-33. 
  48.  
  49. Schwarzweller, C.: 2005, Mizar Verification of Generic Algebraic Algorithms, PhD thesis, Wilhelm-Schicard-Institute for Computer Science, Tubingem. 
  50.  
  51. Suszko, R.: 1968, Ontology in the tractatus of L. Wittgenstein, Notre Dame Journal of Formal Logic 9, 7-33. 
  52.  
  53. 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. 
  54.  
  55. Trybulec, A.: 1982, Logic Information Language MIZAR-MSE, ICS PAS Reports, nr 465, Institute of Computer Science Polish Academy of Sciences, Warsaw. 
  56.  
  57. Trybulec, A.: 1990, Tarski Grothendieck set theory, Formalized Mathematics 1(1), 9-11. 
  58.  
  59. Urban, J.: 2010, Mizar Mode for Emacs, http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MizarMode, data dostępu: 1 XII 2010 r. 
  60.  
  61. Zalewska, A.: 1987, Application of Mizar-MSE in a course in logic, w: J. Srzednicki (red.), Initiatives in Logic, Nijhoff Publishers, Dordrecht, 224-230. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.