Abstract

On July 20 - 22, 1995, Warsaw University (Bialystok Branch) hosted the QED Workshop II. The workshop was under the auspices of the State Committee for Scientific Research (Poland), supported by special funding from the Office of Naval Research (USA), cosponsored by Microsoft (Poland) and the Mizar Users Group.

QED is the title of an international project to build a computer system that effectively represents much of important mathematical knowledge and technique. The QED system will conform to the highest standards of mathematical rigor, including the use of strict formality in the internal representation of knowledge and the use of mechanical methods to check proofs of the correctness of all entries in the system. A principal application of the QED system will be the verification of computer programs. For background on the idea of the QED Project see "The QED Manifesto", Automated Deduction - CADE 12, Springer Verlag, LNAI 814, pp. 238-251, 1994, and available by anonymous ftp at info.mcs.anl.gov, file pub/qed/manifesto. The results of the QED Workshop I (1994) are documented in URL http://www.mcs.anl.gov/qed/.

The workshop was split into one-hour discussions dedicated to specific problems. Each such discussion was preceded by a short introductory lecture. Reports of the presentations and discussions are attached below.

Contents

  • 1. Introduction - Roman Matuszewski - (.ps)
  • 2. Can we resolve the tension between constructive type theorists and classical mathematicians? - Paul Jackson - (.ps)
  • 3. The organization of a data base of mathematical knowledge - Martin Strecker - (.ps)
  • 4. Indefiniteness - Randall Holmes - (.ps)
  • 5. Possible use of already formalized mathematical knowledge - Manfred Kerber - (.ps)
  • 6. Reflection: practical necessity or not? - John Harrison - (.ps)
  • 7. Development of analysis in the QED Project - Javier Thayer - (.ps)
  • 8. Mathematical synthesis - Peter White - (.ps)
  • 9. The mutilated checkerboard in set theory - John McCarthy - (.ps)
  • 10. To type or not to type - Piotr Rudnicki - (.ps)
  • 11. Cooperation of automated and interactive theorem provers - Ingo Dahn - (.ps)
  • 12. What are the connections, inter-relations and antipathies between proof checking and automated theorem proving? - Deepak Kapur - (.ps)
  • 13. The mutilated chessboard problem - checked by Mizar - Grzegorz Bancerek - (.ps)
  • 14. What can QED offer to mathematics? - Manfred Kerber - (.ps)
  • 15. General discussion: Where do we go from here? - Deepak Kapur - (.ps)
    ( romat-16.10.1995)