Content Development for Distance Education in Advanced University Mathematics Using Mizar

点击翻译按钮获取中文摘要

The Mizar system is a software program to mechanically verify the correctness of theorem proofs written in a formal mathematical language. The applicants have helped to drive an international project for pursuing research on the formalization of mathematical theorems using the Mizar system and creating an open archive of the compiled mathematical knowledge. In order to apply the results of this work to education, the members built a module for embedding the Mizar system into an e-learning CMS used in a graduate curriculum and developed contents for training students in logic and advanced university mathematics. The results of this research offer an effective solution to the serious and difficult task of "training logical thinking skills to students" in higher education.