To Table of Contents No.1

Report on QED Workshop, Warsaw University, 1995

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 of Argonne National Laboratory (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.