Practical computer formalization of mathematics with the
Mizar proof assistant
25–28 January 2010
University of Hyderabad, Gachibowli, India
University of Hyderabad, Gachibowli, India
The workshop Practical computer formalization of mathematics with the Mizar proof assistant is part of ISLA 2010, the third Indian School on Logic and its Applications.
The workshop happens in the second week of ISLA 2010, from 25 January till 28 January, 2010. The details of the talks are as below.
Adam Naumowicz (University of Białystok, Poland)
Introduction to the Mizar proof-assistant
Monday, 25 January 2010, 10:45–11:45
[Abstract +]This talk will provide an overview of the Mizar system used for practical computer formalization of mathematical theorems. The participants will get familiar with the formal Mizar language used for encoding mathematics, the logical foundations of the verification system, and also the world's largest repository of formalized and computer-checked mathematical knowledge, Mizar Mathematical Library.
Some examples demonstrating the practice of creating rigorous mathematics in regular university-level courses on logic and set theory will be presented. The talk will also provide links to several external systems connected with Mizar that facilitate the whole process of writing formal mathematics, e.g. effective semantic-based information retrieval, browsing the contents of MML in 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.
Artur Kornilowicz (University of Białystok, Poland)
Practical presentation of Mizar and the contents of Mizar Mathematical Library
Tuesday, 26 January 2010, 12:00–13:00
[Abstract +]This talk will be devoted to presenting how the informal mathematical text is turned into a formal Mizar script verified by the computer.
The basic syntax of Mizar reflecting the notions used in standard mathematics will be described. Building formulas, statements, and natural deduction proofs will be demonstrated on a basis of simple examples from set theory.
The theory of monoids will serve as an example of developing definitions and theorems into a whole theory.
The structure and contents of Mizar Mathematical Library will be briefly described, providing information on the domains of mathematics that have been formalized, important theorems, most difficult proofs, etc.
Czeslaw Byliński (University of Białystok, Poland)
The implementation of Mizar proof-checking software
Wednesday, 27 January 2010, 12:00–13:00
[Abstract +]This talk will describe the implementation details of the Mizar proof-checker including a historical perspective.
The participants will learn how the language is analysed by the software on the lexical, syntactic and semantic level.
The modules of the Mizar verifier and their functions will be presented in detail. The talk will also present recent directions in developing the software by strengthening the capabilities of the proof-checker and currently considered future enhancements.
Also, the practice of creating and maintaining the database of formal texts will be described.
Several utility programs for enhancing Mizar texts will be demonstrated.
-
Josef Urban (Radboud University, Nijmegen)
Artificial intelligence methods in automated reasoning
Thursday, 27 January 2010, 12:00–13:00
[Abstract +]This talk will offer a perspective on Mizar and its large formal library as an interesting emerging topic for Automated Reasoning and general Artificial Intelligence methods.
A short overview of the translation between the Mizar formalism and untyped first-order logic (used by existing strong automated theorem provers (ATPs)) will be given, providing also semantics for Mizar based on untyped first-order logic.
A system for independent ATP-based cross-verification of the Mizar formalizations (made possible by the Mizar-to-ATP translation) will be presented. The task of Automated Reasoning over a very large mathematical theory (knowledge base) will be shortly discussed, and some recent results and combined deductive/inductive AI systems built for this purpose will be presented.
Organisers
Adam Naumowicz (University of Białystok, Poland)