ITEE seminar: Prof Piotr Rudnicki, 01.00PM, Thu 10 Apr 2003

Mizar and its applications

Speaker: Prof Piotr Rudnicki, Department of Computing Science, University of Alberta, Canada

When: 01.00PM, Thursday 10 Apr 2003

Venue: 78-420

Host: Dr Colin Fidge

Abstract:

  Mizar is a proof-checking system used to build the Mizar
  Mathematical Library (MML) - a long term project aiming at building
  a comprehensive library of formalized mathematical knowledge.

  The main goal for the design of Mizar (an effort led by Dr. Andrzej
  Trybulec) has been to create a formal system close to the
  mathematical vernacular used in main-stream mathematical
  publications with the requirement that the language be simple enough
  to enable computerized processing, in particular mechanical
  verification of correctness.  The continual development of Mizar has
  resulted in a language, software for checking the correctness of
  texts written in it, numerous utility programs, a centrally
  maintained library of mathematics, and an electronic hyper-linked
  journal, all of which are available on the Internet
  (http://mizar.org).  The logic of Mizar is classical, the proofs are
  written in a natural (Jaskowski) deduction style and like almost all
  of mathematics it is based on ZF set theory + existence of
  arbitrarily large, strongly inaccessible cardinals.  Mizar
  definitions allow to introduce new constructors for types, algebraic
  structures, terms, adjectives, and atomic formulae.  The Mizar
  language and the checking software evolve, and the evolution is
  driven by the growing library.

  The talk starts with the general information on the Mizar system,
  its history, its current state and its future.  Then, depending on
  the interest of the audience, we can look deeper into:

  - overview of the contents of the Mizar Mathematical Library
  - Mizar in education: logic and mathematics
  - Mizar in verification: algorithms, software, hardware
  - searching problems and tools for the Mizar library

Biography:

  In Poland, Dr. Rudnicki worked at the Polish Academy of Sciences in
  the Institute of the Foundations of Computer Science in Warsaw.
  Since 1984, he has been at the University of Alberta.  Dr. Rudnicki
  has participated in the Mizar (mizar.org) project since its
  beginning in 1973 and his research has been associated with this
  project ever since. Mizar is a long term project aiming at building
  a comprehensive library of formalized mathematical knowledge based
  on classical logic and set theory.  Besides formalizing pure
  mathematics, Dr. Rudnicki has applied Mizar at the experimental
  level in verification of algorithms, software and hardware.

Contact:

Dr Colin Fidge, seminar host (cjf@itee.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator) (guido@itee.uq.edu.au)

ITEE seminar web page: http://www.itee.uq.edu.au/~seminar

[All seminars]