Beth Dissertation Award

Conference on Formal Grammar

ESSLLI Poster







Weather Forecast |  Weather Maps |  Weather Radar

Logic and computation

Week 1 Time: 9:00 - 10:30 Room 249


An Introduction to Computer Formalization of Mathematics

Adam Naumowicz

Website


Content of the course:

The proposed course will provide an introduction to practical computer formalization of mathematical theorems using the Mizar system. The system is best noted for its formal language derived from informal mathematics and the world’s largest repository of formalized and computer-checked mathematical knowledge, Mizar Mathematical Library (MML). In the first part of the course, the ESSLLI school participants will be able to learn both the formal Mizar language used for encoding mathematics and the logical foundations of the verification system.
By its design, Mizar supports writing proofs in a declarative way (i.e mostly forward reasoning), resembling the standard mathematical practice. The proofs written in Mizar are constructed according to the rules of the Fitch-Jaśkowski style of natural deduction. It is this part of the Mizar language that has had the biggest influence on other systems and became the inspiration to develop similar proof layers on top of several procedural systems. To name the most important ones, there was the system Declare by D. Syme, the Mizar mode for HOL by J. Harrison, the Isar language for Isabelle by M. Wenzel, Mizar-light for HOL-light by F. Wiedijk and most recently the declarative proof language (DPL) for Coq by P. Corbineau. The Mizar way of writing proofs was also the model for the notion of ’formal proof sketches’ developed by F. Wiedijk. The second part of the course will show how to use this technique to encode informal mathematics into fully formal proofs.
Apart from the long-term goal of developing MML into a database for mathematics, one of the most important applications of Mizar today is in mathematics education by demonstrating the practice of creating rigorous mathematics. For several decades Mizar has been used for educational purposes on various levels: from secondary school to doctoral studies. Usually the teaching was organized as Mizar-aided courses, most typically on introduction to logic, topology, lattice theory, general and universal algebra, category theory, etc. Easy to follow examples of proofs concerning basic set theoretic notions (sets, relations, functions, etc.) will be presented during the course. Apart from first-order reasoning steps, the course will also present reasoning based on the use of schemes (e.g. inductive proofs in arithmetic).
The current distribution of MML includes over a thousand articles comprising about fifty thousand theorems and ten thousand definitions written by over two hundred authors from Canada, China, Czech Republic, Germany, Italy, Japan, the Netherlands, Poland, Russia and USA. All these developments have been created in a steady fashion on top of the chosen axiomatics and previously formalized data. Effective formalization requires a interaction with this huge collection of data. Therefore MML’s structure, organization, current development and methods of maintenance will be showed at the end of the course.
To facilitate the whole process of writing formal mathematics, several external systems have been developed that complement the Mizar proof checker, which might be very interesting to ESSLLI students with various computer science ad mathematical background. For example, effective semantic-based information retrieval, i.e., searching, browsing and presentation of MML can be done with the MML Query system developed by G. Bancerek. Several sites provide an on-line Mizar processor, writing proofs may also be assisted by the systems MoMM (a matching and interreduction tool) and the Mizar Proof Advisor developed by J. Urban. The contents of MML as well as newly created documents can be presented in various user-friendly formats, including a semantically-linked XML-based web pages or an automatically generated translation into English in the form of an electronic and printed journal, Formalized Mathematics. The use and capabilities of these systems will be demonstrated during the course.

Tentative outline

Day 1: The language of mathematics in the formalized computer environment

Day 2: From informal mathematics, through proof sketches to formal proofs

Day 3: Formalizing proofs about basic set theoretic notions (sets, relations, functions, etc.)

Day 4: Formalizing inductive proofs (e.g. in arithmetic)

Day 5: Interacting with a semanticaly-linked library of formal mathematical knowledge

References

• A. Grabowski, A. Kornilowicz and A. Naumowicz: Mizar in a Nutshell. In: A. Asperti et al. (Eds.) User Tutorials I. Journal of Formalized Reasoning 3(2), pp. 153-245, 2010 (available at: http://jfr.cib.unibo.it/article/viewFile/1980/1356)

• A. Naumowicz and A. Kornilowicz: A Brief Overview of Mizar. In: S. Berghofer et al. (Eds.), TPHOLs 2009, Springer LNCS 5674, 2009 (available at: http://www.springerlink.com/content/08138878w5n05278/)

• F. Wiedijk (Ed.): Seventeen Provers of the World. Springer LNAI 3600, 2006 (available at: http://link.springer.de/link/service/series/0558/tocs/t3600.htm)

• F. Wiedijk: Writing a Mizar Article in Nine Easy Steps (available at: http://www.cs.ru.nl/~freek/mizar/mizman.pdf)

Prerequisites

The only prerequisites for the course are basic knowledge of classical first-order logic and set theoretic foundations of mathematics. As the course is based on using an interactive proof assistant software, good computer text editing skills would be an asset. The level of the course will be comparable to the papers listed above. However, mastering the topic requires also some guided practice which the course will provide for the participants.


Minister of Science and Higher Education - Professor Barbara Kudrycka Marshall of Opole Province (Voivodeship) - Mr Józef Sebesta Rector of Opole University - Professor Krystyna Czaja Mayor of Opole - Mr Ryszard Zembaczyński RADIO OPOLE TVP Opole Polish Association for Logic and Philosophy of Science The INFTY Research Networking Programme The Association for Symbolic Logic European Network for Social Intelligence ZAK S.A. Cement Plant ODRA

Springer Princeton University Press Cambridge Scholars Publishers Oxford University Press Birkhauser